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 in #11975.

Implementation notes #

We make the definiton 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 in #11976 to have better definitional equalities.

source
@[simp]
theorem CoalgebraCat.toComonObj_counit {R : Type u} [CommRing R] (X : CoalgebraCat R) :
X.toComonObj.counit = ModuleCat.ofHom Coalgebra.counit
source
@[simp]
theorem CoalgebraCat.toComonObj_comul {R : Type u} [CommRing R] (X : CoalgebraCat R) :
X.toComonObj.comul = ModuleCat.ofHom Coalgebra.comul
source
@[simp]
theorem CoalgebraCat.toComonObj_X {R : Type u} [CommRing R] (X : CoalgebraCat R) :
X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat
source
def CoalgebraCat.toComonObj {R : Type u} [CommRing R] (X : CoalgebraCat R) :
Comon_ (ModuleCat R)

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
    source
    @[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.ofHom ↑f.toCoalgHom
    source
    @[simp]
    theorem CoalgebraCat.toComon_obj (R : Type u) [CommRing R] (X : CoalgebraCat R) :
    (CoalgebraCat.toComon R).obj X = X.toComonObj
    source
    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
      source
      @[simp]
      theorem CoalgebraCat.ofComonObjCoalgebraStruct_comul {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      Coalgebra.comul = X.comul
      source
      @[simp]
      theorem CoalgebraCat.ofComonObjCoalgebraStruct_counit {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      Coalgebra.counit = X.counit
      source
      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
      source
      def CoalgebraCat.ofComonObj {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      CoalgebraCat R

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

      Equations
      Instances For
        source
        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
          source
          @[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)) ⋯
          source
          @[simp]
          theorem CoalgebraCat.comonEquivalence_functor (R : Type u) [CommRing R] :
          (CoalgebraCat.comonEquivalence R).functor = CoalgebraCat.toComon R
          source
          @[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)) ⋯
          source
          @[simp]
          theorem CoalgebraCat.comonEquivalence_inverse (R : Type u) [CommRing R] :
          (CoalgebraCat.comonEquivalence R).inverse = CoalgebraCat.ofComon R
          source
          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
            source
            noncomputable def CoalgebraCat.instMonoidalCategoryAux {R : Type u} [CommRing R] :
            CategoryTheory.MonoidalCategory (CoalgebraCat 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.CoalgebraCat.Monoidal in #11976 will have better definitional equalities.

            Equations
            Instances For
              source
              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
              source
              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
              source
              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)
              source
              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)
              source
              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)
              source
              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
              source
              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
              source
              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
              source
              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
              source
              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
              source
              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