Documentation

Mathlib.CategoryTheory.Endofunctor.Algebra

Algebras of endofunctors #

This file defines (co)algebras of an endofunctor, and provides the category instance for them. It also defines the forgetful functor from the category of (co)algebras. It is shown that the structure map of the initial algebra of an endofunctor is an isomorphism. Furthermore, it is shown that for an adjunction F ⊣ G the category of algebras over F is equivalent to the category of coalgebras over G.

TODO #

An algebra of an endofunctor; str stands for "structure morphism"

  • a : C

    carrier of the algebra

  • str : F.obj self.a self.a

    structure morphism of the algebra

Instances For
    Equations
    theorem CategoryTheory.Endofunctor.Algebra.Hom.ext {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C} {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} {x y : A₀.Hom A₁}, x.f = y.fx = y
    theorem CategoryTheory.Endofunctor.Algebra.Hom.ext_iff {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C} {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} {x y : A₀.Hom A₁}, x = y x.f = y.f

    A morphism between algebras of endofunctor F

    Instances For

      The identity morphism of an algebra of endofunctor F

      Equations
      Instances For

        The composition of morphisms between algebras of endofunctor F

        Equations
        Instances For

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

          Equations
          Instances For

            The forgetful functor from the category of algebras, forgetting the algebraic structure.

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

              An algebra morphism with an underlying isomorphism hom in C is an algebra isomorphism.

              An algebra morphism with an underlying epimorphism hom in C is an algebra epimorphism.

              An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.

              From a natural transformation α : G → F we get a functor from algebras of F to algebras of G.

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

                The identity transformation induces the identity endofunctor on the category of algebras.

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

                  A composition of natural transformations gives the composition of corresponding functors.

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

                    If α and β are two equal natural transformations, then the functors of algebras induced by them are isomorphic. We define it like this as opposed to using eq_to_iso 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

                      Naturally isomorphic endofunctors give equivalent categories of algebras. Furthermore, they are equivalent as categories over C, that is, we have equiv_of_nat_iso hforget = forget.

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

                        The inverse of the structure map of an initial algebra

                        Equations
                        Instances For

                          The structure map of the initial algebra is an isomorphism, hence endofunctors preserve their initial algebras

                          A coalgebra of an endofunctor; str stands for "structure morphism"

                          • V : C

                            carrier of the coalgebra

                          • str : self.V F.obj self.V

                            structure morphism of the coalgebra

                          Instances For
                            Equations
                            theorem CategoryTheory.Endofunctor.Coalgebra.Hom.ext {C : Type u} :
                            ∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C} {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} {x y : V₀.Hom V₁}, x.f = y.fx = y

                            A morphism between coalgebras of an endofunctor F

                            Instances For

                              The identity morphism of an algebra of endofunctor F

                              Equations
                              Instances For

                                The composition of morphisms between algebras of endofunctor F

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

                                    The forgetful functor from the category of coalgebras, forgetting the coalgebraic structure.

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

                                      A coalgebra morphism with an underlying isomorphism hom in C is a coalgebra isomorphism.

                                      An algebra morphism with an underlying epimorphism hom in C is an algebra epimorphism.

                                      An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.

                                      From a natural transformation α : F → G we get a functor from coalgebras of F to coalgebras of G.

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

                                        The identity transformation induces the identity endofunctor on the category of coalgebras.

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

                                          A composition of natural transformations gives the composition of corresponding functors.

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

                                            If α and β are two equal natural transformations, then the functors of coalgebras induced by them are isomorphic. We define it like this as opposed to using eq_to_iso 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

                                              Naturally isomorphic endofunctors give equivalent categories of coalgebras. Furthermore, they are equivalent as categories over C, that is, we have equiv_of_nat_iso hforget = forget.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} {G : CategoryTheory.Functor C C} (adj : F G) (A₁ : CategoryTheory.Endofunctor.Algebra F) (A₂ : CategoryTheory.Endofunctor.Algebra F) (f : A₁ A₂) :
                                                CategoryTheory.CategoryStruct.comp ((adj.homEquiv A₁.a A₁.a) A₁.str) (G.map f.f) = CategoryTheory.CategoryStruct.comp f.f ((adj.homEquiv A₂.a A₂.a) A₂.str)
                                                theorem CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} {G : CategoryTheory.Functor C C} (adj : F G) (V₁ : CategoryTheory.Endofunctor.Coalgebra G) (V₂ : CategoryTheory.Endofunctor.Coalgebra G) (f : V₁ V₂) :
                                                CategoryTheory.CategoryStruct.comp (F.map f.f) ((adj.homEquiv V₂.V V₂.V).symm V₂.str) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv V₁.V V₁.V).symm V₁.str) f.f

                                                Given an adjunction F ⊣ G, the functor that associates to an algebra over F a coalgebra over G defined via adjunction applied to the structure map.

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

                                                  Given an adjunction F ⊣ G, the functor that associates to a coalgebra over G an algebra over F defined via adjunction applied to the structure map.

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

                                                    Given an adjunction, assigning to an algebra over the left adjoint a coalgebra over its right adjoint and going back is isomorphic to the identity functor.

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

                                                      Given an adjunction, assigning to a coalgebra over the right adjoint an algebra over the left adjoint and going back is isomorphic to the identity functor.

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

                                                        If F is left adjoint to G, then the category of algebras over F is equivalent to the category of coalgebras over G.

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