CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from
theorem CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [self : CategoryTheory.Limits.InitialMonoClass C]
{I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)
The theorem `CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from` states that, for any category `C` that is also an instance of `InitialMonoClass`, given any initial object `I` in `C` and any other object `X` in `C`, the morphism from the initial object to `X` is a monomorphism. In category theory, a monomorphism is a morphism (or arrow) that is left-cancellable. This means that for any object `X` in the category, the morphism from the initial object to `X` has the property that if it is followed by two other morphisms and the resulting compositions are equal, then the two other morphisms must have been equal.
More concisely: In any category with initial objects and monomorphisms (an instance of `InitialMonoClass`), the morphism from the initial object to any other object is a monomorphism.
|
CategoryTheory.Limits.IsInitial.epi_to
theorem CategoryTheory.Limits.IsInitial.epi_to :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsInitial X → ∀ (f : Y ⟶ X), CategoryTheory.Epi f
This theorem states that for any category `C`, and any objects `X` and `Y` in `C`, if `X` is an initial object (i.e., the cocone it induces on the empty diagram is a colimit), then any morphism `f` from `Y` to `X` is an epimorphism (surjective homomorphism). In other words, in a category, any morphism to an initial object is an epimorphism.
More concisely: In any category, an initial object is the colimit of the empty diagram, and any morphism to an initial object is an epimorphism.
|
CategoryTheory.Limits.IsInitial.hasInitial
theorem CategoryTheory.Limits.IsInitial.hasInitial :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.HasInitial C
The theorem `CategoryTheory.Limits.IsInitial.hasInitial` states that for any category `C` and any object `X` of `C`, if `X` is an initial object (meaning that the cocone it induces on the empty diagram is colimiting), then `C` has an initial object (meaning that it has a colimit over the empty diagram).
More concisely: If an object `X` in a category `C` is initial, then `C` has an initial object.
|
CategoryTheory.Limits.IsInitial.to_self
theorem CategoryTheory.Limits.IsInitial.to_self :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X),
t.to X = CategoryTheory.CategoryStruct.id X
This theorem states that for any category `C` and any object `X` in `C`, if `X` is an initial object in the category (denoted by `CategoryTheory.Limits.IsInitial X`), then the morphism from the initial object `X` to itself (`CategoryTheory.Limits.IsInitial.to t X`) is identical to the identity morphism on `X` (`CategoryTheory.CategoryStruct.id X`). In other words, in any category, the morphism from an initial object to itself is always the identity morphism.
More concisely: In any category, the morphism from an initial object to itself is the identity morphism.
|
Mathlib.CategoryTheory.Limits.Shapes.Terminal._auxLemma.1
theorem Mathlib.CategoryTheory.Limits.Shapes.Terminal._auxLemma.1 :
∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True
This theorem, which is part of the CategoryTheory in Mathlib, states that for any type `α` that is a subsingleton (i.e., a type with at most one instance), any two instances `x` and `y` of `α` are equal. The equality `x = y` is always `True`. Therefore, in a subsingleton category, there's essentially only one object, so any two objects must be the same.
More concisely: In a subsingleton type `α`, any two instances `x` and `y` are equal: `x = y`.
|
CategoryTheory.Limits.hasTerminal_of_unique
theorem CategoryTheory.Limits.hasTerminal_of_unique :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (Y ⟶ X)],
CategoryTheory.Limits.HasTerminal C
This theorem states that we can more explicitly demonstrate that a category has a terminal object by specifying an object (`X`) in this category (`C`), and proving that there exists a unique morphism from any other object (`Y`) in the category to this specified object (`X`). In other words, if for every object `Y` in some category `C`, there is a unique morphism from `Y` to a particular object `X`, then `C` has a terminal object. This is a fundamental concept in category theory, where a terminal object is one that has exactly one morphism from every other object in the category.
More concisely: A category has a terminal object if and only if there exists an object with a unique morphism to every other object.
|
CategoryTheory.Limits.InitialMonoClass.of_isTerminal
theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I T : C} (hI : CategoryTheory.Limits.IsInitial I),
CategoryTheory.Limits.IsTerminal T → CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
This theorem states that in order to demonstrate that a category is an `InitialMonoClass`, it is sufficient to prove that the unique morphism from an initial object to a terminal object is a monomorphism. Here, `InitialMonoClass` is a class of categories and a monomorphism is a morphism in a category which can be "cancelled" from the left. An initial object in a category is an object for which there is exactly one morphism from that object to any other object in the category. Correspondingly, a terminal object in a category is an object for which there is exactly one morphism to that object from any other object in the category. Hence, the theorem asserts that the category can be deemed as an `InitialMonoClass` if the morphism between the initial and terminal objects of the category possesses the properties of a monomorphism.
More concisely: A category has the initial-terminal object property (is an InitialMonoClass) if the unique morphism from the initial object to the terminal object is a monomorphism.
|
CategoryTheory.Limits.InitialMonoClass.of_terminal
theorem CategoryTheory.Limits.InitialMonoClass.of_terminal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
[inst_2 : CategoryTheory.Limits.HasTerminal C],
CategoryTheory.Mono (CategoryTheory.Limits.initial.to (⊤_ C)) → CategoryTheory.Limits.InitialMonoClass C
This theorem states that in order to demonstrate that a category is an `InitialMonoClass`, it is enough to show that the unique morphism from the initial object to a terminal object is a monomorphism. More specifically, given a category `C` that has an initial object and a terminal object, if the morphism from the initial object to the terminal object in `C` is a monomorphism (which means it is left-cancellable), then `C` is an `InitialMonoClass` category. This means that in `C`, every morphism from the initial object is a monomorphism.
More concisely: In a category with an initial and terminal object, the unique morphism between them being a monomorphism implies that every morphism from the initial object is a monomorphism, making the category an InitialMonoClass.
|
CategoryTheory.Limits.initial.to_comp
theorem CategoryTheory.Limits.initial.to_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P Q : C}
(f : P ⟶ Q),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to P) f = CategoryTheory.Limits.initial.to Q
This theorem states that for any category `C` that has an initial object, and any two objects `P` and `Q` in `C`, with a morphism `f` from `P` to `Q`, the composition of the morphism from the initial object to `P` with `f` is equal to the morphism from the initial object to `Q`. This is essentially a specific instance of the universal property of the initial object, stating that there is a unique morphism from the initial object to any object in the category, which commutes with any other morphisms in the category.
More concisely: For any category with an initial object, the unique morphism from the initial object to any object commutes with any morphism from that object to another.
|
CategoryTheory.Limits.isIso_ι_of_isTerminal
theorem CategoryTheory.Limits.isIso_ι_of_isTerminal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
{j : J},
CategoryTheory.Limits.IsTerminal j →
∀ (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
The theorem `CategoryTheory.Limits.isIso_ι_of_isTerminal` states that for any category `C`, index category `J`, object `j` in `J`, and functor `F` from `J` to `C`, if `j` is a terminal object in `J`, then the map `colimit.ι F j` from the object `F.obj j` in `C` to the colimit of `F` is an isomorphism. In category theory, this corresponds to the intuitive idea that if `j` is a terminal object (i.e., there is a unique morphism from any object in the category to `j`), then the morphism from `F.obj j` to the colimit of `F` fully captures the structure of the colimit.
More concisely: If `j` is a terminal object in the index category `J` of a functor `F:` `J` → `C`, then the map `colimit.ι F j:` `F.obj j` → `Colim F` is an isomorphism in `C`.
|
CategoryTheory.Limits.IsTerminal.from_self
theorem CategoryTheory.Limits.IsTerminal.from_self :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X),
t.from X = CategoryTheory.CategoryStruct.id X
This theorem, `CategoryTheory.Limits.IsTerminal.from_self`, states that for any category `C` and any object `X` in `C` that is terminal (as per the definition `CategoryTheory.Limits.IsTerminal`), the morphism from `X` to itself (obtained using `CategoryTheory.Limits.IsTerminal.from`) is the identity morphism on `X` (as per `CategoryTheory.CategoryStruct.id`). In category-theoretical terms, this expresses the property that in any category, the morphism from a terminal object to itself is always the identity morphism.
More concisely: In any category, the morphism from a terminal object to itself is the identity morphism.
|
CategoryTheory.Limits.isIso_π_of_isInitial
theorem CategoryTheory.Limits.isIso_π_of_isInitial :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
{j : J},
CategoryTheory.Limits.IsInitial j →
∀ (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
This theorem states that, given a Category `C` and an Index Category `J`, if `j` is an initial object in the category `J`, then the projection map from the limit of a functor `F` to the object `F.obj j`, denoted as `limit.π F j`, is an isomorphism. This implies that the limit object and the object `F.obj j` are isomorphic when viewed through the functor `F`, assuming the functor `F` has a limit in the category `C` and `j` is an initial object in the index category `J`.
More concisely: Given a functor `F` with a limit in a category `C` and an initial object `j` in the index category `J`, the projection from the limit of `F` to `F.obj j` is an isomorphism.
|
CategoryTheory.Limits.hasInitial_of_unique
theorem CategoryTheory.Limits.hasInitial_of_unique :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (X ⟶ Y)],
CategoryTheory.Limits.HasInitial C
This theorem states that we can explicitly demonstrate that a category has an initial object by indicating a particular object, and showing that there exists a unique morphism from this object to any other object in the category. Specifically, for any category `C`, if there is an object `X` in `C` such that for every object `Y` in `C` there exists a unique morphism from `X` to `Y`, then `C` has an initial object. This object is unique up to unique isomorphism. This theorem is an important characteristic property of initial objects in category theory.
More concisely: A category has an initial object if and only if there exists an object with a unique morphism to every other object.
|
CategoryTheory.Limits.IsTerminal.hom_ext
theorem CategoryTheory.Limits.IsTerminal.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsTerminal X → ∀ (f g : Y ⟶ X), f = g
This theorem states that in any category 'C', for any two objects 'X' and 'Y' such that 'X' is a terminal object, any two morphisms from 'Y' to 'X' are equal. In other words, if 'X' is a terminal object in the category 'C', then there is a unique morphism from any object 'Y' in 'C' to 'X'.
More concisely: In any category, a terminal object has unique morphisms from any object.
|
CategoryTheory.Limits.terminal.comp_from
theorem CategoryTheory.Limits.terminal.comp_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P Q : C}
(f : P ⟶ Q),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.terminal.from Q) =
CategoryTheory.Limits.terminal.from P
This theorem, `CategoryTheory.Limits.terminal.comp_from`, states that for any category `C` that has a terminal object, and any two objects `P` and `Q` in that category, the composition of any morphism `f` from `P` to `Q` with the morphism from `Q` to the terminal object is equal to the morphism from `P` to the terminal object. In simpler terms, it says that in a category with a terminal object, going from any object `P` to any other object `Q` and then to the terminal object is the same as going directly from `P` to the terminal object. This theorem formalizes the intuitive property of terminal objects in category theory.
More concisely: For any category with a terminal object, the composition of any morphism with the unique morphism to the terminal object is equal to that morphism.
|
CategoryTheory.Limits.IsTerminal.mono_from
theorem CategoryTheory.Limits.IsTerminal.mono_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsTerminal X → ∀ (f : X ⟶ Y), CategoryTheory.Mono f
This theorem states that in any category `C`, for any objects `X` and `Y` in `C`, if `X` is a terminal object, then any morphism `f` from `X` to `Y` is a monomorphism. In category theory, a monomorphism (or "mono") is a morphism (in this case `f`) that is left-cancellable, meaning that for any other morphisms `g`, `h`, if `f ∘ g = f ∘ h` then `g = h`. A terminal object in a category is an object such that there exists a unique morphism from any object in the category to the terminal object.
More concisely: In any category, a terminal object is the unique object mapping to every other object via monomorphisms.
|
CategoryTheory.Limits.IsTerminal.isSplitMono_from
theorem CategoryTheory.Limits.IsTerminal.isSplitMono_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsTerminal X → ∀ (f : X ⟶ Y), CategoryTheory.IsSplitMono f
This theorem states that for any category `C`, and any two objects `X` and `Y` in `C`, if `X` is a terminal object in the category, then any morphism `f` from `X` to `Y` is a split monomorphism. In the context of category theory, a terminal object is one which has a unique morphism to every other object, while a split monomorphism is a left inverse, meaning there exists a morphism going in the opposite direction that makes the composition equal to the identity.
More concisely: In any category, a terminal object is the initial object of the opposite category and its morphisms to other objects are split monomorphisms.
|
CategoryTheory.Limits.IsInitial.hom_ext
theorem CategoryTheory.Limits.IsInitial.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsInitial X → ∀ (f g : X ⟶ Y), f = g
This theorem states that in any category `C`, if `X` is an initial object, then any two morphisms from `X` to another object `Y` in the category must be equal. Here, "initial object" refers to an object in the category for which there exists exactly one morphism to every object in the category.
More concisely: In any category, if there exists a unique morphism from the initial object to every object, then any two morphisms from the initial object to an arbitrary object are equal.
|
CategoryTheory.Limits.IsTerminal.comp_from
theorem CategoryTheory.Limits.IsTerminal.comp_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsTerminal Z)
{X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (t.from Y) = t.from X
The theorem `CategoryTheory.Limits.IsTerminal.comp_from` states that for any category `C` and any terminal object `Z` in `C`, for any objects `X`, `Y` in `C` and any morphism `f` from `X` to `Y`, the composition of `f` with the unique morphism from `Y` to the terminal object `Z` is equal to the unique morphism from `X` to `Z`. This is essentially asserting the uniqueness property of the morphism to the terminal object in a category.
More concisely: For any category `C` with a terminal object `Z`, given objects `X`, `Y` in `C` and a morphism `f : X → Y`, the unique morphisms from `Y` to `Z` and from `X` to `Z` are equal, i.e., `f ∘ u = t`, where `u` is the unique morphism from `Y` to `Z`, and `t` is the unique morphism from `X` to `Z`.
|
CategoryTheory.Limits.InitialMonoClass.of_isInitial
theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : C} (hI : CategoryTheory.Limits.IsInitial I),
(∀ (X : C), CategoryTheory.Mono (hI.to X)) → CategoryTheory.Limits.InitialMonoClass C
The theorem `CategoryTheory.Limits.InitialMonoClass.of_isInitial` states that, for a given category `C` and an object `I` in `C`, if `I` is an initial object and every morphism from `I` to any other object in `C` is a monomorphism (a morphism which is left-cancellative), then `C` is an `InitialMonoClass`. In other words, to prove that a category is an `InitialMonoClass`, it's enough to show the existence of an initial object from which every outgoing morphism is a monomorphism.
More concisely: In a category, if every morphism from an initial object is a monomorphism, then the category has the initial object property in the monic morphism class.
|
CategoryTheory.Limits.IsTerminal.hasTerminal
theorem CategoryTheory.Limits.IsTerminal.hasTerminal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.HasTerminal C
This theorem states that for any Category `C` and object `X` in this category, if `X` is a terminal object (i.e., `CategoryTheory.Limits.IsTerminal X` holds), then the category `C` itself has a terminal object (i.e., `CategoryTheory.Limits.HasTerminal C` holds). In category theory, a terminal object is one for which there is a unique morphism from any other object in the category to the terminal object. Thus, the theorem essentially establishes the existence of a terminal object in the category if any one of its objects is terminal.
More concisely: If an object `X` in a category `C` is terminal, then `C` itself has a terminal object.
|
CategoryTheory.Limits.IsInitial.isSplitEpi_to
theorem CategoryTheory.Limits.IsInitial.isSplitEpi_to :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
CategoryTheory.Limits.IsInitial X → ∀ (f : Y ⟶ X), CategoryTheory.IsSplitEpi f
This theorem states that in any category `C`, for any objects `X` and `Y` within `C`, if `X` is an initial object, then any morphism `f` from `Y` to `X` is a split epimorphism. In other words, in the context of category theory, if we start with an initial object and a morphism from some object to this initial object, the morphism can be "split" or factored into an epimorphism followed by a monomorphism, essentially providing a sort of "reverse" to the morphism.
More concisely: In any category, an initial object's morphisms are split epimorphisms.
|
CategoryTheory.Limits.InitialMonoClass.of_initial
theorem CategoryTheory.Limits.InitialMonoClass.of_initial :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
(∀ (X : C), CategoryTheory.Mono (CategoryTheory.Limits.initial.to X)) →
CategoryTheory.Limits.InitialMonoClass C
The theorem `CategoryTheory.Limits.InitialMonoClass.of_initial` states that for any category `C` that has an initial object, if every morphism from the initial object to any object `X` in `C` is a monomorphism (which is a morphism that is "left-cancellable", i.e., if the composition of it with any other morphism is equal to the composition with another morphism, then the two morphisms are equal), then `C` is an `InitialMonoClass`. In other words, a category is an `InitialMonoClass` if every morphism that begins at the initial object is a monomorphism.
More concisely: In a category with an initial object, if every morphism from the initial object is a monomorphism, then the category is an InitialMonoClass.
|