CategoryTheory.Limits.IsInitial.isIso_to
theorem CategoryTheory.Limits.IsInitial.isIso_to :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
{I : C}, CategoryTheory.Limits.IsInitial I → ∀ {A : C} (f : A ⟶ I), CategoryTheory.IsIso f
The theorem `CategoryTheory.Limits.IsInitial.isIso_to` states that for any category `C` that has strict initial objects, if `I` is an initial object in `C`, then any morphism `f` from any object `A` in `C` to `I` is an isomorphism. In other words, in a category with strict initial objects, all morphisms to an initial object are isomorphisms.
More concisely: In a category with strict initial objects, every morphism to the initial object is an isomorphism.
|
CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal
theorem CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictTerminalObjects C]
{J : Type v} [inst_2 : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C)
[inst_3 : CategoryTheory.Limits.HasLimit F] (i : J),
((j : J) → j ≠ i → CategoryTheory.Limits.IsTerminal (F.obj j)) →
∀ [inst_4 : Subsingleton (i ⟶ i)], CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F i)
This theorem states that given a category `C` with strict terminal objects, a small category `J`, and a functor `F` from `J` to `C` for which a limit exists, if all but one object in the diagram (represented by the functor) are strict terminal, then the limit is isomorphic to the non-strict-terminal object. This isomorphism is realized via `limit.π` that projects from the limit object to a value of the functor. Note that the object is a singleton, i.e., there is only one morphism from the object to itself.
More concisely: Given a small category `J`, a functor `F` from `J` to a category `C` with strict terminal objects, if `F` has a limit with all but one object being a strict terminal in the diagram, then the limit is isomorphic to the non-strict-terminal object via `limit.π`.
|
CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict
theorem CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
(∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f) → CategoryTheory.Limits.HasStrictInitialObjects C
This theorem states that given any category `C` that has an initial object, if every morphism targeted at this initial object is an isomorphism, then the category `C` has strict initial objects. Here, strict initial objects refer to those initial objects in a category where any morphism targeted at them is necessarily an identity morphism. The theorem thus connects the condition of all morphisms being isomorphisms to the existence of strict initial objects in the category.
More concisely: If every morphism to the initial object in a category with an initial object is an isomorphism, then the initial object is a strict initial object.
|
CategoryTheory.Limits.IsInitial.strict_hom_ext
theorem CategoryTheory.Limits.IsInitial.strict_hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
{I : C}, CategoryTheory.Limits.IsInitial I → ∀ {A : C} (f g : A ⟶ I), f = g
This theorem states that for any category `C` that has strict initial objects, if `I` is an initial object in `C`, then for any object `A` in `C` and any two morphisms `f` and `g` from `A` to `I`, `f` must be equal to `g`. This property is characteristic of initial objects in a category, where there is exactly one morphism from any object to the initial object.
More concisely: In any category with strict initial objects, two morphisms from an arbitrary object to the initial object are equal.
|
CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict
theorem CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C),
(∀ (A : C) (f : I ⟶ A), CategoryTheory.IsIso f) → CategoryTheory.Limits.HasStrictTerminalObjects C
This theorem states that in any category `C`, if there exists an object `I` such that every morphism originating from `I` is an isomorphism, then `C` possesses strict terminal objects. In other words, if every morphism from a certain object in the category has an inverse, the category has strict terminal objects, i.e., objects for which there is exactly one morphism going into it from any other object.
More concisely: In a category with an initial object, the existence of an object from which every morphism is an isomorphism implies the existence of strict terminal objects.
|