Documentation

Mathlib.CategoryTheory.Monad.Limits

Limits and colimits in the category of (co)algebras #

This file shows that the forgetful functor forget T : Algebra T ⥤ C for a monad T : C ⥤ C creates limits and creates any colimits which T preserves. This is used to show that Algebra T has any limits which C has, and any colimits which C has and T preserves. This is generalised to the case of a monadic functor D ⥤ C.

Dually, this file shows that the forgetful functor forget T : Coalgebra T ⥤ C for a comonad T : C ⥤ C creates colimits and creates any limits which T preserves. This is used to show that Coalgebra T has any colimits which C has, and any limits which C has and T preserves. This is generalised to the case of a comonadic functor D ⥤ C.

def CategoryTheory.Monad.ForgetCreatesLimits.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) :
D.comp (T.forget.comp T.toFunctor) D.comp T.forget

(Impl) The natural transformation used to define the new cone

Equations
Instances For

    (Impl) This new cone is used to construct the algebra structure

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

      The algebra structure which will be the apex of the new limit cone for D.

      Equations
      Instances For

        (Impl) Construct the lifted cone in Algebra T which will be limiting.

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

          (Impl) Prove that the lifted cone is limiting.

          Equations
          Instances For

            The forgetful functor from the Eilenberg-Moore category creates limits.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem CategoryTheory.Monad.ForgetCreatesColimits.γ_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (j : J) :
            CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a
            def CategoryTheory.Monad.ForgetCreatesColimits.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} :
            (D.comp T.forget).comp T.toFunctor D.comp T.forget

            (Impl) The natural transformation given by the algebra structure maps, used to construct a cocone c with point colimit (D ⋙ forget T).

            Equations
            • CategoryTheory.Monad.ForgetCreatesColimits.γ = { app := fun (j : J) => (D.obj j).a, naturality := }
            Instances For

              (Impl) A cocone for the diagram (D ⋙ forget T) ⋙ T found by composing the natural transformation γ with the colimiting cocone for D ⋙ forget T.

              Equations
              Instances For
                @[reducible, inline]

                (Impl) Define the map λ : TL ⟶ L, which will serve as the structure of the coalgebra on L, and we will show is the colimiting object. We use the cocone constructed by c and the fact that T preserves colimits to produce this morphism.

                Equations
                Instances For

                  (Impl) Construct the colimiting algebra from the map λ : TL ⟶ L given by lambda. We are required to show it satisfies the two algebra laws, which follow from the algebra laws for the image of D and our commuting lemma.

                  Equations
                  Instances For

                    (Impl) Construct the lifted cocone in Algebra T which will be colimiting.

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

                      (Impl) Prove that the lifted cocone is colimiting.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        noncomputable instance CategoryTheory.Monad.forgetCreatesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] :

                        The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Equations
                        • CategoryTheory.Monad.forgetCreatesColimitsOfShape = { CreatesColimit := fun {K : CategoryTheory.Functor J T.Algebra} => inferInstance }

                        For D : J ⥤ Algebra T, D ⋙ forget T has a colimit, then D has a colimit provided colimits of shape J are preserved by T.

                        A monadic functor creates any colimits of shapes it preserves.

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

                          The reflector always preserves terminal objects. Note this in general doesn't apply to any other limit.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def CategoryTheory.Comonad.ForgetCreatesColimits'.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) :
                            D.comp T.forget D.comp (T.forget.comp T.toFunctor)

                            (Impl) The natural transformation used to define the new cocone

                            Equations
                            Instances For

                              (Impl) This new cocone is used to construct the coalgebra structure

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

                                The coalgebra structure which will be the point of the new colimit cone for D.

                                Equations
                                Instances For

                                  (Impl) Construct the lifted cocone in Coalgebra T which will be colimiting.

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

                                    (Impl) Prove that the lifted cocone is colimiting.

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

                                      The forgetful functor from the Eilenberg-Moore category creates colimits.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      @[simp]
                                      theorem CategoryTheory.Comonad.ForgetCreatesLimits'.γ_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (j : J) :
                                      CategoryTheory.Comonad.ForgetCreatesLimits'.γ.app j = (D.obj j).a
                                      def CategoryTheory.Comonad.ForgetCreatesLimits'.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} :
                                      D.comp T.forget (D.comp T.forget).comp T.toFunctor

                                      (Impl) The natural transformation given by the coalgebra structure maps, used to construct a cone c with point limit (D ⋙ forget T).

                                      Equations
                                      • CategoryTheory.Comonad.ForgetCreatesLimits'.γ = { app := fun (j : J) => (D.obj j).a, naturality := }
                                      Instances For

                                        (Impl) A cone for the diagram (D ⋙ forget T) ⋙ T found by composing the natural transformation γ with the limiting cone for D ⋙ forget T.

                                        Equations
                                        Instances For
                                          @[reducible, inline]

                                          (Impl) Define the map λ : L ⟶ TL, which will serve as the structure of the algebra on L, and we will show is the limiting object. We use the cone constructed by c and the fact that T preserves limits to produce this morphism.

                                          Equations
                                          Instances For

                                            (Impl) Construct the limiting coalgebra from the map λ : L ⟶ TL given by lambda. We are required to show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of D and our commuting lemma.

                                            Equations
                                            Instances For

                                              (Impl) Construct the lifted cone in Coalgebra T which will be limiting.

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

                                                (Impl) Prove that the lifted cone is limiting.

                                                Equations
                                                Instances For
                                                  noncomputable instance CategoryTheory.Comonad.forgetCreatesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] :

                                                  The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit which the comonad itself preserves.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Equations
                                                  • CategoryTheory.Comonad.forgetCreatesLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J T.Coalgebra} => inferInstance }

                                                  For D : J ⥤ Coalgebra T, D ⋙ forget T has a limit, then D has a limit provided limits of shape J are preserved by T.

                                                  The coreflector always preserves initial objects. Note this in general doesn't apply to any other colimit.

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