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.
Implementation notes #
We make the definition CoalgebraCat.instMonoidalCategoryAux in this file, which is the
monoidal structure on CoalgebraCat 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 CoalgebraCat is
constructed in Mathlib.Algebra.Category.CoalgebraCat.Monoidal to have better
definitional equalities.
An R-coalgebra is a comonoid object in the category of R-modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CoalgebraCat.toComonObj_counit
{R : Type u}
[CommRing R]
(X : CoalgebraCat R)
:
X.toComonObj.counit = ModuleCat.asHom Coalgebra.counit
@[simp]
theorem
CoalgebraCat.toComonObj_X
{R : Type u}
[CommRing R]
(X : CoalgebraCat R)
:
X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat
@[simp]
theorem
CoalgebraCat.toComonObj_comul
{R : Type u}
[CommRing R]
(X : CoalgebraCat R)
:
X.toComonObj.comul = ModuleCat.asHom Coalgebra.comul
def
CoalgebraCat.toComon
(R : Type u)
[CommRing R]
:
CategoryTheory.Functor (CoalgebraCat 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.
Instances For
@[simp]
theorem
CoalgebraCat.toComon_obj
(R : Type u)
[CommRing R]
(X : CoalgebraCat R)
:
(CoalgebraCat.toComon R).obj X = X.toComonObj
@[simp]
theorem
CoalgebraCat.toComon_map_hom
(R : Type u)
[CommRing R]
:
∀ {X Y : CoalgebraCat R} (f : X ⟶ Y), ((CoalgebraCat.toComon R).map f).hom = ModuleCat.asHom ↑f.toCoalgHom
instance
CoalgebraCat.ofComonObjCoalgebraStruct
{R : Type u}
[CommRing R]
(X : Comon_ (ModuleCat R))
:
CoalgebraStruct R ↑X.X
A comonoid object in the category of R-modules has a natural comultiplication
and counit.
Equations
- CoalgebraCat.ofComonObjCoalgebraStruct X = { comul := X.comul, counit := X.counit }
A comonoid object in the category of R-modules has a natural R-coalgebra
structure.
Equations
- CoalgebraCat.ofComonObj X = { toModuleCat := ModuleCat.mk ↑X.X, instCoalgebra := let __src := CoalgebraCat.ofComonObjCoalgebraStruct X; Coalgebra.mk ⋯ ⋯ ⋯ }
Instances For
def
CoalgebraCat.ofComon
(R : Type u)
[CommRing R]
:
CategoryTheory.Functor (Comon_ (ModuleCat R)) (CoalgebraCat 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.
Instances For
noncomputable def
CoalgebraCat.comonEquivalence
(R : Type u)
[CommRing R]
:
CoalgebraCat 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.
Instances For
@[simp]
theorem
CoalgebraCat.comonEquivalence_unitIso
(R : Type u)
[CommRing R]
:
(CoalgebraCat.comonEquivalence R).unitIso = CategoryTheory.NatIso.ofComponents
(fun (x : CoalgebraCat R) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgebraCat R)).obj x)) ⋯
@[simp]
theorem
CoalgebraCat.comonEquivalence_functor
(R : Type u)
[CommRing R]
:
(CoalgebraCat.comonEquivalence R).functor = CoalgebraCat.toComon R
@[simp]
theorem
CoalgebraCat.comonEquivalence_inverse
(R : Type u)
[CommRing R]
:
(CoalgebraCat.comonEquivalence R).inverse = CoalgebraCat.ofComon R
@[simp]
theorem
CoalgebraCat.comonEquivalence_counitIso
(R : Type u)
[CommRing R]
:
(CoalgebraCat.comonEquivalence R).counitIso = CategoryTheory.NatIso.ofComponents
(fun (x : Comon_ (ModuleCat R)) =>
CategoryTheory.Iso.refl (((CoalgebraCat.ofComon R).comp (CoalgebraCat.toComon R)).obj x))
⋯
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.CoalgebraCat.Monoidal has better
definitional equalities.
Equations
- CoalgebraCat.instMonoidalCategoryAux = CategoryTheory.Monoidal.transport (CoalgebraCat.comonEquivalence R).symm
Instances For
theorem
CoalgebraCat.MonoidalCategoryAux.tensorObj_comul
{R : Type u}
[CommRing R]
(K : CoalgebraCat R)
(L : CoalgebraCat R)
:
Coalgebra.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
TensorProduct.map Coalgebra.comul Coalgebra.comul
theorem
CoalgebraCat.MonoidalCategoryAux.tensorHom_toLinearMap
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{P : Type u}
{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.MonoidalCategory.tensorHom (CoalgebraCat.ofHom f) (CoalgebraCat.ofHom g)).toCoalgHom.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
theorem
CoalgebraCat.MonoidalCategoryAux.associator_hom_toLinearMap
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{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.MonoidalCategory.associator (CoalgebraCat.of R M) (CoalgebraCat.of R N)
(CoalgebraCat.of R P)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.assoc R M N P)
theorem
CoalgebraCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap
{R : Type u}
[CommRing R]
{M : Type u}
[AddCommGroup M]
[Module R M]
[Coalgebra R M]
:
(CategoryTheory.MonoidalCategory.leftUnitor (CoalgebraCat.of R M)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.lid R M)
theorem
CoalgebraCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap
{R : Type u}
[CommRing R]
{M : Type u}
[AddCommGroup M]
[Module R M]
[Coalgebra R M]
:
(CategoryTheory.MonoidalCategory.rightUnitor (CoalgebraCat.of R M)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.rid R M)
theorem
CoalgebraCat.MonoidalCategoryAux.comul_tensorObj
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[Coalgebra R M]
[Coalgebra R N]
:
Coalgebra.comul = Coalgebra.comul
theorem
CoalgebraCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{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]
:
Coalgebra.comul = Coalgebra.comul
theorem
CoalgebraCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{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]
:
Coalgebra.comul = Coalgebra.comul
theorem
CoalgebraCat.MonoidalCategoryAux.counit_tensorObj
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[Coalgebra R M]
[Coalgebra R N]
:
Coalgebra.counit = Coalgebra.counit
theorem
CoalgebraCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{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]
:
Coalgebra.counit = Coalgebra.counit
theorem
CoalgebraCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left
{R : Type u}
[CommRing R]
{M : Type u}
{N : Type u}
{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]
:
Coalgebra.counit = Coalgebra.counit