CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit
theorem CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.Limits.HasTerminal C]
[inst : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G],
CategoryTheory.Limits.HasTerminal D
The theorem `CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit` states that if a category `C` has a terminal object and a functor `G` preserves terminal objects, then another category `D` also has a terminal object. This is a significant property that is unique to (co)limits of the empty diagram; for more general `J`, the existence of limits of shape `J` in `C` and their preservation by `G` doesn't necessarily imply that `D` has limits of shape `J`.
More concisely: If a category has a terminal object and a functor preserves terminal objects, then the category has a terminal object as well.
|
CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit
theorem CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.Limits.HasInitial C]
[inst : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G],
CategoryTheory.Limits.HasInitial D
The theorem `CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit` states that, for any categories `C` and `D`, and a functor `G` from `C` to `D`, if `C` has an initial object and `G` preserves initial objects (which are represented as colimits over the empty diagram), then `D` also has an initial object. This property is somewhat unique to colimits of the empty diagram: for a general shape `J`, if `C` has colimits of shape `J` and `G` preserves them, `D` does not necessarily have colimits of shape `J`.
More concisely: If `C` is a category with an initial object and `G` is a functor from `C` to `D` preserving initial objects (as colimits over the empty diagram), then `D` has an initial object.
|