Revert "feat(Algebra/Category): some lemmas about adjunctions in Under R (#24589)"

This reverts commit 44c008f.

Author: erdOne

Mathlib.lean

@@ -183,7 +183,6 @@ import Mathlib.Algebra.Category.Ring.Instances
 import Mathlib.Algebra.Category.Ring.Limits
 import Mathlib.Algebra.Category.Ring.LinearAlgebra
 import Mathlib.Algebra.Category.Ring.Topology
-import Mathlib.Algebra.Category.Ring.Under.Adjunctions
 import Mathlib.Algebra.Category.Ring.Under.Basic
 import Mathlib.Algebra.Category.Ring.Under.Limits
 import Mathlib.Algebra.Category.Semigrp.Basic

Mathlib/Algebra/Category/Ring/Topology.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.Category.Ring.Colimits
 import Mathlib.Algebra.Category.Ring.Constructions
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.Topology.Algebra.Ring.Basic
-import Mathlib.Topology.Category.TopCat.Basic
 
 /-!
 # Topology on `Hom(R, S)`
@@ -138,6 +137,8 @@ instance [TopologicalSpace S] [IsTopologicalRing S] [T1Space S] [CompactSpace S]
     CompactSpace (R ⟶ S) :=
   (isClosedEmbedding_hom R S).compactSpace
 
+open Limits
+
 /-- `Hom(A ⊗[S] B, R)` has the subspace topology from `Hom(A, R) × Hom(B, R)`. -/
 lemma isEmbedding_pushout [TopologicalSpace R] [IsTopologicalRing R]
     (φ : S ⟶ A) (ψ : S ⟶ B) :
@@ -172,17 +173,4 @@ lemma isEmbedding_pushout [TopologicalSpace R] [IsTopologicalRing R]
     congr($(pushout.condition (f := φ)).hom s).symm
   ext f s <;> simp [fA, fB, fAB, PA, PB, PAB, F, this]
 
-variable (S) in
-/-- The functor defined by above construction. -/
-def topFunctor [TopologicalSpace S] : CommRingCatᵒᵖ ⥤ TopCat where
-  obj R := TopCat.of (R.unop ⟶ S)
-  map f := TopCat.ofHom {
-      toFun := (f.unop ≫ ·)
-      continuous_toFun := continuous_precomp f.unop
-    }
-
-/-- The Yoneda embedding factors through topFunctor. -/
-@[simp]
-lemma topFunctor_forget [TopologicalSpace S] : topFunctor S ⋙ forget TopCat = yoneda.obj S := rfl
-
 end CommRingCat.HomTopology

Mathlib/Algebra/Category/Ring/Under/Adjunctions.lean

@@ -28,7 +28,7 @@ namespace CommRingCat
 instance : CoeSort (Under R) (Type u) where
   coe A := A.right
 
-instance algebra (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
+instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
 
 /-- Turn a morphism in `Under R` into an algebra homomorphism. -/
 def toAlgHom {A B : Under R} (f : A ⟶ B) : A →ₐ[R] B where
@@ -62,10 +62,6 @@ lemma mkUnder_ext {A : Type u} [CommRing A] [Algebra R A] {B : Under R}
   ext x
   exact h x
 
-@[simp]
-lemma mkUnder_eq (A : Type u) [CommRing A] [inst : Algebra R A] :
-  algebra (R.mkUnder A) = inst := Algebra.algebra_ext _ _ (congrFun rfl)
-
 end CommRingCat
 
 namespace AlgHom
@@ -89,22 +85,6 @@ lemma toUnder_comp {A B C : Type u} [CommRing A] [CommRing B] [CommRing C]
     (g.comp f).toUnder = f.toUnder ≫ g.toUnder :=
   rfl
 
-@[simp]
-lemma toUnder_eq {A B : Type u} [CommRing A]  [CommRing B]
-  [instA : Algebra R A] [instB : Algebra R B] (f : A →ₐ[R] B) : CommRingCat.toAlgHom f.toUnder =
-      (cast <| congr_arg₂ (fun instA instB => @AlgHom R A B _ _ _ instA instB)
-      (CommRingCat.mkUnder_eq A).symm (CommRingCat.mkUnder_eq B).symm) f :=
-    have [instA : Algebra R A] [instB : Algebra R B] [instA' : Algebra R A] [instB' : Algebra R B]
-      (eqA : instA = instA') (eqB : instB = instB') (f : @AlgHom R A B _ _ _ instA instB) :
-      @OneHom.toFun A B _ _ f = @OneHom.toFun A B _ _ (
-        (cast <| congr_arg₂ (fun instA instB => @AlgHom R A B _ _ _ instA instB) eqA eqB) f
-      ) := by
-        subst eqA eqB
-        rfl
-    ext <| congrFun <| this (instA := instA) (instB := instB)
-      (instA' := CommRingCat.algebra (R.mkUnder A)) (instB' := CommRingCat.algebra (R.mkUnder B))
-      (CommRingCat.mkUnder_eq A).symm (CommRingCat.mkUnder_eq B).symm f
-
 end AlgHom
 
 namespace AlgEquiv