CategoryTheory.Limits.zero_of_target_iso_zero
theorem CategoryTheory.Limits.zero_of_target_iso_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y), (Y ≅ 0) → f = 0
This theorem states that in the context of category theory, given a category `C` with a zero object and zero morphisms, for any objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, if `Y` is isomorphic to the zero object in the category, then the morphism `f` is the zero morphism. This can be thought of as a generalized form of the property in algebra that any function mapping into a zero object (analogous to a zero vector space) must be a zero function (a function that only outputs zero).
More concisely: In a category with a zero object and zero morphisms, if an object is isomorphic to the zero object, then any morphism to it is a zero morphism.
|
CategoryTheory.Limits.hasZeroObject_of_hasInitial_object
theorem CategoryTheory.Limits.hasZeroObject_of_hasInitial_object :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasInitial C], CategoryTheory.Limits.HasZeroObject C
The theorem `CategoryTheory.Limits.hasZeroObject_of_hasInitial_object` states that in a given category `C` with zero morphisms, if `C` also has an initial object, then `C` has a zero object. In category theory terms, if there exist morphisms in `C` which have both their source and target as the zero object (also known as zero morphisms), and `C` has an object (the initial object) such that there exists exactly one morphism from it to every other object in `C`, then `C` has a zero object. The zero object is a special type of object in `C` which is both an initial object and a terminal object.
More concisely: In a category with zero morphisms, the existence of an initial object implies the existence of a zero object.
|
CategoryTheory.Limits.zero_comp
theorem CategoryTheory.Limits.zero_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z : C} {f : Y ⟶ Z}, CategoryTheory.CategoryStruct.comp 0 f = 0
The theorem `CategoryTheory.Limits.zero_comp` states that for any category `C` with zero morphisms, and any objects `X`, `Y`, `Z` in `C`, if `f` is a morphism from `Y` to `Z`, then the composition of the zero morphism (from `X` to `Y`) and `f` is the zero morphism (from `X` to `Z`). Here, zero morphisms are the morphisms that behaves like zero in the category. Essentially, this theorem is saying that "zero times anything is zero" but in the context of category theory.
More concisely: For any category with zero morphisms, the composition of a zero morphism with any morphism is the zero morphism.
|
CategoryTheory.Limits.HasZeroMorphisms.comp_zero
theorem CategoryTheory.Limits.HasZeroMorphisms.comp_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
(f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0
This theorem, `CategoryTheory.Limits.HasZeroMorphisms.comp_zero`, states that in any category `C` which has zero-morphisms (meaning there's a special "zero" morphism between any two objects), for any objects `X`, `Y`, and `Z` in `C`, and any morphism `f` from `X` to `Y`, the composition of `f` with the zero-morphism (from `Y` to `Z`) is equal to the zero-morphism (from `X` to `Z`). In mathematical terms, this would be stated as "for all `f : X ⟶ Y`, we have `f ≫ 0 = 0`," where `≫` denotes the composition of morphisms.
More concisely: In any category with zero-morphisms, for all objects X, Y, Z, and morphisms f : X → Y, we have f ∘ 0 = 0, where ∘ denotes composition and 0 is the zero-morphism from Y to Z.
|
CategoryTheory.Limits.HasZeroMorphisms.ext
theorem CategoryTheory.Limits.HasZeroMorphisms.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I J : CategoryTheory.Limits.HasZeroMorphisms C), I = J
This theorem states that in any category `C`, there can only be one instance of `HasZeroMorphisms`. If you try to assert the existence of two such instances `I` and `J`, they must actually be the same. This is hinting at the uniqueness of zero morphisms in a category: you can't have two distinct sets of zero morphisms. If you're thinking about using this theorem, it suggests you might need to reconsider your approach, as having two `HasZeroMorphisms` instances might be a mistake. Particularly, you should look at the note on `zeroMorphismsOfZeroObject`.
More concisely: In any category, there can only be one instance of `HasZeroMorphisms`.
|
CategoryTheory.Limits.op_zero
theorem CategoryTheory.Limits.op_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : C), 0.op = 0
This theorem, `CategoryTheory.Limits.op_zero`, states that in any category `C` that possesses zero morphisms, the opposite of a zero morphism is still a zero morphism. More specifically, for any two objects `X` and `Y` in the category, the opposite of the zero morphism from `X` to `Y` is equal to the zero morphism.
More concisely: In a category with zero morphisms, the opposite of a zero morphism is equal to the zero morphism.
|
CategoryTheory.Limits.image.ι_zero'
theorem CategoryTheory.Limits.image.ι_zero' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasEqualizers C] {X Y : C}
{f : X ⟶ Y}, f = 0 → ∀ [inst_4 : CategoryTheory.Limits.HasImage f], CategoryTheory.Limits.image.ι f = 0
This theorem states that in a category `C` with zero morphisms, a zero object, and equalizers, if a morphism `f` from object `X` to object `Y` is the zero morphism (`f = 0`), then the inclusion of the image of `f` into the target `Y` is also the zero morphism (`CategoryTheory.Limits.image.ι f = 0`). This might require a bit of work because in general, equality of morphisms `f = g` only implies that the image of `f` is isomorphic to the image of `g` (`image f ≅ image g`).
More concisely: In a category with zero morphisms, a zero object, and equalizers, the zero morphism from an object to another object maps its source to the zero morphism of the target.
|
CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object
theorem CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasTerminal C], CategoryTheory.Limits.HasZeroObject C
This theorem states that within any category `C`, if `C` has zero morphisms and a terminal object, then `C` also has a zero object. In other words, if there exists a terminal object (an object such that there is exactly one morphism from every other object to it) and all zero morphisms (morphisms that satisfy certain properties in relation with the zero object) in a category, then that category certainly contains a zero object (an object that is both initial and terminal). This theorem bridges the concepts of terminal objects, zero morphisms, and zero objects in category theory.
More concisely: In any category with zero morphisms and a terminal object, the terminal object is the unique zero object.
|
CategoryTheory.Limits.zero_of_from_zero
theorem CategoryTheory.Limits.zero_of_from_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : 0 ⟶ X), f = 0
This theorem states that in the context of category theory, if we have a category 'C' that has a zero object and zero morphisms, then any morphism (represented by 'f') that starts at the zero object and leads to any object 'X' in the category, is a zero morphism. This is essentially saying that any arrow originating from the zero object is itself a zero.
More concisely: In a category with a zero object and zero morphisms, any morphism starting from the zero object is a zero morphism.
|
CategoryTheory.Limits.zero_of_epi_comp
theorem CategoryTheory.Limits.zero_of_epi_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [inst_2 : CategoryTheory.Epi f],
CategoryTheory.CategoryStruct.comp f g = 0 → g = 0
This theorem, `CategoryTheory.Limits.zero_of_epi_comp`, states that for any category `C` with zero morphisms and any objects `X`, `Y`, and `Z` in `C`, if `f` is an epimorphism (surjective morphism) from `X` to `Y` and the composition of `f` and `g` (`f ≫ g`, where `g` is a morphism from `Y` to `Z`) equals the zero morphism, then `g` must be the zero morphism. This essentially means that in a category with zero morphisms, the composition of an epimorphism and another morphism results in the zero morphism if and only if the second morphism is the zero morphism.
More concisely: In a category with zero morphisms, if an epimorphism's composition with another morphism equals the zero morphism, then the second morphism is the zero morphism.
|
CategoryTheory.Limits.zero_of_source_iso_zero
theorem CategoryTheory.Limits.zero_of_source_iso_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y), (X ≅ 0) → f = 0
This theorem states that in any category `C` which has a zero object and zero morphisms, for any morphism `f` from object `X` to `Y`, if `X` is isomorphic to the zero object, then `f` is the zero morphism. In other words, any morphism whose source object is isomorphic to the zero object must itself be the zero morphism.
More concisely: In any category with a zero object and zero morphisms, a morphism equals the zero morphism if and only if its source is isomorphic to the zero object.
|
CategoryTheory.Limits.HasZeroMorphisms.zero_comp
theorem CategoryTheory.Limits.HasZeroMorphisms.zero_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
{Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0
The theorem `CategoryTheory.Limits.HasZeroMorphisms.zero_comp` states that for any category `C` that has zero morphisms (as indicated by `CategoryTheory.Limits.HasZeroMorphisms C`), for any objects `X`, `Y`, and `Z` in the category `C`, and for any morphism `f` from `Y` to `Z`, the composition of the zero morphism (denoted as `0`) and `f` is the zero morphism. This can be seen as a property of the zero morphism, which, when composed with any other morphism, results in the zero morphism.
More concisely: For any category with zero morphisms, the composition of a zero morphism with any other morphism is the zero morphism.
|
CategoryTheory.Limits.zero_of_comp_mono
theorem CategoryTheory.Limits.zero_of_comp_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [inst_2 : CategoryTheory.Mono g],
CategoryTheory.CategoryStruct.comp f g = 0 → f = 0
This theorem is about the zero morphisms and monomorphisms in a category. Specifically, for any category 'C' with zero morphisms and given objects 'X', 'Y', and 'Z' in 'C', it states that if 'f' is a morphism from 'X' to 'Y' and 'g' is a monomorphism from 'Y' to 'Z', then if the composition of 'f' and 'g' is a zero morphism, 'f' must also be a zero morphism. In other words, if composing 'f' with a monomorphism results in a zero morphism, 'f' itself must be a zero morphism.
More concisely: If `f : X -> Y` is a morphism, `g : Y -> Z` is a monomorphism, and their composition `g ∘ f` is a zero morphism in a category with zero morphisms, then `f` is a zero morphism.
|
CategoryTheory.Limits.comp_zero
theorem CategoryTheory.Limits.comp_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} {f : X ⟶ Y} {Z : C}, CategoryTheory.CategoryStruct.comp f 0 = 0
The theorem `CategoryTheory.Limits.comp_zero` states that for any category `C` which has zero morphisms, given any objects `X`, `Y`, and `Z` in `C` and a morphism `f` from `X` to `Y`, the composition of `f` with the zero morphism from `Y` to `Z` is the zero morphism from `X` to `Z`. This is a formal expression of the fact in category theory that composing any morphism with the zero morphism results in the zero morphism.
More concisely: For any category with zero morphisms, the composition of any morphism with the zero morphism is the zero morphism.
|
CategoryTheory.Limits.zero_of_to_zero
theorem CategoryTheory.Limits.zero_of_to_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : X ⟶ 0), f = 0
This theorem, `CategoryTheory.Limits.zero_of_to_zero`, states that in any category `C` that has a zero object and zero morphisms, any morphism `f` from an object `X` to the zero object is itself a zero morphism. This is a general property in category theory related to zero objects and zero morphisms.
More concisely: In a category with zero object and zero morphisms, any morphism to the zero object is a zero morphism.
|
CategoryTheory.Limits.IsZero.iff_id_eq_zero
theorem CategoryTheory.Limits.IsZero.iff_id_eq_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X : C), CategoryTheory.Limits.IsZero X ↔ CategoryTheory.CategoryStruct.id X = 0
The theorem `CategoryTheory.Limits.IsZero.iff_id_eq_zero` states that for all categories `C` which have zero morphisms, an object `X` is considered a zero object if and only if the identity morphism of `X` is equal to zero. In other words, an object in a category is zero if its identity morphism is a zero morphism.
More concisely: In a category with zero morphisms, an object is a zero object if and only if its identity morphism equals the zero morphism.
|
CategoryTheory.Limits.id_zero
theorem CategoryTheory.Limits.id_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], CategoryTheory.CategoryStruct.id 0 = 0
This theorem, `CategoryTheory.Limits.id_zero`, states that for any category `C` equipped with a zero object and zero morphisms, the identity morphism on the zero object is equal to the zero morphism. More formally, in the context of category theory, given a category `C` that has zero objects (which serve as both initial and terminal objects) and zero morphisms (which serve as both the initial and terminal morphisms), the identity morphism on the zero object (represented as `CategoryTheory.CategoryStruct.id 0`) is equal to the zero morphism (represented as `0`).
More concisely: In any category with zero objects and zero morphisms, the identity morphism on the zero object is equal to the zero morphism.
|
CategoryTheory.Limits.unop_zero
theorem CategoryTheory.Limits.unop_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : Cᵒᵖ), 0.unop = 0
This theorem states that in any category `C` (of type `u` and category structure `v`) which has zero morphisms, for any two objects `X` and `Y` in the opposite category `Cᵒᵖ`, the unop of the zero morphism is zero. Here, `unop` is an operation that switches an object or morphism from the opposite category back to the original category.
More concisely: In any category with zero morphisms, the unop of the zero morphism between any two objects is the identity morphism. (Note: In the context of the given theorem, "unop of the zero morphism" means the morphism obtained by switching the zero morphism from the opposite category back to the original category.)
|