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

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

    Instances For

      The identity homomorphism for an Eilenberg–Moore algebra.

      Instances For

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

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

        Instances For

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

          Instances For
            @[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), ((CategoryTheory.Monad.free T).map f).f = T.map f

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

            Instances For

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

              Instances For

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

                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.

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

                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.

                  Instances For

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

                    Instances For

                      An Eilenberg-Moore coalgebra for a comonad T.

                      Instances For

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

                        Instances For

                          The identity homomorphism for an Eilenberg–Moore coalgebra.

                          Instances For

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

                            Instances For

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

                              Instances For
                                @[simp]

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

                                Instances For

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

                                  Instances For

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

                                    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.