CategoryTheory.NormalEpiCategory.mono_of_cancel_zero
theorem CategoryTheory.NormalEpiCategory.mono_of_cancel_zero :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
[inst_4 : CategoryTheory.NormalEpiCategory C] [inst_5 : CategoryTheory.Limits.HasZeroObject C] {X Y : C}
(f : X ⟶ Y),
(∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) → CategoryTheory.Mono f
The given theorem states that in a category `C` (that has zero morphisms, finite coproducts, cokernels, is a normal epi-category, and has a zero object), for any two objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, if the composition of `f` and any morphism `g` from a third object `Z` to `X` results in a zero morphism implies that `g` is a zero morphism, then `f` is a monomorphism. In mathematical terms, if for all `g`: `Z ⟶ X`, `g ≫ f = 0` implies `g = 0`, then `f` is a monomorphism.
More concisely: If in a zero object-preserving category with zero morphisms, finite coproducts, cokernels, and is a normal epi-category, a morphism `f` is a monomorphism if for all morphisms `g`, `g ∘ f = 0` implies `g = 0`.
|
CategoryTheory.NormalMonoCategory.epi_of_zero_cancel
theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cancel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : CategoryTheory.Limits.HasKernels C]
[inst_4 : CategoryTheory.NormalMonoCategory C] [inst_5 : CategoryTheory.Limits.HasZeroObject C] {X Y : C}
(f : X ⟶ Y), (∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) → CategoryTheory.Epi f
This theorem states that in any category `C` that has zero morphisms, finite products, kernels, and is a normal monomorphism category with a zero object, for any objects `X` and `Y` in `C` and morphism `f` from `X` to `Y`, if the composition of `f` and any morphism `g` from `Y` to any object `Z` is zero implies that `g` is zero, then `f` is an epimorphism. In mathematical terms, this means if `f` cancels out everything on the right, it is an epimorphism. An epimorphism, in category theory, is a morphism that is right-cancellable, meaning that for any pair of morphisms `g` and `h` from `Y` to any object `Z`, if `f` followed by `g` equals `f` followed by `h`, then `g` equals `h`.
More concisely: In a category with zero morphisms, finite products, kernels, and a zero object, if a morphism cancels out on the right (i.e., the composition with any morphism to another object is zero implies the morphism is zero) then it is an epimorphism.
|
CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel
theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : CategoryTheory.Limits.HasKernels C]
[inst_4 : CategoryTheory.NormalMonoCategory C] {X Y : C} (f : X ⟶ Y) (Z : C),
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯) → CategoryTheory.Epi f
The theorem `CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel` states that in a category `C` that has zero morphisms, finite products, kernels, and is a normal monomorphism category, if a zero morphism is a cokernel of a morphism `f` from `X` to `Y`, then `f` is an epimorphism.
In other words, if the composite of `f` and a zero morphism results in the zero morphism (which is the defining property of cokernels in the category of abelian groups or modules over a ring), then `f` is a right-cancellable morphism (which is the definition of an epimorphism). This theorem is a part of the category theory branch of mathematics.
More concisely: In a normal monomorphism category with zero morphisms and finite products, if a zero morphism is the cokernel of a morphism, then that morphism is an epimorphism.
|
CategoryTheory.NormalEpiCategory.mono_of_zero_kernel
theorem CategoryTheory.NormalEpiCategory.mono_of_zero_kernel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
[inst_4 : CategoryTheory.NormalEpiCategory C] {X Y : C} (f : X ⟶ Y) (Z : C),
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 ⋯) → CategoryTheory.Mono f
This theorem states that if a zero morphism is a kernel of a morphism `f` in a category `C` that has zero morphisms, finite coproducts, cokernels, and is a normal epimorphic category, then `f` is a monomorphism. More intuitively, in the context of category theory, it asserts that if all paths through `f` starting from a zero object end up at the same place, then `f` is injective in the categorical sense, which means that two different objects in the domain of `f` cannot map to the same object in the codomain of `f`.
More concisely: In a category with zero morphisms, finite coproducts, cokernels, and normal epimorphisms, a zero morphism being a kernel of a morphism implies that morphism is a monomorphism.
|