The category equivalence between R-coalgebras and comonoid objects in R-Mod

Given a commutative ring R, this file defines the equivalence of categories between R-coalgebras and comonoid objects in the category of R-modules.

We then use this to set up boilerplate for the Coalgebra instance on a tensor product of coalgebras defined in Mathlib/RingTheory/Coalgebra/TensorProduct.lean.

Implementation notes

We make the definition CoalgCat.instMonoidalCategoryAux in this file, which is the monoidal structure on CoalgCat induced by the equivalence with Comon(R-Mod). We use this to show the comultiplication and counit on a tensor product of coalgebras satisfy the coalgebra axioms, but our actual MonoidalCategory instance on CoalgCat is constructed in Mathlib/Algebra/Category/CoalgCat/Monoidal.lean to have better definitional equalities.

noncomputable instance CoalgCat.instComonObjModuleCatOfCarrier {R : Type u} [CommRing R] (X : CoalgCat R) : ComonObj (ModuleCat.of R ↑X.toModuleCat)

Equations

• X.instComonObjModuleCatOfCarrier = { counit := ModuleCat.ofHom CoalgebraStruct.counit, comul := ModuleCat.ofHom CoalgebraStruct.comul, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }

@[simp]

theorem CoalgCat.counit_def {R : Type u} [CommRing R] (X : CoalgCat R) : ComonObj.counit = ModuleCat.ofHom CoalgebraStruct.counit

@[simp]

theorem CoalgCat.comul_def {R : Type u} [CommRing R] (X : CoalgCat R) : ComonObj.comul = ModuleCat.ofHom CoalgebraStruct.comul

noncomputable def CoalgCat.toComonObj {R : Type u} [CommRing R] (X : CoalgCat R) : Comon (ModuleCat R)

An R-coalgebra is a comonoid object in the category of R-modules.

Equations

• X.toComonObj = { X := ModuleCat.of R ↑X.toModuleCat, comon := X.instComonObjModuleCatOfCarrier }

@[simp]

theorem CoalgCat.toComonObj_X {R : Type u} [CommRing R] (X : CoalgCat R) : X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat

noncomputable def CoalgCat.toComon (R : Type u) [CommRing R] : CategoryTheory.Functor (CoalgCat R) (Comon (ModuleCat R))

The natural functor from R-coalgebras to comonoid objects in the category of R-modules.

Equations

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

@[simp]

theorem CoalgCat.toComon_obj (R : Type u) [CommRing R] (X : CoalgCat R) : (toComon R).obj X = X.toComonObj

@[simp]

theorem CoalgCat.toComon_map_hom (R : Type u) [CommRing R] {X✝ Y✝ : CoalgCat R} (f : X✝ ⟶ Y✝) : ((toComon R).map f).hom = ModuleCat.ofHom ↑f.toCoalgHom'

noncomputable instance CoalgCat.ofComonObjCoalgebraStruct {R : Type u} [CommRing R] (X : ModuleCat R) [ComonObj X] : CoalgebraStruct R ↑X

A comonoid object in the category of R-modules has a natural comultiplication and counit.

Equations

• CoalgCat.ofComonObjCoalgebraStruct X = { comul := ModuleCat.Hom.hom ComonObj.comul, counit := ModuleCat.Hom.hom ComonObj.counit }

@[simp]

theorem CoalgCat.ofComonObjCoalgebraStruct_counit {R : Type u} [CommRing R] (X : ModuleCat R) [ComonObj X] : CoalgebraStruct.counit = ModuleCat.Hom.hom ComonObj.counit

@[simp]

theorem CoalgCat.ofComonObjCoalgebraStruct_comul {R : Type u} [CommRing R] (X : ModuleCat R) [ComonObj X] : CoalgebraStruct.comul = ModuleCat.Hom.hom ComonObj.comul

noncomputable def CoalgCat.ofComonObj {R : Type u} [CommRing R] (X : ModuleCat R) [ComonObj X] : CoalgCat R

A comonoid object in the category of R-modules has a natural R-coalgebra structure.

Equations

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

noncomputable def CoalgCat.ofComon (R : Type u) [CommRing R] : CategoryTheory.Functor (Comon (ModuleCat R)) (CoalgCat R)

The natural functor from comonoid objects in the category of R-modules to R-coalgebras.

Equations

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

noncomputable def CoalgCat.comonEquivalence (R : Type u) [CommRing R] : CoalgCat R ≌ Comon (ModuleCat R)

The natural category equivalence between R-coalgebras and comonoid objects in the category of R-modules.

Equations

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

@[simp]

theorem CoalgCat.comonEquivalence_unitIso (R : Type u) [CommRing R] : (comonEquivalence R).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : CoalgCat R) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgCat R)).obj x)) ⋯

@[simp]

theorem CoalgCat.comonEquivalence_functor (R : Type u) [CommRing R] : (comonEquivalence R).functor = toComon R

@[simp]

theorem CoalgCat.comonEquivalence_counitIso (R : Type u) [CommRing R] : (comonEquivalence R).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : Comon (ModuleCat R)) => CategoryTheory.Iso.refl (((ofComon R).comp (toComon R)).obj x)) ⋯

@[simp]

theorem CoalgCat.comonEquivalence_inverse (R : Type u) [CommRing R] : (comonEquivalence R).inverse = ofComon R

noncomputable def CoalgCat.instMonoidalCategoryAux {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategory (CoalgCat R)

The monoidal category structure on the category of R-coalgebras induced by the equivalence with Comon(R-Mod). This is just an auxiliary definition; the MonoidalCategory instance we make in Mathlib/Algebra/Category/CoalgCat/Monoidal.lean has better definitional equalities.

Equations

• CoalgCat.instMonoidalCategoryAux = CategoryTheory.Monoidal.transport (CoalgCat.comonEquivalence R).symm

theorem CoalgCat.MonoidalCategoryAux.tensorObj_comul {R : Type u} [CommRing R] (K L : CoalgCat R) : CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

theorem CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap {R : Type u} [CommRing R] {M N P Q : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : (CategoryTheory.MonoidalCategoryStruct.tensorHom (ofHom f) (ofHom g)).toCoalgHom'.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap

theorem CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : (CategoryTheory.MonoidalCategoryStruct.associator (of R M) (of R N) (of R P)).hom.toCoalgHom'.toLinearMap = ↑(TensorProduct.assoc R M N P)

theorem CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap {R : Type u} [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] [Coalgebra R M] : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (of R M)).hom.toCoalgHom'.toLinearMap = ↑(TensorProduct.lid R M)

theorem CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap {R : Type u} [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] [Coalgebra R M] : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (of R M)).hom.toCoalgHom'.toLinearMap = ↑(TensorProduct.rid R M)

theorem CoalgCat.MonoidalCategoryAux.comul_tensorObj {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Coalgebra R M] [Coalgebra R N] : CoalgebraStruct.comul = CoalgebraStruct.comul

theorem CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : CoalgebraStruct.comul = CoalgebraStruct.comul

theorem CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : CoalgebraStruct.comul = CoalgebraStruct.comul

theorem CoalgCat.MonoidalCategoryAux.counit_tensorObj {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Coalgebra R M] [Coalgebra R N] : CoalgebraStruct.counit = CoalgebraStruct.counit

theorem CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : CoalgebraStruct.counit = CoalgebraStruct.counit

theorem CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] : CoalgebraStruct.counit = CoalgebraStruct.counit