The category of commutative bialgebras over a commutative ring

This file defines the bundled category CommBialgCat R of commutative bialgebras over a fixed commutative ring R along with the forgetful functor to CommAlgCat.

structure CommBialgCat (R : Type u) [CommRing R] : Type (max u (v + 1))

The category of commutative R-bialgebras and their morphisms.

• carrier : Type v

  The underlying type.

• commRing : CommRing ↑self
• bialgebra : Bialgebra R ↑self

instance CommBialgCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (CommBialgCat R) (Type v)

Equations

• CommBialgCat.instCoeSortType = { coe := CommBialgCat.carrier }

@[reducible, inline]

abbrev CommBialgCat.of (R : Type u) [CommRing R] (X : Type v) [CommRing X] [Bialgebra R X] : CommBialgCat R

Turn an unbundled R-bialgebra into the corresponding object in the category of R-bialgebras.

This is the preferred way to construct a term of CommBialgCat R.

Equations

• CommBialgCat.of R X = { carrier := X, commRing := inst✝¹, bialgebra := inst✝ }

theorem CommBialgCat.coe_of (R : Type u) [CommRing R] (X : Type v) [CommRing X] [Bialgebra R X] : ↑(of R X) = X

structure CommBialgCat.Hom {R : Type u} [CommRing R] (A B : CommBialgCat R) : Type v

The type of morphisms in CommBialgCat R.

• hom' : ↑A →ₐc[R] ↑B

  The underlying bialgebra map.

theorem CommBialgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {A B : CommBialgCat R} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem CommBialgCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {A B : CommBialgCat R} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

