feat(Algebra/Category): some lemmas about adjunctions in Under R

Mathlib.lean

@@ -183,6 +183,7 @@ 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,6 +7,7 @@ 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)`
@@ -137,8 +138,6 @@ 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) :
@@ -173,4 +172,17 @@ 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

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2025 Ruiqi Chen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ruiqi Chen
+-/
+import Mathlib.Algebra.Category.Ring.Under.Basic
+import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.RingTheory.TensorProduct.MvPolynomial
+import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.Algebra.Category.Ring.Adjunctions
+
+/-!
+# Adjunctions related to `Under (R : CommRingCat)`
+
+In this file we provide functors `forgetRelative R S : Under S ⥤ Under R` for `S` an `R`-algebra,
+`freeAbsolute R : Type u ⥤ Under R` the free functor given by polynomials over `R` and
+`forget : Under R ⥤ Type u` the forgetful functor. And prove some basic facts including adjunctions
+`tensorProd R S ⊣ forgetRelative R S` and `freeAbsolute R ⊣ forget`.
+-/
+
+noncomputable section
+
+open TensorProduct CategoryTheory
+
+universe u
+variable {R S : CommRingCat.{u}}
+variable [Algebra R S]
+
+namespace CommRingCat
+
+variable (R S) in
+/-- The forgetful base change functor. -/
+@[simps! map_right]
+def forgetRelative : Under S ⥤ Under R := Under.map <| ofHom Algebra.algebraMap
+
+/-- The adjunction between `tensorProd R S` and `forgetRelative R S`. -/
+@[simps! unit_app counit_app]
+def adjTensorForget : tensorProd R S ⊣ forgetRelative R S :=
+  (Under.mapPushoutAdj (ofHom <| algebraMap R S)).ofNatIsoLeft ((R.tensorProdIsoPushout S).symm)
+
+variable (R) in
+/-- The free functor given by polynomials. -/
+@[simps! map_right]
+def freeAbsolute : Type u ⥤ Under R where
+  obj σ := R.mkUnder <| MvPolynomial σ R
+  map f := (MvPolynomial.rename f).toUnder
+  map_id σ := congr_arg (fun x => x.toUnder) <| MvPolynomial.rename_id (σ := σ) (R := R)
+  map_comp f g := congr_arg (fun x => x.toUnder) (MvPolynomial.rename_comp_rename (R := R) f g).symm
+
+@[simp]
+lemma freeAbsolute_obj (σ : Type u) : algebra ((freeAbsolute R).obj σ) = MvPolynomial.algebra :=
+  mkUnder_eq <| MvPolynomial σ R
+
+@[simp]
+lemma freeAbsolute_map {σ τ : Type u} (f : σ ⟶ τ) :
+    toAlgHom ((freeAbsolute R).map f) =
+    (cast <| congr_arg₂
+    (fun instA instB => @AlgHom R (MvPolynomial σ R) (MvPolynomial τ R) _ _ _ instA instB)
+    (mkUnder_eq (MvPolynomial σ R)).symm
+    (mkUnder_eq (MvPolynomial τ R)).symm) (MvPolynomial.rename f)
+  := AlgHom.toUnder_eq (MvPolynomial.rename f)
+
+/-- The forgetful functor `Under R ⥤ CommRingCat ⥤ Type`. -/
+def forget : Under R ⥤ Type u := Under.forget R ⋙ HasForget.forget
+
+lemma tensorProd_freeAbsolute_tauto : freeAbsolute R ⋙ R.tensorProd S = {
+    obj σ := S.mkUnder <| S ⊗[R] (MvPolynomial σ R)
+    map f := (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).toUnder
+    map_id σ := by
+      simp only
+      have : MvPolynomial.rename (𝟙 σ) = AlgHom.id R (MvPolynomial σ R) :=
+        MvPolynomial.rename_id (R := R) (σ := σ)
+      rw [this, Algebra.TensorProduct.map_id]
+      rfl
+    map_comp f g := by
+      simp only
+      have : MvPolynomial.rename (R := R) (f ≫ g) =
+        (MvPolynomial.rename g).comp (MvPolynomial.rename f) :=
+        (MvPolynomial.rename_comp_rename f g).symm
+      rw [this, Algebra.TensorProduct.map_id_comp, AlgHom.toUnder_comp]
+    } := by
+  apply CategoryTheory.Functor.ext
+  · intro σ τ f
+    unfold freeAbsolute tensorProd
+    dsimp
+    rw [AlgHom.toUnder_eq]
+    -- find out the path induction
+    have (ninstσ : Algebra R (MvPolynomial σ R)) (ninstτ : Algebra R (MvPolynomial τ R))
+        (eqσ : ninstσ = MvPolynomial.algebra) (eqτ : ninstτ = MvPolynomial.algebra) :
+        (@Algebra.TensorProduct.map _ _ _ _ _ _ _ _ _ _ _ _ _ _
+        (ninstσ) _ _ _ _ _ (ninstτ) (AlgHom.id S S)
+        ((cast <| congr_arg₂ (fun instσ instτ => @AlgHom R (MvPolynomial σ R)
+            (MvPolynomial τ R) _ _ _ instσ instτ)
+        eqσ.symm eqτ.symm) (MvPolynomial.rename f))).toUnder =
+        eqToHom (congr_arg
+          (fun inst => S.mkUnder <| @TensorProduct R _ S (MvPolynomial σ R) _ _ _
+          (@Algebra.toModule _ _ _ _ inst)) <| eqσ) ≫
+        (@Algebra.TensorProduct.map _ _ _ _ _ _ _ _ _ _ _ _ _ _ MvPolynomial.algebra _ _ _ _ _
+          MvPolynomial.algebra (AlgHom.id S S) (MvPolynomial.rename f)).toUnder ≫
+        eqToHom (congr_arg
+          (fun inst => S.mkUnder <| @TensorProduct R _ S (MvPolynomial τ R) _ _ _
+          (@Algebra.toModule _ _ _ _ inst)) <| eqτ).symm := by
+      subst eqσ eqτ
+      rfl
+    exact this (algebra (R.mkUnder (MvPolynomial σ R))) (algebra (R.mkUnder (MvPolynomial τ R)))
+      (mkUnder_eq (MvPolynomial σ R)) (mkUnder_eq (MvPolynomial τ R))
+
+/-- We obtain `freeAbsolute S` by base changing `freeAbsolute R` using `⊗[R] S`. -/
+def tensorProd_freeAbsolute : freeAbsolute R ⋙ R.tensorProd S ≅ freeAbsolute S := by
+  -- To get rid of algebra_eq
+  rw [tensorProd_freeAbsolute_tauto]
+  exact (NatIso.ofComponents
+    (fun σ => (MvPolynomial.algebraTensorAlgEquiv (σ := σ) R S).symm.toUnder)
+    (fun {σ τ} f => by
+      show (MvPolynomial.rename f).toUnder ≫
+          (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.toUnder
+          = (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.toUnder ≫
+          (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).toUnder
+      suffices (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.comp (MvPolynomial.rename f)
+          = (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).comp
+            (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom from
+        congr_arg (fun f => f.toUnder) this
+      suffices (e : σ) →
+          (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom
+          ((MvPolynomial.rename f) (MvPolynomial.X e))
+          = (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f))
+          ((MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom (MvPolynomial.X e)) from by
+        exact MvPolynomial.algHom_ext this
+      unfold MvPolynomial.algebraTensorAlgEquiv
+      simp only [AlgEquiv.toAlgHom_eq_coe, MvPolynomial.rename_X, AlgHom.coe_coe,
+        AlgEquiv.ofAlgHom_symm_apply, MvPolynomial.aeval_X, Algebra.TensorProduct.map_tmul,
+        AlgHom.coe_id, id_eq, implies_true]
+    )).symm
+
+/-- A commutative ring is an algebra over `ℤ` which is commutative. -/
+def Under_ℤ : Under (of (ULift.{u, 0} ℤ)) ≌ CommRingCat.{u} :=
+  Under.equivalenceOfIsInitial isInitial
+
+/-- The defined `freeAbsolute ℤ` is isomorphic to `free` -/
+def freeAbsolute_ℤ_tauto : free ⋙ Under_ℤ.inverse ≅ freeAbsolute (of (ULift.{u, 0} ℤ)) where
+  hom := {
+    app σ := Under.homMk
+      (CommRingCat.ofHom <| MvPolynomial.map <| Int.castRingHom (ULift.{u, 0} ℤ))
+      (Limits.IsInitial.hom_ext isInitial _ _)
+    naturality {σ τ} f := by
+      apply Under.UnderMorphism.ext
+      exact hom_ext <| MvPolynomial.map_comp_rename (Int.castRingHom (ULift.{u, 0} ℤ)) f
+  }
+  inv := {
+    app σ := Under.homMk (CommRingCat.ofHom <| MvPolynomial.map RingHom.smulOneHom)
+      (Limits.IsInitial.hom_ext isInitial _ _)
+    naturality {σ τ} f := by
+      apply Under.UnderMorphism.ext
+      exact hom_ext <| MvPolynomial.map_comp_rename RingHom.smulOneHom f
+  }
+  hom_inv_id := by
+    ext σ (x : MvPolynomial σ ℤ)
+    show (MvPolynomial.map RingHom.smulOneHom)
+      ((MvPolynomial.map (Int.castRingHom (ULift.{u, 0} ℤ))) x) = x
+    rw [MvPolynomial.map_map _ (RingHom.smulOneHom (R := (ULift.{u, 0} ℤ)))]
+    have : RingHom.smulOneHom.comp (Int.castRingHom (ULift.{u, 0} ℤ)) = RingHom.id ℤ := by aesop_cat
+    rw [this]
+    exact MvPolynomial.map_id x
+  inv_hom_id := by
+    ext σ (x : MvPolynomial σ (ULift.{u, 0} ℤ))
+    show (MvPolynomial.map (Int.castRingHom (ULift.{u, 0} ℤ)))
+      ((MvPolynomial.map RingHom.smulOneHom) x) = x
+    rw [MvPolynomial.map_map]
+    have : (Int.castRingHom (ULift.{u, 0} ℤ)).comp (RingHom.smulOneHom (R := ULift.{u, 0} ℤ))
+        = RingHom.id (ULift.{u, 0} ℤ) := by aesop_cat
+    rw [this]
+    exact MvPolynomial.map_id x
+
+instance (R : CommRingCat.{u}) : Algebra (of (ULift.{u, 0} ℤ)) R
+  := RingHom.toAlgebra RingHom.smulOneHom
+
+/-- The free forgetful adjunction of `Under R`. -/
+def adjFreeForget : freeAbsolute R ⊣ forget :=
+  (adj.comp (Under_ℤ.symm.toAdjunction.comp adjTensorForget)).ofNatIsoLeft
+  (isoWhiskerRight freeAbsolute_ℤ_tauto ((of (ULift.{u, 0} ℤ)).tensorProd R)
+      ≪≫ tensorProd_freeAbsolute)
+
+end CommRingCat

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

@@ -28,7 +28,7 @@ namespace CommRingCat
 instance : CoeSort (Under R) (Type u) where
   coe A := A.right
 
-instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
+instance algebra (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,6 +62,10 @@ 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
@@ -85,6 +89,22 @@ 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