Documentation

Mathlib.CategoryTheory.Monad.Algebra

Eilenberg-Moore (co)algebras for a (co)monad #

This file defines Eilenberg-Moore (co)algebras for a (co)monad, and provides the category instance for them.

Further it defines the adjoint pair of free and forgetful functors, respectively from and to the original category, as well as the adjoint pair of forgetful and cofree functors, respectively from and to the original category.

References #

An Eilenberg-Moore algebra for a monad T. cf Definition 5.2.3 in [Riehl][riehl2017].

Instances For

    The unit axiom associated to an algebra.

    The associativity axiom associated to an algebra.

    theorem CategoryTheory.Monad.Algebra.Hom.ext_iff {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra} (x y : A.Hom B), x = y x.f = y.f
    theorem CategoryTheory.Monad.Algebra.Hom.ext {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra} (x y : A.Hom B), x.f = y.fx = y
    structure CategoryTheory.Monad.Algebra.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra) (B : T.Algebra) :
    Type v₁

    A morphism of Eilenberg–Moore algebras for the monad T.

    Instances For
      @[simp]
      theorem CategoryTheory.Monad.Algebra.Hom.h {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (self : A.Hom B) :

      Compatibility with the structure morphism, for a morphism of algebras.

      The identity homomorphism for an Eilenberg–Moore algebra.

      Equations
      Instances For
        def CategoryTheory.Monad.Algebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {P : T.Algebra} {Q : T.Algebra} {R : T.Algebra} (f : P.Hom Q) (g : Q.Hom R) :
        P.Hom R

        Composition of Eilenberg–Moore algebra homomorphisms.

        Equations
        Instances For
          theorem CategoryTheory.Monad.Algebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (Y : T.Algebra) (f : X Y) (g : X Y) (h : f.f = g.f) :
          f = g
          @[simp]
          theorem CategoryTheory.Monad.Algebra.comp_eq_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {A' : T.Algebra} {A'' : T.Algebra} (f : A A') (g : A' A'') :
          @[simp]
          theorem CategoryTheory.Monad.Algebra.comp_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {A' : T.Algebra} {A'' : T.Algebra} (f : A A') (g : A' A'') :

          The category of Eilenberg-Moore algebras for a monad. cf Definition 5.2.4 in [Riehl][riehl2017].

          Equations
          def CategoryTheory.Monad.Algebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (h : A.A B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom) _auto✝) :
          A B

          To construct an isomorphism of algebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Monad.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (A : T.Algebra) :
            T.forget.obj A = A.A
            @[simp]
            theorem CategoryTheory.Monad.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) :
            ∀ {X Y : T.Algebra} (f : X Y), T.forget.map f = f.f

            The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure.

            Equations
            • T.forget = { obj := fun (A : T.Algebra) => A.A, map := fun {X Y : T.Algebra} (f : X Y) => f.f, map_id := , map_comp := }
            Instances For
              @[simp]
              theorem CategoryTheory.Monad.free_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) :
              (T.free.obj X).a = T.app X
              @[simp]
              theorem CategoryTheory.Monad.free_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) :
              ∀ {X Y : C} (f : X Y), (T.free.map f).f = T.map f
              @[simp]
              theorem CategoryTheory.Monad.free_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) :
              (T.free.obj X).A = T.obj X

              The free functor from the Eilenberg-Moore category, constructing an algebra for any object.

              Equations
              • T.free = { obj := fun (X : C) => { A := T.obj X, a := T.app X, unit := , assoc := }, map := fun {X Y : C} (f : X Y) => { f := T.map f, h := }, map_id := , map_comp := }
              Instances For
                Equations
                • T.instInhabitedAlgebra = { default := T.free.obj default }
                @[simp]
                theorem CategoryTheory.Monad.adj_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) :
                T.adj.unit = { app := fun (X : C) => T.app X, naturality := }
                @[simp]
                theorem CategoryTheory.Monad.adj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) :
                T.adj.counit = { app := fun (Y : T.Algebra) => { f := Y.a, h := }, naturality := }

                The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for a monad. cf Lemma 5.2.8 of [Riehl][riehl2017].

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

                  Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.

                  Equations
                  • =
                  Equations
                  • =
                  theorem CategoryTheory.Monad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X : T.Algebra} {Y : T.Algebra} (f : X Y) [h : CategoryTheory.Epi f.f] :

                  Given an algebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.

                  Given an algebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.

                  @[simp]
                  theorem CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₂ T₁) :
                  ∀ {X Y : T₁.Algebra} (f : X Y), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f

                  Given a monad morphism from T₂ to T₁, we get a functor from the algebras of T₁ to algebras of T₂.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra) :
                    (CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom
                    @[simp]
                    theorem CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra) :
                    (CategoryTheory.Monad.algebraFunctorOfMonadHomId.inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).inv

                    The identity monad morphism induces the identity functor from the category of algebras to itself.

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

                      A composition of monad morphisms gives the composition of corresponding functors.

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

                        If f and g are two equal morphisms of monads, then the functors of algebras induced by them are isomorphic. We define it like this as opposed to using eqToIso so that the components are nicer to prove lemmas about.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def CategoryTheory.Monad.algebraEquivOfIsoMonads {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ T₂) :
                          T₁.Algebra T₂.Algebra

                          Isomorphic monads give equivalent categories of algebras. Furthermore, they are equivalent as categories over C, that is, we have algebraEquivOfIsoMonads hforget = forget.

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

                            An Eilenberg-Moore coalgebra for a comonad T.

                            Instances For

                              The counit axiom associated to a coalgebra.

                              The coassociativity axiom associated to a coalgebra.

                              theorem CategoryTheory.Comonad.Coalgebra.Hom.ext_iff {C : Type u₁} :
                              ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (x y : A.Hom B), x = y x.f = y.f
                              theorem CategoryTheory.Comonad.Coalgebra.Hom.ext {C : Type u₁} :
                              ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (x y : A.Hom B), x.f = y.fx = y
                              structure CategoryTheory.Comonad.Coalgebra.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : G.Coalgebra) (B : G.Coalgebra) :
                              Type v₁

                              A morphism of Eilenberg-Moore coalgebras for the comonad G.

                              Instances For
                                @[simp]
                                theorem CategoryTheory.Comonad.Coalgebra.Hom.h {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (self : A.Hom B) :

                                Compatibility with the structure morphism, for a morphism of coalgebras.

                                The identity homomorphism for an Eilenberg–Moore coalgebra.

                                Equations
                                Instances For
                                  def CategoryTheory.Comonad.Coalgebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {P : G.Coalgebra} {Q : G.Coalgebra} {R : G.Coalgebra} (f : P.Hom Q) (g : Q.Hom R) :
                                  P.Hom R

                                  Composition of Eilenberg–Moore coalgebra homomorphisms.

                                  Equations
                                  Instances For

                                    The category of Eilenberg-Moore coalgebras for a comonad.

                                    Equations
                                    theorem CategoryTheory.Comonad.Coalgebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X : G.Coalgebra) (Y : G.Coalgebra) (f : X Y) (g : X Y) (h : f.f = g.f) :
                                    f = g
                                    @[simp]
                                    theorem CategoryTheory.Comonad.Coalgebra.comp_eq_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {A' : G.Coalgebra} {A'' : G.Coalgebra} (f : A A') (g : A' A'') :
                                    @[simp]
                                    theorem CategoryTheory.Comonad.Coalgebra.comp_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {A' : G.Coalgebra} {A'' : G.Coalgebra} (f : A A') (g : A' A'') :

                                    The category of Eilenberg-Moore coalgebras for a comonad.

                                    Equations
                                    def CategoryTheory.Comonad.Coalgebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (h : A.A B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a) _auto✝) :
                                    A B

                                    To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Comonad.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) :
                                      ∀ {X Y : G.Coalgebra} (f : X Y), G.forget.map f = f.f
                                      @[simp]
                                      theorem CategoryTheory.Comonad.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (A : G.Coalgebra) :
                                      G.forget.obj A = A.A

                                      The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic structure.

                                      Equations
                                      • G.forget = { obj := fun (A : G.Coalgebra) => A.A, map := fun {X Y : G.Coalgebra} (f : X Y) => f.f, map_id := , map_comp := }
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Comonad.cofree_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) :
                                        ∀ {X Y : C} (f : X Y), (G.cofree.map f).f = G.map f
                                        @[simp]
                                        theorem CategoryTheory.Comonad.cofree_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) :
                                        (G.cofree.obj X).A = G.obj X
                                        @[simp]
                                        theorem CategoryTheory.Comonad.cofree_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) :
                                        (G.cofree.obj X).a = G.app X

                                        The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object.

                                        Equations
                                        • G.cofree = { obj := fun (X : C) => { A := G.obj X, a := G.app X, counit := , coassoc := }, map := fun {X Y : C} (f : X Y) => { f := G.map f, h := }, map_id := , map_comp := }
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Comonad.adj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) :
                                          G.adj.counit = { app := fun (Y : C) => G.app Y, naturality := }
                                          @[simp]
                                          theorem CategoryTheory.Comonad.adj_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) :
                                          G.adj.unit = { app := fun (X : G.Coalgebra) => { f := X.a, h := }, naturality := }

                                          The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras for a comonad.

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

                                            Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalgebra isomorphism.

                                            Equations
                                            • =
                                            theorem CategoryTheory.Comonad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X : G.Coalgebra} {Y : G.Coalgebra} (f : X Y) [h : CategoryTheory.Epi f.f] :

                                            Given a coalgebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.

                                            Given a coalgebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.