instance CommBialgCat.instCategory {R : Type u} [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (CommBialgCat R)

Equations

• One or more equations did not get rendered due to their size.

instance CommBialgCat.instConcreteCategoryBialgHomCarrier {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (CommBialgCat R) fun (x1 x2 : CommBialgCat R) => ↑x1 →ₐc[R] ↑x2

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CommBialgCat.Hom.hom {R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A.Hom B) : ↑A →ₐc[R] ↑B

Turn a morphism in CommBialgCat back into a BialgHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev CommBialgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Bialgebra R X} {x✝³ : Bialgebra R Y} (f : X →ₐc[R] Y) : of R X ⟶ of R Y

Typecheck a BialgHom as a morphism in CommBialgCat R.

Equations

• CommBialgCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def CommBialgCat.Hom.Simps.hom {R : Type u} [CommRing R] (A B : CommBialgCat R) (f : A.Hom B) : ↑A →ₐc[R] ↑B

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• CommBialgCat.Hom.Simps.hom A B f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem CommBialgCat.hom_id {R : Type u} [CommRing R] {A : CommBialgCat R} : ↑(Hom.hom (CategoryTheory.CategoryStruct.id A)) = AlgHom.id R ↑A

@[simp]

theorem CommBialgCat.hom_comp {R : Type u} [CommRing R] {A B C : CommBialgCat R} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem CommBialgCat.id_apply {R : Type u} [CommRing R] (A : CommBialgCat R) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

theorem CommBialgCat.comp_apply {R : Type u} [CommRing R] {A B C : CommBialgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

theorem CommBialgCat.hom_ext {R : Type u} [CommRing R] {A B : CommBialgCat R} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem CommBialgCat.hom_ext_iff {R : Type u} [CommRing R] {A B : CommBialgCat R} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem CommBialgCat.hom_ofHom {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] (f : X →ₐc[R] Y) : Hom.hom (ofHom f) = f

@[simp]

theorem CommBialgCat.ofHom_hom {R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem CommBialgCat.ofHom_id {R : Type u} [CommRing R] {X : Type v} [CommRing X] [Bialgebra R X] : ofHom (BialgHom.id R X) = CategoryTheory.CategoryStruct.id (of R X)

@[simp]

theorem CommBialgCat.ofHom_comp {R : Type u} [CommRing R] {X Y Z : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] [CommRing Z] [Bialgebra R Z] (f : X →ₐc[R] Y) (g : Y →ₐc[R] Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem CommBialgCat.ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] (f : X →ₐc[R] Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem CommBialgCat.inv_hom_apply {R : Type u} [CommRing R] {A B : CommBialgCat R} (e : A ≅ B) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem CommBialgCat.hom_inv_apply {R : Type u} [CommRing R] {A B : CommBialgCat R} (e : A ≅ B) (x : ↑B) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x

instance CommBialgCat.instInhabited {R : Type u} [CommRing R] : Inhabited (CommBialgCat R)

Equations

• CommBialgCat.instInhabited = { default := CommBialgCat.of R R }

theorem CommBialgCat.forget_obj {R : Type u} [CommRing R] (A : CommBialgCat R) : (CategoryTheory.forget (CommBialgCat R)).obj A = ↑A

theorem CommBialgCat.forget_map {R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : (CategoryTheory.forget (CommBialgCat R)).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

instance CommBialgCat.instCommRingObjForget {R : Type u} [CommRing R] {A : CommBialgCat R} : CommRing ((CategoryTheory.forget (CommBialgCat R)).obj A)

Equations

• CommBialgCat.instCommRingObjForget = inferInstanceAs (CommRing ↑A)

instance CommBialgCat.instBialgebraObjForget {R : Type u} [CommRing R] {A : CommBialgCat R} : Bialgebra R ((CategoryTheory.forget (CommBialgCat R)).obj A)

Equations

• CommBialgCat.instBialgebraObjForget = inferInstanceAs (Bialgebra R ↑A)

instance CommBialgCat.hasForgetToCommAlgCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CommBialgCat R) (CommAlgCat R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommBialgCat.forget₂_commAlgCat_obj {R : Type u} [CommRing R] (A : CommBialgCat R) : (CategoryTheory.forget₂ (CommBialgCat R) (CommAlgCat R)).obj A = CommAlgCat.of R ↑A

@[simp]

theorem CommBialgCat.forget₂_commAlgCat_map {R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : (CategoryTheory.forget₂ (CommBialgCat R) (CommAlgCat R)).map f = CommAlgCat.ofHom ↑(Hom.hom f)

def CommBialgCat.ofSelfIso {R : Type u} [CommRing R] (M : CommBialgCat R) : of R ↑M ≅ M

Forgetting to the underlying type and then building the bundled object returns the original bialgebra.

Equations

• M.ofSelfIso = { hom := CategoryTheory.CategoryStruct.id M, inv := CategoryTheory.CategoryStruct.id M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CommBialgCat.ofSelfIso_inv {R : Type u} [CommRing R] (M : CommBialgCat R) : M.ofSelfIso.inv = CategoryTheory.CategoryStruct.id M

@[simp]

theorem CommBialgCat.ofSelfIso_hom {R : Type u} [CommRing R] (M : CommBialgCat R) : M.ofSelfIso.hom = CategoryTheory.CategoryStruct.id M

def CommBialgCat.isoMk {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Bialgebra R X} {x✝³ : Bialgebra R Y} (e : X ≃ₐc[R] Y) : of R X ≅ of R Y

Build an isomorphism in the category CommBialgCat R from a BialgEquiv between Bialgebras.

Equations

• CommBialgCat.isoMk e = { hom := CommBialgCat.ofHom ↑e, inv := CommBialgCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CommBialgCat.isoMk_inv {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Bialgebra R X} {x✝³ : Bialgebra R Y} (e : X ≃ₐc[R] Y) : (isoMk e).inv = ofHom ↑e.symm

@[simp]

theorem CommBialgCat.isoMk_hom {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Bialgebra R X} {x✝³ : Bialgebra R Y} (e : X ≃ₐc[R] Y) : (isoMk e).hom = ofHom ↑e

def CommBialgCat.bialgEquivOfIso {R : Type u} [CommRing R] {A B : CommBialgCat R} (i : A ≅ B) : ↑A ≃ₐc[R] ↑B

Build a BialgEquiv from an isomorphism in the category CommBialgCat R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommBialgCat.bialgEquivOfIso_apply {R : Type u} [CommRing R] {A B : CommBialgCat R} (i : A ≅ B) (a : ↑A) : (bialgEquivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

theorem CommBialgCat.bialgEquivOfIso_symm_apply {R : Type u} [CommRing R] {A B : CommBialgCat R} (i : A ≅ B) (a : ↑B) : (bialgEquivOfIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a

def CommBialgCat.isoEquivBialgEquiv {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] : (of R X ≅ of R Y) ≃ X ≃ₐc[R] Y

Bialgebra equivalences between Bialgebras are the same as isomorphisms in CommBialgCat.

Equations

• CommBialgCat.isoEquivBialgEquiv = { toFun := CommBialgCat.bialgEquivOfIso, invFun := CommBialgCat.isoMk, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CommBialgCat.isoEquivBialgEquiv_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] (i : of R X ≅ of R Y) : isoEquivBialgEquiv i = bialgEquivOfIso i

@[simp]

theorem CommBialgCat.isoEquivBialgEquiv_symm_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Bialgebra R X] [CommRing Y] [Bialgebra R Y] (e : X ≃ₐc[R] Y) : isoEquivBialgEquiv.symm e = isoMk e

instance CommBialgCat.reflectsIsomorphisms_forget {R : Type u} [CommRing R] : (CategoryTheory.forget (CommBialgCat R)).ReflectsIsomorphisms

instance CommAlgCat.mon_ClassOpOf {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Bialgebra R A] : Mon_Class (Opposite.op (of R A))

Equations

• CommAlgCat.mon_ClassOpOf = { one := (CommAlgCat.ofHom (Bialgebra.counitAlgHom R A)).op, mul := (CommAlgCat.ofHom (Bialgebra.comulAlgHom R A)).op, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem CommAlgCat.one_op_of_unop_hom {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Bialgebra R A] : Hom.hom Mon_Class.one.unop = Bialgebra.counitAlgHom R A

@[simp]

theorem CommAlgCat.mul_op_of_unop_hom {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Bialgebra R A] : Hom.hom Mon_Class.mul.unop = Bialgebra.comulAlgHom R A

instance instIsCommMonOppositeCommAlgCatOpOfOfIsCocomm {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Bialgebra R A] [Coalgebra.IsCocomm R A] : IsCommMon (Opposite.op (CommAlgCat.of R A))

instance instIsMon_HomOppositeCommAlgCatOpOfHomToAlgHomBialgHom {R : Type u} [CommRing R] {A B : Type u} [CommRing A] [Bialgebra R A] [CommRing B] [Bialgebra R B] (f : A →ₐc[R] B) : IsMon_Hom (CommAlgCat.ofHom ↑f).op

instance instBialgebraCarrierUnopCommAlgCatOfMon_ClassOpposite {R : Type u} [CommRing R] (A : (CommAlgCat R)ᵒᵖ) [Mon_Class A] : Bialgebra R ↑(Opposite.unop A)

Equations

• instBialgebraCarrierUnopCommAlgCatOfMon_ClassOpposite A = Bialgebra.ofAlgHom (CommAlgCat.Hom.hom Mon_Class.mul.unop) (CommAlgCat.Hom.hom Mon_Class.one.unop) ⋯ ⋯ ⋯

def commBialgCatEquivComonCommAlgCat (R : Type u) [CommRing R] : CommBialgCat R ≌ (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ

Commutative bialgebras over a commutative ring R are the same thing as comonoid R-algebras.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem commBialgCatEquivComonCommAlgCat_unitIso_hom_app (R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem commBialgCatEquivComonCommAlgCat_inverse_obj (R : Type u) [CommRing R] (A : (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).inverse.obj A = CommBialgCat.of R ↑(Opposite.unop (Opposite.unop A).X)

@[simp]

theorem commBialgCatEquivComonCommAlgCat_functor_obj_unop_X (R : Type u) [CommRing R] (A : CommBialgCat R) : (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X = Opposite.op (CommAlgCat.of R ↑A)

@[simp]

theorem commBialgCatEquivComonCommAlgCat_counitIso_inv_app (R : Type u) [CommRing R] (X : (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem commBialgCatEquivComonCommAlgCat_unitIso_inv_app (R : Type u) [CommRing R] (X : CommBialgCat R) : (commBialgCatEquivComonCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id (CommBialgCat.of R ↑X)

@[simp]

theorem commBialgCatEquivComonCommAlgCat_counitIso_hom_app (R : Type u) [CommRing R] (X : (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ) : (commBialgCatEquivComonCommAlgCat R).counitIso.hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), mon := CommAlgCat.mon_ClassOpOf })

@[simp]

theorem commBialgCatEquivComonCommAlgCat_functor_map_unop_hom {R : Type u} [CommRing R] {A B : CommBialgCat R} (f : A ⟶ B) : ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom = (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op

@[simp]

theorem commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom {R : Type u} [CommRing R] {A B : (Mon_ (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B) : ↑(CommBialgCat.Hom.hom ((commBialgCatEquivComonCommAlgCat R).inverse.map f)) = CommAlgCat.Hom.hom f.unop.hom.unop

instance instIsCommMonOppositeCommAlgCatXUnopMon_ObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier {R : Type u} [CommRing R] {A : CommBialgCat R} [Coalgebra.IsCocomm R ↑A] : IsCommMon (Opposite.unop ((commBialgCatEquivComonCommAlgCat R).functor.obj A)).X