CategoryTheory.Limits.IsZero.eq_of_src
theorem CategoryTheory.Limits.IsZero.eq_of_src :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
CategoryTheory.Limits.IsZero X → ∀ (f g : X ⟶ Y), f = g
This theorem states that for any category `C` and any two objects `X` and `Y` in `C`, if `X` is a zero object (an object that is both initial and terminal), then any two morphisms `f` and `g` from `X` to `Y` are equal. In other words, in a given category, all morphisms originating from a zero object to any other object are the same.
More concisely: In any category, if an object is both initial and terminal, then all morphisms from it to any other object are equal.
|
CategoryTheory.Limits.IsZero.eq_of_tgt
theorem CategoryTheory.Limits.IsZero.eq_of_tgt :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
CategoryTheory.Limits.IsZero X → ∀ (f g : Y ⟶ X), f = g
This theorem states that for any category `C` and any objects `X` and `Y` in this category, if `X` is a zero object in the category, then any two morphisms `f` and `g` from `Y` to `X` are equal. Here, a zero object in a category is an object that is both an initial object and a terminal object, i.e., it has a unique morphism to every object and a unique morphism from every object.
More concisely: In any category, if an object is both initial and terminal, then any two morphisms from any object to it are equal.
|
CategoryTheory.Limits.IsZero.unique_from
theorem CategoryTheory.Limits.IsZero.unique_from :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
CategoryTheory.Limits.IsZero X → ∀ (Y : C), Nonempty (Unique (Y ⟶ X))
This theorem states that for any category `C` and any object `X` in `C` that is a zero object, for any other object `Y` in `C`, there exists a unique morphism from `Y` to `X`. In the context of category theory, a zero object is an object that is both an initial object and a terminal object. This theorem therefore asserts the uniqueness of morphisms from any object to a zero object in the category.
More concisely: For any zero object X in a category C, there exists a unique morphism from any object Y in C to X.
|
CategoryTheory.Functor.isZero
theorem CategoryTheory.Functor.isZero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
(F : CategoryTheory.Functor C D),
(∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)) → CategoryTheory.Limits.IsZero F
This theorem states that given two categories `C` and `D`, and a functor `F` from `C` to `D`, if for all objects `X` in `C`, `F.obj X` is a zero object in `D` (meaning it's both a terminal and initial object), then the functor `F` itself is considered a zero functor in the limit theory of categories. This is under the condition that `C` and `D` have respective category structures.
More concisely: If for every object X in a category C, the image F.obj X under a functor F from C to D is a zero object in D, then F is a zero functor in the limit theory of categories C and D.
|
CategoryTheory.Limits.IsZero.of_iso
theorem CategoryTheory.Limits.IsZero.of_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
CategoryTheory.Limits.IsZero Y → (X ≅ Y) → CategoryTheory.Limits.IsZero X
This theorem states that in any category `C`, if `Y` is a zero object (meaning it has the property that for every object in the category, there exists a unique morphism from `Y` to that object and from that object to `Y`), and `X` is isomorphic to `Y`, then `X` is also a zero object. The key premise is that being a zero object is preserved under isomorphism.
More concisely: If `X` is isomorphic to a zero object `Y` in a category `C`, then `X` is also a zero object.
|
CategoryTheory.Limits.IsZero.unique_to
theorem CategoryTheory.Limits.IsZero.unique_to :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
CategoryTheory.Limits.IsZero X → ∀ (Y : C), Nonempty (Unique (X ⟶ Y))
This theorem states that for any category `C` and any object `X` in this category, if `X` is a zero object (meaning it has certain properties as defined in the category theory), then for every other object `Y` in the same category, there is a unique morphism (also known as an arrow or function) from `X` to `Y`.
More concisely: For any category `C` and zero object `X` in `C`, there exists a unique morphism from `X` to every other object `Y` in `C`.
|
CategoryTheory.Limits.HasZeroObject.to_zero_ext
theorem CategoryTheory.Limits.HasZeroObject.to_zero_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
(f g : X ⟶ 0), f = g
This theorem states that in the context of category theory, given any category `C` that has a zero object, for any object `X` in `C`, any two morphisms `f` and `g` from `X` to the zero object are equal. In essence, it asserts the uniqueness of the morphism from any object to the zero object in a category with a zero object.
More concisely: In a category with a zero object, any two morphisms from an object to the zero object are equal.
|
CategoryTheory.Limits.IsZero.obj
theorem CategoryTheory.Limits.IsZero.obj :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
[inst_2 : CategoryTheory.Limits.HasZeroObject D] {F : CategoryTheory.Functor C D},
CategoryTheory.Limits.IsZero F → ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
This theorem states that for any categories `C` and `D` where `D` has a zero object, and any functor `F` from `C` to `D`, if `F` is a zero functor (i.e., it maps every object to the zero object of `D` and every morphism to the zero morphism of `D`), then for any object `X` in `C`, the image of `X` under `F` (`F.obj X`) is a zero object in `D`. In simpler terms, a zero functor sends all objects to a zero object and all morphisms to the zero morphism.
More concisely: For any categories `C` and `D` with a zero object, and any zero functor `F` from `C` to `D`, the image of any object `X` in `C` under `F` is the zero object in `D`.
|
CategoryTheory.Iso.isZero_iff
theorem CategoryTheory.Iso.isZero_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
(X ≅ Y) → (CategoryTheory.Limits.IsZero X ↔ CategoryTheory.Limits.IsZero Y)
This theorem states that in a category `C`, for any objects `X` and `Y`, if `X` is isomorphic to `Y` (denoted by `X ≅ Y`), then `X` is a zero object in the category if and only if `Y` is also a zero object. In category theory, a zero object is both an initial object and a terminal object. This theorem essentially shows that the property of being a zero object is preserved under isomorphism.
More concisely: In a category, if two objects are isomorphic, then they are both zero objects if and only if they each are.
|
CategoryTheory.Limits.HasZeroObject.from_zero_ext
theorem CategoryTheory.Limits.HasZeroObject.from_zero_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
(f g : 0 ⟶ X), f = g
This theorem states that in the context of category theory, given a category `C` with a zero object, and for any object `X` in `C`, any two morphisms `f` and `g` from the zero object to `X` are equal. This is an expression of the uniqueness property of morphisms from the zero object in a category with a zero object.
More concisely: In a category with a zero object, any two morphisms from the zero object to an object X are equal.
|
CategoryTheory.Limits.isZero_zero
theorem CategoryTheory.Limits.isZero_zero :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C],
CategoryTheory.Limits.IsZero 0
This theorem states that for any type `C` which is a Category, and given that `C` has a Zero object, the object `0` is a Zero object in the category `C`. In the context of category theory, a Zero object is an object that is both an initial object and a terminal object. This means that there's exactly one morphism going to (for terminal objects) and coming from (for initial objects) the Zero object to any other object in the category.
More concisely: In any category with a Zero object, the Zero object is both initial and terminal.
|
CategoryTheory.Limits.HasZeroObject.zero
theorem CategoryTheory.Limits.HasZeroObject.zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasZeroObject C],
∃ X, CategoryTheory.Limits.IsZero X
This theorem states that for any given category `C` (of Type `u`), if `C` has a zero object, there exists an object `X` in `C` such that `X` is a zero object. In category theory, a zero object is an object that is both a terminal object and an initial object.
More concisely: In any category with a zero object, there exists a unique object that is both initial and terminal.
|