Skip to content

Commit 44c008f

Browse files
undergraduate-ruiqi-chenundergraduate-ruiqi-chen
authored
feat(Algebra/Category): some lemmas about adjunctions in Under R (#24589)
* The adjunction between `tensorProd R S` and `forget R S` * topFunctor * Slight changes and some translation * Move some code to Adjunctions.lean * finish proving toUnder_eq * Commented * Using cast in toUnder_eq * Solving tensorProd_freeAbs_tauto * Tidy the proof * tensorProd_freeAbs * prepare for freeAbs_ℤ_tauto * Finish proving adjFreeForget * Remove Topology & add copyright * Slight Changes * Slight Changes, add some comments * Slight Changes
1 parent be447a3 commit 44c008f

4 files changed

Lines changed: 219 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,7 @@ import Mathlib.Algebra.Category.Ring.Instances
183183
import Mathlib.Algebra.Category.Ring.Limits
184184
import Mathlib.Algebra.Category.Ring.LinearAlgebra
185185
import Mathlib.Algebra.Category.Ring.Topology
186+
import Mathlib.Algebra.Category.Ring.Under.Adjunctions
186187
import Mathlib.Algebra.Category.Ring.Under.Basic
187188
import Mathlib.Algebra.Category.Ring.Under.Limits
188189
import Mathlib.Algebra.Category.Semigrp.Basic

‎Mathlib/Algebra/Category/Ring/Topology.lean‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Category.Ring.Colimits
77
import Mathlib.Algebra.Category.Ring.Constructions
88
import Mathlib.Algebra.MvPolynomial.CommRing
99
import Mathlib.Topology.Algebra.Ring.Basic
10+
import Mathlib.Topology.Category.TopCat.Basic
1011

1112
/-!
1213
# Topology on `Hom(R, S)`
@@ -137,8 +138,6 @@ instance [TopologicalSpace S] [IsTopologicalRing S] [T1Space S] [CompactSpace S]
137138
CompactSpace (R ⟶ S) :=
138139
(isClosedEmbedding_hom R S).compactSpace
139140

140-
open Limits
141-
142141
/-- `Hom(A ⊗[S] B, R)` has the subspace topology from `Hom(A, R) × Hom(B, R)`. -/
143142
lemma isEmbedding_pushout [TopologicalSpace R] [IsTopologicalRing R]
144143
(φ : S ⟶ A) (ψ : S ⟶ B) :
@@ -173,4 +172,17 @@ lemma isEmbedding_pushout [TopologicalSpace R] [IsTopologicalRing R]
173172
congr($(pushout.condition (f := φ)).hom s).symm
174173
ext f s <;> simp [fA, fB, fAB, PA, PB, PAB, F, this]
175174

175+
variable (S) in
176+
/-- The functor defined by above construction. -/
177+
def topFunctor [TopologicalSpace S] : CommRingCatᵒᵖ ⥤ TopCat where
178+
obj R := TopCat.of (R.unop ⟶ S)
179+
map f := TopCat.ofHom {
180+
toFun := (f.unop ≫ ·)
181+
continuous_toFun := continuous_precomp f.unop
182+
}
183+
184+
/-- The Yoneda embedding factors through topFunctor. -/
185+
@[simp]
186+
lemma topFunctor_forget [TopologicalSpace S] : topFunctor S ⋙ forget TopCat = yoneda.obj S := rfl
187+
176188
end CommRingCat.HomTopology

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

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
/-
2+
Copyright (c) 2025 Ruiqi Chen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ruiqi Chen
5+
-/
6+
import Mathlib.Algebra.Category.Ring.Under.Basic
7+
import Mathlib.Algebra.MvPolynomial.Basic
8+
import Mathlib.RingTheory.TensorProduct.MvPolynomial
9+
import Mathlib.Algebra.MvPolynomial.CommRing
10+
import Mathlib.Algebra.Category.Ring.Adjunctions
11+
12+
/-!
13+
# Adjunctions related to `Under (R : CommRingCat)`
14+
15+
In this file we provide functors `forgetRelative R S : Under S ⥤ Under R` for `S` an `R`-algebra,
16+
`freeAbsolute R : Type u ⥤ Under R` the free functor given by polynomials over `R` and
17+
`forget : Under R ⥤ Type u` the forgetful functor. And prove some basic facts including adjunctions
18+
`tensorProd R S ⊣ forgetRelative R S` and `freeAbsolute R ⊣ forget`.
19+
-/
20+
21+
noncomputable section
22+
23+
open TensorProduct CategoryTheory
24+
25+
universe u
26+
variable {R S : CommRingCat.{u}}
27+
variable [Algebra R S]
28+
29+
namespace CommRingCat
30+
31+
variable (R S) in
32+
/-- The forgetful base change functor. -/
33+
@[simps! map_right]
34+
def forgetRelative : Under S ⥤ Under R := Under.map <| ofHom Algebra.algebraMap
35+
36+
/-- The adjunction between `tensorProd R S` and `forgetRelative R S`. -/
37+
@[simps! unit_app counit_app]
38+
def adjTensorForget : tensorProd R S ⊣ forgetRelative R S :=
39+
(Under.mapPushoutAdj (ofHom <| algebraMap R S)).ofNatIsoLeft ((R.tensorProdIsoPushout S).symm)
40+
41+
variable (R) in
42+
/-- The free functor given by polynomials. -/
43+
@[simps! map_right]
44+
def freeAbsolute : Type u ⥤ Under R where
45+
obj σ := R.mkUnder <| MvPolynomial σ R
46+
map f := (MvPolynomial.rename f).toUnder
47+
map_id σ := congr_arg (fun x => x.toUnder) <| MvPolynomial.rename_id (σ := σ) (R := R)
48+
map_comp f g := congr_arg (fun x => x.toUnder) (MvPolynomial.rename_comp_rename (R := R) f g).symm
49+
50+
@[simp]
51+
lemma freeAbsolute_obj (σ : Type u) : algebra ((freeAbsolute R).obj σ) = MvPolynomial.algebra :=
52+
mkUnder_eq <| MvPolynomial σ R
53+
54+
@[simp]
55+
lemma freeAbsolute_map {σ τ : Type u} (f : σ ⟶ τ) :
56+
toAlgHom ((freeAbsolute R).map f) =
57+
(cast <| congr_arg₂
58+
(fun instA instB => @AlgHom R (MvPolynomial σ R) (MvPolynomial τ R) _ _ _ instA instB)
59+
(mkUnder_eq (MvPolynomial σ R)).symm
60+
(mkUnder_eq (MvPolynomial τ R)).symm) (MvPolynomial.rename f)
61+
:= AlgHom.toUnder_eq (MvPolynomial.rename f)
62+
63+
/-- The forgetful functor `Under R ⥤ CommRingCat ⥤ Type`. -/
64+
def forget : Under R ⥤ Type u := Under.forget R ⋙ HasForget.forget
65+
66+
lemma tensorProd_freeAbsolute_tauto : freeAbsolute R ⋙ R.tensorProd S = {
67+
obj σ := S.mkUnder <| S ⊗[R] (MvPolynomial σ R)
68+
map f := (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).toUnder
69+
map_id σ := by
70+
simp only
71+
have : MvPolynomial.rename (𝟙 σ) = AlgHom.id R (MvPolynomial σ R) :=
72+
MvPolynomial.rename_id (R := R) (σ := σ)
73+
rw [this, Algebra.TensorProduct.map_id]
74+
rfl
75+
map_comp f g := by
76+
simp only
77+
have : MvPolynomial.rename (R := R) (f ≫ g) =
78+
(MvPolynomial.rename g).comp (MvPolynomial.rename f) :=
79+
(MvPolynomial.rename_comp_rename f g).symm
80+
rw [this, Algebra.TensorProduct.map_id_comp, AlgHom.toUnder_comp]
81+
} := by
82+
apply CategoryTheory.Functor.ext
83+
· intro σ τ f
84+
unfold freeAbsolute tensorProd
85+
dsimp
86+
rw [AlgHom.toUnder_eq]
87+
-- find out the path induction
88+
have (ninstσ : Algebra R (MvPolynomial σ R)) (ninstτ : Algebra R (MvPolynomial τ R))
89+
(eqσ : ninstσ = MvPolynomial.algebra) (eqτ : ninstτ = MvPolynomial.algebra) :
90+
(@Algebra.TensorProduct.map _ _ _ _ _ _ _ _ _ _ _ _ _ _
91+
(ninstσ) _ _ _ _ _ (ninstτ) (AlgHom.id S S)
92+
((cast <| congr_arg₂ (fun instσ instτ => @AlgHom R (MvPolynomial σ R)
93+
(MvPolynomial τ R) _ _ _ instσ instτ)
94+
eqσ.symm eqτ.symm) (MvPolynomial.rename f))).toUnder =
95+
eqToHom (congr_arg
96+
(fun inst => S.mkUnder <| @TensorProduct R _ S (MvPolynomial σ R) _ _ _
97+
(@Algebra.toModule _ _ _ _ inst)) <| eqσ) ≫
98+
(@Algebra.TensorProduct.map _ _ _ _ _ _ _ _ _ _ _ _ _ _ MvPolynomial.algebra _ _ _ _ _
99+
MvPolynomial.algebra (AlgHom.id S S) (MvPolynomial.rename f)).toUnder ≫
100+
eqToHom (congr_arg
101+
(fun inst => S.mkUnder <| @TensorProduct R _ S (MvPolynomial τ R) _ _ _
102+
(@Algebra.toModule _ _ _ _ inst)) <| eqτ).symm := by
103+
subst eqσ eqτ
104+
rfl
105+
exact this (algebra (R.mkUnder (MvPolynomial σ R))) (algebra (R.mkUnder (MvPolynomial τ R)))
106+
(mkUnder_eq (MvPolynomial σ R)) (mkUnder_eq (MvPolynomial τ R))
107+
108+
/-- We obtain `freeAbsolute S` by base changing `freeAbsolute R` using `⊗[R] S`. -/
109+
def tensorProd_freeAbsolute : freeAbsolute R ⋙ R.tensorProd S ≅ freeAbsolute S := by
110+
-- To get rid of algebra_eq
111+
rw [tensorProd_freeAbsolute_tauto]
112+
exact (NatIso.ofComponents
113+
(fun σ => (MvPolynomial.algebraTensorAlgEquiv (σ := σ) R S).symm.toUnder)
114+
(fun {σ τ} f => by
115+
show (MvPolynomial.rename f).toUnder ≫
116+
(MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.toUnder
117+
= (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.toUnder ≫
118+
(Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).toUnder
119+
suffices (MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom.comp (MvPolynomial.rename f)
120+
= (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f)).comp
121+
(MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom from
122+
congr_arg (fun f => f.toUnder) this
123+
suffices (e : σ) →
124+
(MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom
125+
((MvPolynomial.rename f) (MvPolynomial.X e))
126+
= (Algebra.TensorProduct.map (AlgHom.id S S) (MvPolynomial.rename f))
127+
((MvPolynomial.algebraTensorAlgEquiv R S).symm.toAlgHom (MvPolynomial.X e)) from by
128+
exact MvPolynomial.algHom_ext this
129+
unfold MvPolynomial.algebraTensorAlgEquiv
130+
simp only [AlgEquiv.toAlgHom_eq_coe, MvPolynomial.rename_X, AlgHom.coe_coe,
131+
AlgEquiv.ofAlgHom_symm_apply, MvPolynomial.aeval_X, Algebra.TensorProduct.map_tmul,
132+
AlgHom.coe_id, id_eq, implies_true]
133+
)).symm
134+
135+
/-- A commutative ring is an algebra over `ℤ` which is commutative. -/
136+
def Under_ℤ : Under (of (ULift.{u, 0} ℤ)) ≌ CommRingCat.{u} :=
137+
Under.equivalenceOfIsInitial isInitial
138+
139+
/-- The defined `freeAbsolute ℤ` is isomorphic to `free` -/
140+
def freeAbsolute_ℤ_tauto : free ⋙ Under_ℤ.inverse ≅ freeAbsolute (of (ULift.{u, 0} ℤ)) where
141+
hom := {
142+
app σ := Under.homMk
143+
(CommRingCat.ofHom <| MvPolynomial.map <| Int.castRingHom (ULift.{u, 0} ℤ))
144+
(Limits.IsInitial.hom_ext isInitial _ _)
145+
naturality {σ τ} f := by
146+
apply Under.UnderMorphism.ext
147+
exact hom_ext <| MvPolynomial.map_comp_rename (Int.castRingHom (ULift.{u, 0} ℤ)) f
148+
}
149+
inv := {
150+
app σ := Under.homMk (CommRingCat.ofHom <| MvPolynomial.map RingHom.smulOneHom)
151+
(Limits.IsInitial.hom_ext isInitial _ _)
152+
naturality {σ τ} f := by
153+
apply Under.UnderMorphism.ext
154+
exact hom_ext <| MvPolynomial.map_comp_rename RingHom.smulOneHom f
155+
}
156+
hom_inv_id := by
157+
ext σ (x : MvPolynomial σ ℤ)
158+
show (MvPolynomial.map RingHom.smulOneHom)
159+
((MvPolynomial.map (Int.castRingHom (ULift.{u, 0} ℤ))) x) = x
160+
rw [MvPolynomial.map_map _ (RingHom.smulOneHom (R := (ULift.{u, 0} ℤ)))]
161+
have : RingHom.smulOneHom.comp (Int.castRingHom (ULift.{u, 0} ℤ)) = RingHom.id ℤ := by aesop_cat
162+
rw [this]
163+
exact MvPolynomial.map_id x
164+
inv_hom_id := by
165+
ext σ (x : MvPolynomial σ (ULift.{u, 0} ℤ))
166+
show (MvPolynomial.map (Int.castRingHom (ULift.{u, 0} ℤ)))
167+
((MvPolynomial.map RingHom.smulOneHom) x) = x
168+
rw [MvPolynomial.map_map]
169+
have : (Int.castRingHom (ULift.{u, 0} ℤ)).comp (RingHom.smulOneHom (R := ULift.{u, 0} ℤ))
170+
= RingHom.id (ULift.{u, 0} ℤ) := by aesop_cat
171+
rw [this]
172+
exact MvPolynomial.map_id x
173+
174+
instance (R : CommRingCat.{u}) : Algebra (of (ULift.{u, 0} ℤ)) R
175+
:= RingHom.toAlgebra RingHom.smulOneHom
176+
177+
/-- The free forgetful adjunction of `Under R`. -/
178+
def adjFreeForget : freeAbsolute R ⊣ forget :=
179+
(adj.comp (Under_ℤ.symm.toAdjunction.comp adjTensorForget)).ofNatIsoLeft
180+
(isoWhiskerRight freeAbsolute_ℤ_tauto ((of (ULift.{u, 0} ℤ)).tensorProd R)
181+
≪≫ tensorProd_freeAbsolute)
182+
183+
end CommRingCat

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

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ namespace CommRingCat
2828
instance : CoeSort (Under R) (Type u) where
2929
coe A := A.right
3030

31-
instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
31+
instance algebra (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
3232

3333
/-- Turn a morphism in `Under R` into an algebra homomorphism. -/
3434
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}
6262
ext x
6363
exact h x
6464

65+
@[simp]
66+
lemma mkUnder_eq (A : Type u) [CommRing A] [inst : Algebra R A] :
67+
algebra (R.mkUnder A) = inst := Algebra.algebra_ext _ _ (congrFun rfl)
68+
6569
end CommRingCat
6670

6771
namespace AlgHom
@@ -85,6 +89,22 @@ lemma toUnder_comp {A B C : Type u} [CommRing A] [CommRing B] [CommRing C]
8589
(g.comp f).toUnder = f.toUnder ≫ g.toUnder :=
8690
rfl
8791

92+
@[simp]
93+
lemma toUnder_eq {A B : Type u} [CommRing A] [CommRing B]
94+
[instA : Algebra R A] [instB : Algebra R B] (f : A →ₐ[R] B) : CommRingCat.toAlgHom f.toUnder =
95+
(cast <| congr_arg₂ (fun instA instB => @AlgHom R A B _ _ _ instA instB)
96+
(CommRingCat.mkUnder_eq A).symm (CommRingCat.mkUnder_eq B).symm) f :=
97+
have [instA : Algebra R A] [instB : Algebra R B] [instA' : Algebra R A] [instB' : Algebra R B]
98+
(eqA : instA = instA') (eqB : instB = instB') (f : @AlgHom R A B _ _ _ instA instB) :
99+
@OneHom.toFun A B _ _ f = @OneHom.toFun A B _ _ (
100+
(cast <| congr_arg₂ (fun instA instB => @AlgHom R A B _ _ _ instA instB) eqA eqB) f
101+
) := by
102+
subst eqA eqB
103+
rfl
104+
ext <| congrFun <| this (instA := instA) (instB := instB)
105+
(instA' := CommRingCat.algebra (R.mkUnder A)) (instB' := CommRingCat.algebra (R.mkUnder B))
106+
(CommRingCat.mkUnder_eq A).symm (CommRingCat.mkUnder_eq B).symm f
107+
88108
end AlgHom
89109

90110
namespace AlgEquiv

0 commit comments

Comments
 (0)