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.

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.toComonObj_counit {R : Type u} [CommRing R] (X : CoalgebraCat R) :
    X.toComonObj.counit = ModuleCat.ofHom CoalgebraStruct.counit
    source
    @[simp]
    theorem CoalgebraCat.toComonObj_X {R : Type u} [CommRing R] (X : CoalgebraCat R) :
    X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat
    source
    @[simp]
    theorem CoalgebraCat.toComonObj_comul {R : Type u} [CommRing R] (X : CoalgebraCat R) :
    X.toComonObj.comul = ModuleCat.ofHom CoalgebraStruct.comul
    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.toComon_obj (R : Type u) [CommRing R] (X : CoalgebraCat R) :
      (toComon R).obj X = X.toComonObj
      source
      @[simp]
      theorem CoalgebraCat.toComon_map_hom (R : Type u) [CommRing R] {X✝ Y✝ : CoalgebraCat R} (f : X✝ ⟶ Y✝) :
      ((toComon R).map f).hom = ModuleCat.ofHom ↑f.toCoalgHom'
      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
      @[simp]
      theorem CoalgebraCat.ofComonObjCoalgebraStruct_comul {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      CoalgebraStruct.comul = ModuleCat.Hom.hom X.comul
      source
      @[simp]
      theorem CoalgebraCat.ofComonObjCoalgebraStruct_counit {R : Type u} [CommRing R] (X : Comon_ (ModuleCat R)) :
      CoalgebraStruct.counit = ModuleCat.Hom.hom X.counit
      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
          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
            @[simp]
            theorem CoalgebraCat.comonEquivalence_unitIso (R : Type u) [CommRing R] :
            (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_functor (R : Type u) [CommRing R] :
            (comonEquivalence R).functor = toComon R
            source
            @[simp]
            theorem CoalgebraCat.comonEquivalence_inverse (R : Type u) [CommRing R] :
            (comonEquivalence R).inverse = ofComon R
            source
            @[simp]
            theorem CoalgebraCat.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)) ⋯
            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 has better definitional equalities.

            Equations
            Instances For
              source
              theorem CoalgebraCat.MonoidalCategoryAux.tensorObj_comul {R : Type u} [CommRing R] (K L : CoalgebraCat R) :
              CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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)
              source
              theorem CoalgebraCat.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)
              source
              theorem CoalgebraCat.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)
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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
              source
              theorem CoalgebraCat.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