CategoryTheory.Abelian.Pseudoelement.apply_zero
theorem CategoryTheory.Abelian.Pseudoelement.apply_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
CategoryTheory.Abelian.Pseudoelement.pseudoApply f 0 = 0
This theorem states that for any category `C` (where `C` is a type, and `C` is a category with Abelian properties), and any two objects `P` and `Q` within this category, if you have a morphism `f` from `P` to `Q`, then applying this morphism to the zero pseudoelement of `P` will yield the zero pseudoelement of `Q`. In other words, morphisms in an Abelian category map the zero pseudoelement to the zero pseudoelement.
More concisely: In an Abelian category, for any two objects and any morphism between them, the image of the zero pseudoelement under the morphism is the zero pseudoelement.
|
CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal
theorem CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal :
∀ {R : Type u_1} [inst : CommRing R] {G : ModuleCat R} {x y : CategoryTheory.Over G},
CategoryTheory.Abelian.PseudoEqual G x y → LinearMap.range x.hom = LinearMap.range y.hom
In the category of modules over a commutative ring `R` (denoted `Module R`), the theorem states that if two arrows `x` and `y` from objects to a fixed object `G` are pseudo-equal, then the range of the linear maps associated with `x` and `y` are equal. These arrows `x` and `y` are pseudo-equal if there exists an object `R` and two epimorphisms `p : R ⟶ X` and `q : R ⟶ Y` such that the composition of `p` and `f` equals the composition of `q` and `g`. Here, `x.hom` and `y.hom` refer to the linear maps associated with the arrows `x` and `y`, respectively.
More concisely: If `x` and `y` are arrows in the category of modules over a commutative ring with equal ranges and are pseudo-equal via epimorphisms `p : R ⟶ X` and `q : R ⟶ Y`, then `x.hom` and `y.hom` are equal.
|
CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image
theorem CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
(x y : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply f x = CategoryTheory.Abelian.Pseudoelement.pseudoApply f y →
∃ z,
CategoryTheory.Abelian.Pseudoelement.pseudoApply f z = 0 ∧
∀ (R : C) (g : P ⟶ R),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g y = 0 →
CategoryTheory.Abelian.Pseudoelement.pseudoApply g z =
CategoryTheory.Abelian.Pseudoelement.pseudoApply g x
This theorem is from category theory, specifically from the subfield dealing with Abelian categories. The theorem says that given an Abelian category and two pseudoelements `x` and `y` in the category, if they have the same image under a certain morphism `f`, then it is possible to form a "difference" between them, denoted as `z`. This new pseudoelement `z` possesses two key properties. Firstly, the image of `z` under the morphism `f` is zero. Secondly, for any morphism `g`, if the image of `y` under `g` is zero, then the image of `z` under `g` is the same as the image of `x` under `g`.
More concisely: Given an Abelian category and two pseudoelements `x` and `y` with the same image under a morphism `f`, there exists a pseudoelement `z` such that the image of `z` under `f` is zero, and for any morphism `g`, if the image of `y` under `g` is zero, then the image of `z` under `g` equals the image of `x` under `g`.
|
CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff
theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C}
(a : CategoryTheory.Over P), Quot.mk (CategoryTheory.Abelian.PseudoEqual P) a = 0 ↔ a.hom = 0
The theorem `CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff` states that, for any category `C` that is also an Abelian category and for any object `P` in `C`, the pseudoelement induced by an arrow (represented by `a` in the `Over` category over `P`) is zero if and only if that arrow itself is zero. In other words, in the context of Abelian categories, an arrow is zero if and only if it induces a zero pseudoelement.
More concisely: In an Abelian category, an arrow is a zero morphism if and only if the induced pseudoelement in the over category is the zero pseudoelement.
|
CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjective
theorem CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → CategoryTheory.Epi f
This theorem states that in an Abelian category, if a morphism function, represented by `f : P ⟶ Q`, is surjective on pseudoelements, meaning that for every pseudoelement in the codomain `Q`, there is a pseudoelement in the domain `P` that maps to it by applying `f`, then `f` is an epimorphism. An epimorphism in category theory is a morphism after which all further morphisms uniquely determine each other. The surjectivity of `f` on pseudoelements is captured by the function `Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)`.
More concisely: In an Abelian category, a morphism is an epimorphism if and only if it is surjective on pseudoelements.
|
CategoryTheory.Abelian.Pseudoelement.comp_comp
theorem CategoryTheory.Abelian.Pseudoelement.comp_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
(g : Q ⟶ R),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g ∘ CategoryTheory.Abelian.Pseudoelement.pseudoApply f =
CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g)
The theorem `CategoryTheory.Abelian.Pseudoelement.comp_comp` states that for any category `C` that is both a category and an Abelian category, and for any objects `P`, `Q`, and `R` in `C`, the composition of two functions on pseudoelements, one induced by a morphism `f` from `P` to `Q` and another induced by a morphism `g` from `Q` to `R`, is equal to a function on pseudoelements induced by the composition of the morphisms `f` and `g`. In other words, in the setting of Abelian categories, the operation of composing functions on pseudoelements corresponds to the composition of morphisms in the category.
More concisely: In an Abelian category, the function on pseudoelements induced by the composition of morphisms is equal to the composition of functions on pseudoelements induced by each morphism.
|
CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact
theorem CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} {f : P ⟶ Q}
{g : Q ⟶ R},
CategoryTheory.Exact f g →
(∀ (a : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a) =
0) ∧
∀ (b : CategoryTheory.Abelian.Pseudoelement Q),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g b = 0 →
∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = b
This theorem states that for any category `C` with Abelian structure, if we have an exact sequence of morphisms `f : P ⟶ Q` and `g : Q ⟶ R`, then these morphisms behave exactly on pseudoelements. More explicitly, for every pseudoelement `a` of `P`, the composition `g ∘ f(a)` is null in the category. Additionally, for any pseudoelement `b` of `Q` such that `g(b)` is null, there exists a pseudoelement `a` of `P` such that `f(a)` equals `b`. This theorem essentially extends the properties of exact sequences in Abelian categories to pseudoelements.
More concisely: For any exact sequence of morphisms in an Abelian category, the images of pseudoelements under successive morphisms are null and for any null image of a morphism, there exists a pseudoelement mapping to it.
|
CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact
theorem CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
(g : Q ⟶ R),
((∀ (a : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a) =
0) ∧
∀ (b : CategoryTheory.Abelian.Pseudoelement Q),
CategoryTheory.Abelian.Pseudoelement.pseudoApply g b = 0 →
∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = b) →
CategoryTheory.Exact f g
This theorem states that in the context of a Category Theory with Abelian categories, if two morphisms `f` and `g` are "exact" on pseudoelements, then they are indeed exact. More specifically, for any pseudoelement `a` of `P`, the application of morphism `g` to the result of applying morphism `f` to `a` equals to zero, and for any pseudoelement `b` of `Q`, if applying morphism `g` to `b` results in zero, there exists a pseudoelement `a` such that applying morphism `f` to `a` yields `b`.
More concisely: In the context of Category Theory with Abelian categories, if morphisms `f` and `g` preserve pseudoelements' zero elements, then `g ∘ f` is the zero morphism and for any zero element `b` in the codomain of `g`, there exists a zero element `a` in the domain of `f` such that `f(a) = b`.
|
CategoryTheory.Abelian.Pseudoelement.pseudo_surjective_of_epi
theorem CategoryTheory.Abelian.Pseudoelement.pseudo_surjective_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
[inst_2 : CategoryTheory.Epi f], Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
This theorem states that for any category `C` which is abelian, and any two objects `P` and `Q` within this category, if there is an epimorphism `f` from `P` to `Q`, then the function induced by `f` on the pseudoelements of `P` and `Q` is surjective. In other words, every pseudoelement of `Q` is the image of some pseudoelement of `P` under the function induced by `f`. An epimorphism in category theory is a morphism which is right-cancellative, and the pseudoelements of an object form a set that behaves like the elements of the object, if the object were a set.
More concisely: In an abelian category `C`, every epimorphism `f` from object `P` to object `Q` induces a surjective function on the pseudoelements of `P` and `Q`.
|
CategoryTheory.Abelian.Pseudoelement.comp_apply
theorem CategoryTheory.Abelian.Pseudoelement.comp_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
(g : Q ⟶ R) (a : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g) a =
CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)
This theorem, named `CategoryTheory.Abelian.Pseudoelement.comp_apply`, states that in the category of Abelian categories, for any three objects `P`, `Q`, and `R`, and any two morphisms `f : P ⟶ Q` and `g : Q ⟶ R`, and any pseudoelement `a` of `P`, applying the pseudoelement `a` to the composition of the morphisms `f` and `g` (denoted by `CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g) a`) is equivalent to applying the pseudoelement `a` to the morphism `f` and then applying the result to the morphism `g` (denoted by `CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)`). This shows the compatibility of the operation of applying a pseudoelement with the composition of morphisms. However, this equivalence is not a definitional equality, but a theorem that needs to be proved.
More concisely: In the category of Abelian categories, for any objects P, Q, R and morphisms f : P → Q and g : Q → R, and any pseudoelement a of P, the application of a to the composition of f and g is equivalent to the application of a to f followed by the application of a to g.
|
CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext
theorem CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
(∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) →
f = 0
This theorem, named `CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext`, is an extensionality lemma for zero arrows in category theory. Specifically, it states that for any category `C` that's an Abelian category, and any two objects `P` and `Q` in `C`, if a morphism `f` from `P` to `Q` makes every pseudoelement of `P` map to the zero pseudoelement of `Q` under `pseudoApply f`, then the morphism `f` must be the zero morphism. In other words, a morphism is identified as the zero morphism if it sends all pseudoelements of its domain to the zero pseudoelement of its codomain.
More concisely: In an Abelian category, a morphism between objects is the zero morphism if and only if it maps every pseudoelement of its domain to the zero pseudoelement of its codomain.
|
CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux
theorem CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
(a b : CategoryTheory.Over P), a ≈ b → CategoryTheory.Abelian.app f a ≈ CategoryTheory.Abelian.app f b
The theorem `CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux` states that, given an Abelian category `C` with objects `P` and `Q`, and a morphism `f` from `P` to `Q`, if two objects `a` and `b` from the over category of `P` are pseudo-equal (i.e., they are equivalent in a certain sense), then their compositions with the morphism `f` (i.e., `CategoryTheory.Abelian.app f a` and `CategoryTheory.Abelian.app f b`) are also pseudo-equal. This theorem illustrates the principle that "the composition of equivalent objects with the same morphism preserves equivalence", a key property in category theory.
More concisely: Given an Abelian category and morphism, if two objects are pseudo-equal in the over category, then their compositions with the morphism are also pseudo-equal.
|
CategoryTheory.Abelian.pseudoEqual_trans
theorem CategoryTheory.Abelian.pseudoEqual_trans :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C},
Transitive (CategoryTheory.Abelian.PseudoEqual P)
The theorem `CategoryTheory.Abelian.pseudoEqual_trans` states that the relation of pseudo-equality is transitive in any abelian category. In other words, if we have three objects `X`, `Y`, and `Z` in an abelian category, and arrows `f: X ⟶ P`, `g: Y ⟶ P`, and `h: Z ⟶ P` such that `f` is pseudo-equal to `g` and `g` is pseudo-equal to `h`, then `f` is pseudo-equal to `h`. This is established by taking the pullback. The pullback morphisms will be epimorphisms because, in an abelian category, pullbacks of epimorphisms are epimorphisms.
More concisely: In any abelian category, if two morphisms between objects are pseudo-equal, then so are their compositions.
|
CategoryTheory.Abelian.Pseudoelement.pseudo_pullback
theorem CategoryTheory.Abelian.Pseudoelement.pseudo_pullback :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
[inst_2 : CategoryTheory.Limits.HasPullbacks C] {P Q R : C} {f : P ⟶ R} {g : Q ⟶ R}
{p : CategoryTheory.Abelian.Pseudoelement P} {q : CategoryTheory.Abelian.Pseudoelement Q},
CategoryTheory.Abelian.Pseudoelement.pseudoApply f p = CategoryTheory.Abelian.Pseudoelement.pseudoApply g q →
∃ s,
CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.pullback.fst s = p ∧
CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.pullback.snd s = q
This theorem, named `CategoryTheory.Abelian.Pseudoelement.pseudo_pullback`, states that in a category `C` which has all pullbacks and is also an Abelian category, given morphisms `f : P ⟶ R` and `g : Q ⟶ R` and pseudoelements `p` of `P` and `q` of `Q`, if the application of `f` to `p` equals the application of `g` to `q`, then there exists a pseudoelement `s` of the pullback of `f` and `g` such that the application of the first projection of the pullback to `s` equals `p` and the application of the second projection of the pullback to `s` equals `q`. It's worth noting that although Borceux claims that `s` is unique, this is not true, and counterexamples are provided in `Counterexamples/Pseudoelement.lean`. In simpler terms, if two morphisms map two different pseudoelements to the same place, then there exists a pseudoelement in their pullback that maps to both original pseudoelements.
More concisely: In an Abelian category with pullbacks, given morphisms `f : P ⟶ R` and `g : Q ⟶ R` and pseudoelements `p` of `P` and `q` of `Q` with `f(p) = g(q)`, there exists a pseudoelement `s` in the pullback of `f` and `g` such that `p` maps to `s` along the first projection and `q` maps to `s` along the second projection.
|
CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux
theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C} (Q : C)
(f : CategoryTheory.Over P), f ≈ CategoryTheory.Over.mk 0 ↔ f.hom = 0
This theorem states that within an Abelian category, any arrow (morphism) that is pseudo-equal to a zero morphism is precisely a zero morphism itself. More specifically, for any objects `P` and `Q` in the category, and any morphism `f` from `Q` to `P` (manifested as an object in the over category of `P`), `f` is pseudo-equal to the zero morphism if and only if `f` is actually the zero morphism, i.e., `f.hom = 0`. This result connects the concept of pseudo-equality with the actual equality in the context of zero morphisms in Abelian categories.
More concisely: In an Abelian category, a morphism is pseudo-equal to the zero morphism if and only if it is the zero morphism itself.
|
CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero
theorem CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
(∀ (a : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0) →
CategoryTheory.Mono f
The theorem `CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero` states that, in an Abelian category, given any objects `P` and `Q` and any morphism `f` from `P` to `Q`, if for every pseudoelement `a` of `P`, the application of `f` to `a` results in the zero pseudoelement if and only if `a` is the zero pseudoelement itself, then `f` is a monomorphism. In other words, a morphism which only maps the zero pseudoelement of the domain to the zero pseudoelement of the codomain is a monomorphism in the Abelian category.
More concisely: In an Abelian category, a morphism that maps every zero pseudoelement to the zero pseudoelement is a monomorphism.
|
CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero
theorem CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) →
∀ (a : CategoryTheory.Abelian.Pseudoelement P),
CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0
The theorem `CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero` states that for any category `C` of type `u` with Abelian structure and any two objects `P` and `Q` in `C`, if a morphism `f` from `P` to `Q` is such that it is injective on pseudoelements (meaning that if `f` maps two pseudoelements of `P` to the same pseudoelement of `Q`, then those two pseudoelements must have been the same), then it must only map the zero pseudoelement of `P` to the zero pseudoelement of `Q`. In other words, if a pseudoelement `a` of `P` is mapped to zero by `f`, then `a` must be the zero pseudoelement.
More concisely: If `f` is a morphism in an Abelian category that is injective on pseudoelements, then it maps the zero pseudoelement of its domain to the zero pseudoelement of its codomain.
|
CategoryTheory.Abelian.Pseudoelement.pseudo_injective_of_mono
theorem CategoryTheory.Abelian.Pseudoelement.pseudo_injective_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
[inst_2 : CategoryTheory.Mono f], Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
This theorem states that for any category `C` (given it's an Abelian category), and any two objects `P` and `Q` in this category, if there's a morphism `f` from `P` to `Q` which is a monomorphism (i.e., it satisfies the cancellation property), then the function `pseudoApply` induced by `f` on pseudoelements of the category is injective. Here, injectivity means that if `pseudoApply f` takes two possibly different pseudoelements to the same pseudoelement of `Q`, then these two pseudoelements were actually the same to begin with. In mathematical terms, if for any pseudoelements `a₁` and `a₂` of `P`, `pseudoApply f a₁ = pseudoApply f a₂` implies `a₁ = a₂`.
More concisely: In an Abelian category `C`, if `f` is a monomorphism from object `P` to object `Q`, then the induced function `pseudoApply f` on pseudoelements is injective.
|
CategoryTheory.Abelian.Pseudoelement.zero_apply
theorem CategoryTheory.Abelian.Pseudoelement.zero_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C} (Q : C)
(a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply 0 a = 0
The theorem `CategoryTheory.Abelian.Pseudoelement.zero_apply` states that in any Abelian category `C`, for any objects `P` and `Q` and any pseudoelement `a` of `P`, applying the zero morphism from `P` to `Q` to `a` results in the zero pseudoelement of `Q`. In other words, the zero morphism sends every pseudoelement to the zero pseudoelement.
More concisely: In any Abelian category, the zero morphism maps every pseudoelement to the zero pseudoelement.
|
CategoryTheory.Abelian.Pseudoelement.zero_eq_zero
theorem CategoryTheory.Abelian.Pseudoelement.zero_eq_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C},
⟦CategoryTheory.Over.mk 0⟧ = 0
This theorem states that for any category `C` that is also an Abelian category with objects `P` and `Q`, the equivalence class of the object obtained by using the `CategoryTheory.Over.mk` constructor on the zero morphism is equal to zero. In simpler words, in any Abelian category, the "over" object corresponding to the zero morphism is also considered as zero.
More concisely: In any Abelian category, the over object of the zero morphism is equal to the zero object.
|