CategoryTheory.Equivalence.hasInitial_iff
theorem CategoryTheory.Equivalence.hasInitial_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D],
(C ≌ D) → (CategoryTheory.Limits.HasInitial C ↔ CategoryTheory.Limits.HasInitial D)
This theorem states that for any two categories `C` and `D`, if `C` is equivalent to `D` (denoted as `C ≌ D`), then `C` has an initial object if and only if `D` has an initial object. In the context of category theory, an initial object of a category is one that has a single morphism to any object in the category. The equivalence between two categories is a concept that formalizes the idea of the categories being 'essentially the same' in terms of their categorical structure. So, this theorem is saying that the property of having an initial object is preserved under the equivalence of categories.
More concisely: If categories `C` and `D` are equivalent, then `C` has an initial object if and only if `D` has an initial object.
|
CategoryTheory.Equivalence.hasTerminal_iff
theorem CategoryTheory.Equivalence.hasTerminal_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D],
(C ≌ D) → (CategoryTheory.Limits.HasTerminal C ↔ CategoryTheory.Limits.HasTerminal D)
The theorem `CategoryTheory.Equivalence.hasTerminal_iff` asserts that for any two categories `C` and `D` (of type `Type u₁` and `Type u₂`, respectively), if `C` is equivalent to `D` (denoted `C ≌ D`), then `C` has a terminal object if and only if `D` has a terminal object. In category theory, a terminal object in a category is an object that has exactly one morphism going to it from any other object in the category. The equivalence of categories is a relation that expresses that two categories are "essentially the same" in terms of category theory.
More concisely: If categories `C` and `D` are equivalent, then `C` has a terminal object if and only if `D` has a terminal object.
|