CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves
theorem CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
[inst_1 : CategoryTheory.Category.{v, u} J]
[inst_2 : CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] (D : CategoryTheory.Functor J T.Algebra)
[inst_3 : CategoryTheory.Limits.HasColimit (D.comp T.forget)], CategoryTheory.Limits.HasColimit D
This theorem states that for a given monad `T` on a category `C` and a functor `D` from `J` to the algebra of `T`, if the functor `D` followed by the forgetful functor of `T` has a colimit and `T` preserves colimits of shape `J`, then the functor `D` itself has a colimit. In other words, if a monad preserves certain colimits, then those colimits can be lifted from the underlying category to the category of algebras of the monad.
More concisely: If a monad `T` on a category `C` preserves colimits of shape `J`, and the functor `D : J -> T(C)` has a colimit under the forgetful functor `U : T(C) -> C`, then `D` has a colimit in `T(C)`.
|
CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app
theorem CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
[inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
(c : CategoryTheory.Limits.Cone (D.comp T.forget)) (X : J),
(CategoryTheory.Monad.ForgetCreatesLimits.newCone D c).π.app X =
CategoryTheory.CategoryStruct.comp (T.map (c.π.app X)) (D.obj X).a
This theorem states that for any category `C`, monad `T` on `C`, type `J`, functor `D` from `J` to the category of T-algebras, and a cone `c` over the composition of `D` and the forgetful functor from the category of T-algebras to `C`, the morphism given by the natural transformation component of the cone created by the forgetful functor at any object `X` of `J` is equal to the composition of the morphism given by `T` applied to the morphism given by the natural transformation component of cone `c` at `X`, and the morphism given by the algebra structure of the object of `D` at `X`. This theorem essentially describes a property of the new cone created by the forgetful functor in the context of monadic algebraic structures.
More concisely: For any category `C`, monad `T` on `C`, functor `D` from a category `J` to the category of `T`-algebras, and a cone `c` over the composition of `D` and the forgetful functor from the category of `T`-algebras to `C`, the natural transformation component of the forgetful functor's cone at any object `X` of `J` equals the composition of `T` applied to this cone's component at `X` and the algebra structure morphism of `D(X)`.
|
CategoryTheory.hasLimitsOfShape_of_reflective
theorem CategoryTheory.hasLimitsOfShape_of_reflective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J]
[inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] (R : CategoryTheory.Functor D C)
[inst : CategoryTheory.Reflective R], CategoryTheory.Limits.HasLimitsOfShape J D
This theorem states that if a category `C` has limits of a certain shape `J`, then any subcategory `D` that is reflective in `C` (i.e., there exists a functor `R` from `D` to `C` that exhibits `D` as a reflective subcategory of `C`) also has limits of the shape `J`. This restricts the types of limits that are preserved when considering subcategories.
More concisely: If `C` is a category with limits of shape `J` and `D` is a reflective subcategory of `C`, then `D` also has limits of shape `J`.
|
CategoryTheory.Monad.ForgetCreatesColimits.commuting
theorem CategoryTheory.Monad.ForgetCreatesColimits.commuting :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
[inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
(c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
[inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] (j : J),
CategoryTheory.CategoryStruct.comp (T.map (c.ι.app j)) (CategoryTheory.Monad.ForgetCreatesColimits.lambda c t) =
CategoryTheory.CategoryStruct.comp (D.obj j).a (c.ι.app j)
This theorem states that for any category `C` with a monad `T`, and any functor `D` from a category `J` to the category of `T`-algebras, given a cocone `c` under `D` followed by the functor that forgets the algebra structure, if `c` is a colimit cocone, then for every object `j` in `J`, the composition of the map induced by `T` and a certain map `λ` (defined in the context of the theorem) is equal to the composition of the algebra structure of `D.obj j` and the `j`-th component of the cocone `c`. This is a key property defining the map `λ`, ensuring that the forgetful functor `T` creates colimits.
More concisely: For any monad `T` over a category `C`, functor `D` from a category `J` to `T`-algebras, and cocone `c` under `D`, if `c` is a colimit cocone, then for all objects `j` in `J`, the diagram `T(D.obj j) ∘ λ = D.obj j ∘ c.μ(j)` commutes, where `λ` is a specific map defined in the context of the theorem.
|
CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit
theorem CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
[inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
[inst_2 : CategoryTheory.Limits.HasLimit (D.comp T.forget)], CategoryTheory.Limits.HasLimit D
This theorem states that if for a given category `C`, monad `T` on `C`, type `J`, and functor `D` from `J` to the algebra of `T`, the composite of `D` and the forgetful functor of `T` has a limit, then `D` itself also has a limit. In other words, if we can find a limit for the functor obtained by forgetting the monadic structure via `T.forget` and then applying `D`, then we can also find a limit for `D` alone. This is a statement about the relationship between limits in the category of algebras of a monad and limits in the underlying category.
More concisely: If a functor `D` from a category `J` to the algebra of a monad `T` over a category `C` has a limit when composed with the forgetful functor `T.forget`, then `D` itself has a limit in `C`.
|
CategoryTheory.hasLimits_of_reflective
theorem CategoryTheory.hasLimits_of_reflective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C)
[inst_2 : CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] [inst : CategoryTheory.Reflective R],
CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
This theorem is stating that if a category `C` has limits, then any reflective subcategory `D` also has limits. More specifically, given a functor `R` from the subcategory `D` to `C`, if `C` has limits of a certain size, and `R` is a reflective functor (meaning `D` is a reflective subcategory of `C`), then `D` also has limits of that size. The concept of limits is an essential part of category theory and reflects the idea of taking the "best possible" limit within a category.
More concisely: If `C` is a category with limits and `D` is a reflective subcategory of `C` with respect to a functor `R`, then `D` also has limits of the same size.
|
CategoryTheory.hasColimitsOfShape_of_reflective
theorem CategoryTheory.hasColimitsOfShape_of_reflective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J]
(R : CategoryTheory.Functor D C) [inst_3 : CategoryTheory.Reflective R]
[inst : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J D
This theorem states that if a category `C` has colimits of a particular shape `J`, then any reflective subcategory `D` also has colimits of the same shape `J`. Here, the functor `R` is used to reflect the subcategory `D` into the category `C`.
More concisely: If `C` has colimits of shape `J` and `D` is a reflective subcategory of `C` via the reflector functor `R`, then `D` has colimits of shape `J` with the corresponding colimits in `C` preserved by `R`.
|
CategoryTheory.hasColimits_of_reflective
theorem CategoryTheory.hasColimits_of_reflective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C)
[inst_2 : CategoryTheory.Reflective R] [inst : CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C],
CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D
This theorem states that if a category `C` has colimits, then any reflective subcategory `D` (reflected by a functor `R` from `D` to `C`) also has colimits. Here, both `C` and `D` are general categories which could be of any type (`u₁` and `u₂` respectively) and any category size (`v₁` and `v₂` respectively). The theorem assumes that we have a way to generate colimits in `C` (as expressed by `CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C`) and requires us to prove that we have a similar mechanism for constructing colimits in `D` (as expressed by `CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D`).
More concisely: If `C` is a category with colimits and `D` is a reflective subcategory of `C`, then `D` also has colimits.
|