CategoryTheory.NormalEpi.w
theorem CategoryTheory.NormalEpi.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [self : CategoryTheory.NormalEpi f],
CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g f = 0
This theorem states that for any category `C` with zero morphisms, and any morphisms `f` from object `X` to `Y` in `C` that is a normal epimorphism (which, by definition, is a morphism that is the cokernel of some other morphism), the composition of `CategoryTheory.NormalEpi.g` (which is a morphism from `CategoryTheory.NormalEpi.W f` to `X`) and `f` is a zero morphism. In mathematical terms, it is saying that if `f` is a normal epimorphism, then `g ∘ f = 0`, where `g` is `CategoryTheory.NormalEpi.g` and `0` represents the zero morphism.
More concisely: If `f` is a normal epimorphism in a category with zero morphisms, then `CategoryTheory.NormalEpi.g ∘ f = 0`, where `g` is the morphism associated with the cokernel of `f`.
|
CategoryTheory.NormalMono.w
theorem CategoryTheory.NormalMono.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [self : CategoryTheory.NormalMono f],
CategoryTheory.CategoryStruct.comp f CategoryTheory.NormalMono.g = 0
The theorem `CategoryTheory.NormalMono.w` states that in any category `C` that has zero morphisms, for any objects `X` and `Y` in `C` and any morphism `f` from `X` to `Y` that is a normal monomorphism (which by definition is a morphism that is the kernel of some morphism), the composition of `f` and `CategoryTheory.NormalMono.g` (where `CategoryTheory.NormalMono.g` is another morphism related to `f`) equals the zero morphism. In mathematical terms, it says that if `f: X ⟶ Y` is a normal monomorphism, then `f ∘ g = 0`, where `g` is the morphism associated with `f` in the structure of a normal monomorphism.
More concisely: In any category with zero morphisms, a normal monomorphism's composition with its associated morphism is the zero morphism.
|