Documentation

Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence

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.

@[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

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.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

    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.ofComonObjCoalgebraStruct_counit {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      Coalgebra.counit = X.counit
      @[simp]
      theorem CoalgebraCat.ofComonObjCoalgebraStruct_comul {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      Coalgebra.comul = X.comul

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

      Equations

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

      Equations
      Instances For

        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

          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

            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
            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.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