Skip to content

Commit 50468bb

Browse files
YaelDillieserdOneKiolt
committed
feat: the category of commutative bialgebras (leanprover-community#27120)
Define the bundled category `CommBialgCat R` of commutative bialgebras over a fixed commutative ring `R` along with the forgetful functor to `CommAlgCat`. From Toric Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Michał Mrugała <kiolterino@gmail.com>
1 parent 0950f17 commit 50468bb

3 files changed

Lines changed: 235 additions & 2 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,7 @@ import Mathlib.Algebra.Category.CoalgCat.Monoidal
9898
import Mathlib.Algebra.Category.CommAlgCat.Basic
9999
import Mathlib.Algebra.Category.CommAlgCat.FiniteType
100100
import Mathlib.Algebra.Category.CommAlgCat.Monoidal
101+
import Mathlib.Algebra.Category.CommBialgCat
101102
import Mathlib.Algebra.Category.ContinuousCohomology.Basic
102103
import Mathlib.Algebra.Category.FGModuleCat.Basic
103104
import Mathlib.Algebra.Category.FGModuleCat.Colimits

‎Mathlib/Algebra/Category/CommAlgCat/Basic.lean‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -146,17 +146,19 @@ def isoMk {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Algebra R X} {_
146146

147147
/-- Build an `AlgEquiv` from an isomorphism in the category `CommAlgCat R`. -/
148148
@[simps]
149-
def ofIso (i : A ≅ B) : A ≃ₐ[R] B where
149+
def algEquivOfIso (i : A ≅ B) : A ≃ₐ[R] B where
150150
__ := i.hom.hom
151151
toFun := i.hom
152152
invFun := i.inv
153153
left_inv x := by simp
154154
right_inv x := by simp
155155

156+
@[deprecated (since := "2025-08-22")] alias ofIso := algEquivOfIso
157+
156158
/-- Algebra equivalences between `Algebra`s are the same as isomorphisms in `CommAlgCat`. -/
157159
@[simps]
158160
def isoEquivAlgEquiv : (of R X ≅ of R Y) ≃ (X ≃ₐ[R] Y) where
159-
toFun := ofIso
161+
toFun := algEquivOfIso
160162
invFun := isoMk
161163

162164
instance reflectsIsomorphisms_forget : (forget (CommAlgCat.{u} R)).ReflectsIsomorphisms where

‎Mathlib/Algebra/Category/CommBialgCat.lean‎

Lines changed: 230 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,230 @@
1+
/-
2+
Copyright (c) 2025 Yaël Dillies, Michał Mrugała, Andrew Yang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies, Michał Mrugała, Andrew Yang
5+
-/
6+
import Mathlib.Algebra.Category.CommAlgCat.Monoidal
7+
import Mathlib.CategoryTheory.Monoidal.Mon_
8+
import Mathlib.RingTheory.Bialgebra.Equiv
9+
10+
/-!
11+
# The category of commutative bialgebras over a commutative ring
12+
13+
This file defines the bundled category `CommBialgCat R` of commutative bialgebras over a fixed
14+
commutative ring `R` along with the forgetful functor to `CommAlgCat`.
15+
-/
16+
17+
noncomputable section
18+
19+
open Bialgebra Coalgebra Opposite CategoryTheory Limits Mon_Class
20+
open scoped MonoidalCategory
21+
22+
universe v u
23+
variable {R : Type u} [CommRing R]
24+
25+
variable (R) in
26+
/-- The category of commutative `R`-bialgebras and their morphisms. -/
27+
structure CommBialgCat where
28+
private mk ::
29+
/-- The underlying type. -/
30+
carrier : Type v
31+
[commRing : CommRing carrier]
32+
[bialgebra : Bialgebra R carrier]
33+
34+
namespace CommBialgCat
35+
variable {A B C : CommBialgCat.{v} R} {X Y Z : Type v} [CommRing X] [Bialgebra R X]
36+
[CommRing Y] [Bialgebra R Y] [CommRing Z] [Bialgebra R Z]
37+
38+
attribute [instance] commRing bialgebra
39+
40+
initialize_simps_projections CommBialgCat (-commRing, -bialgebra)
41+
42+
instance : CoeSort (CommBialgCat R) (Type v) := ⟨carrier⟩
43+
44+
attribute [coe] CommBialgCat.carrier
45+
46+
variable (R) in
47+
/-- Turn an unbundled `R`-bialgebra into the corresponding object in the category of `R`-bialgebras.
48+
49+
This is the preferred way to construct a term of `CommBialgCat R`. -/
50+
abbrev of (X : Type v) [CommRing X] [Bialgebra R X] : CommBialgCat.{v} R := ⟨X⟩
51+
52+
variable (R) in
53+
lemma coe_of (X : Type v) [CommRing X] [Bialgebra R X] : (of R X : Type v) = X := rfl
54+
55+
/-- The type of morphisms in `CommBialgCat R`. -/
56+
@[ext]
57+
structure Hom (A B : CommBialgCat.{v} R) where
58+
private mk ::
59+
/-- The underlying bialgebra map. -/
60+
hom' : A →ₐc[R] B
61+
62+
instance : Category (CommBialgCat.{v} R) where
63+
Hom A B := Hom A B
64+
id A := ⟨.id R A⟩
65+
comp f g := ⟨g.hom'.comp f.hom'⟩
66+
67+
instance : ConcreteCategory (CommBialgCat.{v} R) (· →ₐc[R] ·) where
68+
hom := Hom.hom'
69+
ofHom := Hom.mk
70+
71+
/-- Turn a morphism in `CommBialgCat` back into a `BialgHom`. -/
72+
abbrev Hom.hom (f : Hom A B) : A →ₐc[R] B := ConcreteCategory.hom (C := CommBialgCat R) f
73+
74+
/-- Typecheck a `BialgHom` as a morphism in `CommBialgCat R`. -/
75+
abbrev ofHom {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Bialgebra R X}
76+
{_ : Bialgebra R Y} (f : X →ₐc[R] Y) : of R X ⟶ of R Y :=
77+
ConcreteCategory.ofHom (C := CommBialgCat R) f
78+
79+
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
80+
def Hom.Simps.hom (A B : CommBialgCat.{v} R) (f : Hom A B) := f.hom
81+
82+
initialize_simps_projections Hom (hom' → hom)
83+
84+
/-!
85+
The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`.
86+
-/
87+
88+
@[simp] lemma hom_id : (𝟙 A : A ⟶ A).hom = AlgHom.id R A := rfl
89+
@[simp] lemma hom_comp (f : A ⟶ B) (g : B ⟶ C) : (f ≫ g).hom = g.hom.comp f.hom := rfl
90+
91+
lemma id_apply (A : CommBialgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp
92+
lemma comp_apply (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by simp
93+
94+
@[ext] lemma hom_ext {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g := Hom.ext hf
95+
96+
@[simp] lemma hom_ofHom (f : X →ₐc[R] Y) : (ofHom f).hom = f := rfl
97+
@[simp] lemma ofHom_hom (f : A ⟶ B) : ofHom f.hom = f := rfl
98+
99+
@[simp] lemma ofHom_id : ofHom (.id R X) = 𝟙 (of R X) := rfl
100+
101+
@[simp]
102+
lemma ofHom_comp (f : X →ₐc[R] Y) (g : Y →ₐc[R] Z) : ofHom (g.comp f) = ofHom f ≫ ofHom g := rfl
103+
104+
lemma ofHom_apply (f : X →ₐc[R] Y) (x : X) : ofHom f x = f x := rfl
105+
106+
lemma inv_hom_apply (e : A ≅ B) (x : A) : e.inv (e.hom x) = x := by simp
107+
lemma hom_inv_apply (e : A ≅ B) (x : B) : e.hom (e.inv x) = x := by simp
108+
109+
instance : Inhabited (CommBialgCat R) := ⟨of R R⟩
110+
111+
lemma forget_obj (A : CommBialgCat.{v} R) : (forget (CommBialgCat.{v} R)).obj A = A := rfl
112+
113+
lemma forget_map (f : A ⟶ B) : (forget (CommBialgCat.{v} R)).map f = f := rfl
114+
115+
instance : CommRing ((forget (CommBialgCat R)).obj A) := inferInstanceAs <| CommRing A
116+
117+
instance : Bialgebra R ((forget (CommBialgCat R)).obj A) := inferInstanceAs <| Bialgebra R A
118+
119+
instance hasForgetToCommAlgCat : HasForget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R) where
120+
forget₂.obj M := .of R M
121+
forget₂.map f := CommAlgCat.ofHom f.hom
122+
123+
@[simp] lemma forget₂_commAlgCat_obj (A : CommBialgCat.{v} R) :
124+
(forget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)).obj A = .of R A := rfl
125+
126+
@[simp] lemma forget₂_commAlgCat_map (f : A ⟶ B) :
127+
(forget₂ (CommBialgCat.{v} R) (CommAlgCat.{v} R)).map f = CommAlgCat.ofHom f.hom := rfl
128+
129+
/-- Forgetting to the underlying type and then building the bundled object returns the original
130+
bialgebra. -/
131+
@[simps]
132+
def ofSelfIso (M : CommBialgCat.{v} R) : of R M ≅ M where
133+
hom := 𝟙 M
134+
inv := 𝟙 M
135+
136+
/-- Build an isomorphism in the category `CommBialgCat R` from a `BialgEquiv` between
137+
`Bialgebra`s. -/
138+
@[simps]
139+
def isoMk {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Bialgebra R X}
140+
{_ : Bialgebra R Y} (e : X ≃ₐc[R] Y) : of R X ≅ of R Y where
141+
hom := ofHom (e : X →ₐc[R] Y)
142+
inv := ofHom (e.symm : Y →ₐc[R] X)
143+
144+
/-- Build a `BialgEquiv` from an isomorphism in the category `CommBialgCat R`. -/
145+
@[simps apply, simps -isSimp symm_apply]
146+
def bialgEquivOfIso (i : A ≅ B) : A ≃ₐc[R] B where
147+
__ := i.hom.hom
148+
toFun := i.hom
149+
invFun := i.inv
150+
left_inv x := by simp
151+
right_inv x := by simp
152+
153+
/-- Bialgebra equivalences between `Bialgebra`s are the same as isomorphisms in `CommBialgCat`. -/
154+
@[simps]
155+
def isoEquivBialgEquiv : (of R X ≅ of R Y) ≃ (X ≃ₐc[R] Y) where
156+
toFun := bialgEquivOfIso
157+
invFun := isoMk
158+
left_inv _ := rfl
159+
right_inv _ := rfl
160+
161+
instance reflectsIsomorphisms_forget : (forget (CommBialgCat.{u} R)).ReflectsIsomorphisms where
162+
reflects {X Y} f _ := by
163+
let i := asIso ((forget (CommBialgCat.{u} R)).map f)
164+
let e : X ≃ₐc[R] Y := { f.hom, i.toEquiv with }
165+
exact (isoMk e).isIso_hom
166+
167+
end CommBialgCat
168+
169+
attribute [local ext] Quiver.Hom.unop_inj
170+
171+
instance CommAlgCat.mon_ClassOpOf {A : Type u} [CommRing A] [Bialgebra R A] :
172+
Mon_Class (op <| CommAlgCat.of R A) where
173+
one := (CommAlgCat.ofHom <| counitAlgHom R A).op
174+
mul := (CommAlgCat.ofHom <| comulAlgHom R A).op
175+
one_mul := by ext; exact Coalgebra.rTensor_counit_comul _
176+
mul_one := by ext; exact Coalgebra.lTensor_counit_comul _
177+
mul_assoc := by ext; exact (Coalgebra.coassoc_symm_apply _).symm
178+
179+
@[simp]
180+
lemma CommAlgCat.one_op_of_unop_hom {A : Type u} [CommRing A] [Bialgebra R A] :
181+
η[op <| CommAlgCat.of R A].unop.hom = counitAlgHom R A := rfl
182+
183+
@[simp]
184+
lemma CommAlgCat.mul_op_of_unop_hom {A : Type u} [CommRing A] [Bialgebra R A] :
185+
μ[op <| CommAlgCat.of R A].unop.hom = comulAlgHom R A := rfl
186+
187+
instance {A : Type u} [CommRing A] [Bialgebra R A] [IsCocomm R A] :
188+
IsCommMon (Opposite.op <| CommAlgCat.of R A) where
189+
mul_comm := by ext; exact comm_comul R _
190+
191+
instance {A B : Type u} [CommRing A] [Bialgebra R A] [CommRing B] [Bialgebra R B]
192+
(f : A →ₐc[R] B) : IsMon_Hom (CommAlgCat.ofHom (f : A →ₐ[R] B)).op where
193+
194+
instance (A : (CommAlgCat R)ᵒᵖ) [Mon_Class A] : Bialgebra R A.unop :=
195+
.ofAlgHom μ[A].unop.hom η[A].unop.hom
196+
congr(($((Mon_Class.mul_assoc_flip A).symm)).unop.hom)
197+
congr(($(Mon_Class.one_mul A)).unop.hom)
198+
congr(($(Mon_Class.mul_one A)).unop.hom)
199+
200+
variable (R) in
201+
/-- Commutative bialgebras over a commutative ring `R` are the same thing as comonoid
202+
`R`-algebras. -/
203+
@[simps! functor_obj_unop_X inverse_obj unitIso_hom_app
204+
unitIso_inv_app counitIso_hom_app counitIso_inv_app]
205+
def commBialgCatEquivComonCommAlgCat : CommBialgCat R ≌ (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ where
206+
functor.obj A := .op <| .mk <| .op <| .of R A
207+
functor.map {A B} f := .op <| .mk' <| .op <| CommAlgCat.ofHom f.hom
208+
inverse.obj A := .of R A.unop.X.unop
209+
inverse.map {A B} f := CommBialgCat.ofHom <| .ofAlgHom f.unop.hom.unop.hom
210+
congr(($(IsMon_Hom.one_hom (f := f.unop.hom))).unop.hom)
211+
congr(($((IsMon_Hom.mul_hom (f := f.unop.hom)).symm)).unop.hom)
212+
unitIso.hom := 𝟙 _
213+
unitIso.inv := 𝟙 _
214+
counitIso.hom := 𝟙 _
215+
counitIso.inv := 𝟙 _
216+
217+
@[simp]
218+
lemma commBialgCatEquivComonCommAlgCat_functor_map_unop_hom {A B : CommBialgCat R} (f : A ⟶ B) :
219+
((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom =
220+
(CommAlgCat.ofHom (AlgHomClass.toAlgHom f.hom)).op := rfl
221+
222+
@[simp]
223+
lemma commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom
224+
{A B : (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) :
225+
AlgHomClass.toAlgHom ((commBialgCatEquivComonCommAlgCat R).inverse.map f).hom =
226+
f.unop.hom.unop.hom := rfl
227+
228+
instance {A : CommBialgCat.{u} R} [IsCocomm R A] :
229+
IsCommMon ((commBialgCatEquivComonCommAlgCat R).functor.obj A).unop.X :=
230+
inferInstanceAs <| IsCommMon <| op <| CommAlgCat.of R A

0 commit comments

Comments
 (0)