CategoryTheory.isSubterminal_of_mono_terminal_from
theorem CategoryTheory.isSubterminal_of_mono_terminal_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
[inst_2 : CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)], CategoryTheory.IsSubterminal A
The theorem `CategoryTheory.isSubterminal_of_mono_terminal_from` states that, within a category `C` that has a terminal object, if the unique morphism from an object `A` in `C` to the terminal object is a monomorphism (an injective morphism), then `A` is a subterminal object. A subterminal object is defined as an object `A` such that for any object `Z` in `C`, there is at most one morphism from `Z` to `A`. This theorem is the converse of `IsSubterminal.mono_terminal_from`, which would assert that if `A` is a subterminal object, then the unique morphism from `A` to the terminal object is a monomorphism.
More concisely: In a category with a terminal object, an object equipped with a monic unique morphism to the terminal object is a subterminal object.
|
CategoryTheory.IsSubterminal.mono_isTerminal_from
theorem CategoryTheory.IsSubterminal.mono_isTerminal_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C},
CategoryTheory.IsSubterminal A →
∀ {T : C} (hT : CategoryTheory.Limits.IsTerminal T), CategoryTheory.Mono (hT.from A)
In the context of category theory, this theorem states that if an object `A` is subterminal in a category `C`, then the unique morphism from `A` to any terminal object `T` in the same category `C` is a monomorphism. This is the converse of the theorem `isSubterminal_of_mono_isTerminal_from`. In other words, if we have an object `A` from which there can be at most one morphism to any other object in the category, then any morphism from `A` to a terminal object (an object to which there is exactly one morphism from every other object) must be monic, meaning it is left-cancellable.
More concisely: If an object `A` is subterminal in a category `C`, then the unique morphism from `A` to the terminal object `T` in `C` is a monomorphism.
|
CategoryTheory.isSubterminal_of_isIso_diag
theorem CategoryTheory.isSubterminal_of_isIso_diag :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct A A]
[inst_2 : CategoryTheory.IsIso (CategoryTheory.Limits.diag A)], CategoryTheory.IsSubterminal A
The theorem `CategoryTheory.isSubterminal_of_isIso_diag` states that in any category `C`, for any object `A` in `C` that has a binary product with itself, if the diagonal morphism of `A` (which is the morphism mapping `A` into the binary product of `A` and `A` via the identity morphisms) is an isomorphism, then the object `A` is a subterminal object in the category `C`. In other words, for any object `Z` in the category, there can be at most one morphism from `Z` to `A`. This is the converse of the theorem `isSubterminal.isIso_diag`.
More concisely: In a category with binary products, if the diagonal morphism of an object is an isomorphism, then that object is subterminal.
|
CategoryTheory.IsSubterminal.isIso_diag
theorem CategoryTheory.IsSubterminal.isIso_diag :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C},
CategoryTheory.IsSubterminal A →
∀ [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A], CategoryTheory.IsIso (CategoryTheory.Limits.diag A)
The theorem `CategoryTheory.IsSubterminal.isIso_diag` states that for any category `C` and an object `A` in `C`, if `A` is subterminal (that is, for any other object `Z` in `C`, there is at most one morphism from `Z` to `A`), and if `A` has a binary product with itself, then the diagonal morphism of `A` is an isomorphism.
In category theory, a morphism is an isomorphism if it has an inverse, that is, there is another morphism that can 'undo' the composition. The diagonal morphism here is created using the identity morphism and the binary product of `A` with itself. So, the theorem essentially says that if an object is subterminal and has a binary product with itself, then the morphism that maps it to this product is invertible.
More concisely: If an object in a category is subterminal and has a binary product with itself, then the diagonal morphism of that object is an isomorphism.
|
CategoryTheory.IsSubterminal.mono_terminal_from
theorem CategoryTheory.IsSubterminal.mono_terminal_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} [inst_1 : CategoryTheory.Limits.HasTerminal C],
CategoryTheory.IsSubterminal A → CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)
The theorem `CategoryTheory.IsSubterminal.mono_terminal_from` states that in any category `C` that has a terminal object, if an object `A` is subterminal (meaning that for every object `Z` in `C`, there is at most one morphism from `Z` to `A`), then the unique morphism from `A` to the terminal object of `C` is a monomorphism (a morphism that is left-cancellative, i.e., for any morphisms `g`, `h`, if `f ∘ g = f ∘ h`, then `g = h`). This theorem is the converse of `isSubterminal_of_mono_terminal_from`.
More concisely: In a category with a terminal object, a subterminal object is isomorphic to the kernel of the unique morphism to the terminal object, which is a monomorphism.
|
CategoryTheory.isSubterminal_of_mono_isTerminal_from
theorem CategoryTheory.isSubterminal_of_mono_isTerminal_from :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A T : C} (hT : CategoryTheory.Limits.IsTerminal T)
[inst_1 : CategoryTheory.Mono (hT.from A)], CategoryTheory.IsSubterminal A
This theorem states that, in a category `C`, if there exists a terminal object `T` and the unique morphism from an object `A` to `T` is a monomorphism, then `A` is a subterminal object. In simpler terms, if the unique path from `A` to a terminal object is a one-way morphism (it can't be reversed), then for any other object `Z` in the category, there can be at most one morphism from `Z` to `A`. The theorem is a converse of another statement (named `IsSubterminal.mono_isTerminal_from`) which presumably describes the reverse implication.
More concisely: If in a category with a terminal object, the unique morphism from an object to the terminal object is a monomorphism, then that object is a subterminal object.
|