CategoryTheory.Limits.kernel.lift_ι
theorem CategoryTheory.Limits.kernel.lift_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f k h) (CategoryTheory.Limits.kernel.ι f) =
k
This theorem states that for any category C with zero morphisms, given objects X, Y and W in the category, and a morphism `f` from X to Y that has a kernel, if another morphism `k` from W to X when composed with `f` results in a zero morphism (`k` composed with `f` is `0`), then the composition of the morphism obtained by lifting `k` to the kernel of `f` and the morphism from the kernel of `f` to X is equal to `k`. This essentially says that lifting `k` to the kernel of `f` correctly "undoes" the effect of mapping into the kernel.
More concisely: Given a category with zero morphisms, if a morphism has a kernel and composing it with another morphism results in the zero morphism, then lifting the second morphism to the kernel of the first morphism equals the second morphism.
|
CategoryTheory.Limits.KernelFork.condition
theorem CategoryTheory.Limits.KernelFork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.KernelFork f),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) f = 0
The theorem `CategoryTheory.Limits.KernelFork.condition` states that for any category `C` with zero morphisms, given any objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y`, if `s` is a kernel fork of `f`, then the composition of the fork morphism `ι s` with `f` is a zero morphism. In other words, if we consider a fork in which the second morphism is a zero morphism (a kernel fork), then the composition of the morphism from the source of the fork to `f` is also a zero morphism. This is a key property of kernels in category theory.
More concisely: For any category with zero morphisms, if `s` is a kernel fork of morphism `f`, then `ι s ∘ f` is a zero morphism.
|
CategoryTheory.Limits.kernel.ι_of_mono
theorem CategoryTheory.Limits.kernel.ι_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
[inst_3 : CategoryTheory.Limits.HasKernel f] [inst_4 : CategoryTheory.Mono f],
CategoryTheory.Limits.kernel.ι f = 0
This theorem states that for any categories `C`, with zero morphisms, a zero object and a morphism `f` from objects `X` to `Y` of the category, if `f` is a monomorphism and has a kernel, then the kernel morphism of `f` is a zero morphism. In other words, in a category with zero morphisms and a zero object, the kernel of any monomorphism is a zero morphism.
More concisely: In a category with zero morphisms and a zero object, the kernel of any monomorphism is a zero morphism.
|
CategoryTheory.Limits.cokernel.π_of_epi
theorem CategoryTheory.Limits.cokernel.π_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
[inst_3 : CategoryTheory.Limits.HasCokernel f] [inst_4 : CategoryTheory.Epi f],
CategoryTheory.Limits.cokernel.π f = 0
This theorem states that in any category `C` with zero morphisms and a zero object, if a morphism `f` from `X` to `Y` has a cokernel and is an epimorphism, then the cokernel morphism of `f` is a zero morphism. Simply put, in the context of category theory, the cokernel of an "onto" morphism (or epimorphism) is essentially a "zero" morphism.
More concisely: In any category with zero morphisms and a zero object, the cokernel of an epimorphism is a zero morphism.
|
CategoryTheory.Limits.cokernel.π_of_zero
theorem CategoryTheory.Limits.cokernel.π_of_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : C), CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π 0)
The theorem `CategoryTheory.Limits.cokernel.π_of_zero` states that for any category `C` that has zero morphisms, the cokernel of a zero morphism (which is essentially a map from the target of the zero morphism to the cokernel of the zero morphism) is an isomorphism. In other words, this map has an inverse and it preserves the structure of the category. This is a principle in the realm of category theory, a branch of mathematics that aims to find common patterns in different mathematical structures.
More concisely: The cokernel of a zero morphism in a category with zero morphisms is an isomorphism.
|
CategoryTheory.Limits.cokernel.π_desc
theorem CategoryTheory.Limits.cokernel.π_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
(CategoryTheory.Limits.cokernel.desc f k h) =
k
The theorem `CategoryTheory.Limits.cokernel.π_desc` states that for any category `C` that has zero morphisms, any morphisms `f : X ⟶ Y` and `k : Y ⟶ W` in `C` such that the composition `f ≫ k` equals the zero morphism, the composition of the cokernel projection of `f` with the cokernel description of `f` with respect to `k` and its nullity condition is equal to `k`. In simpler terms, it expresses a property of the cokernel in category theory, specifically that the cokernel description serves as a factorization of the given morphism through the cokernel projection.
More concisely: For any morphism `f : X ⟶ Y` and `k : Y ⟶ W` in a zero-object category `C`, if `f ∘ k` is the zero morphism then the composition of the cokernel projection of `f` with the description of its cokernel with respect to `k` equals `k`.
|
CategoryTheory.Limits.cokernel.π_desc_assoc
theorem CategoryTheory.Limits.cokernel.π_desc_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0) {Z : C} (h_1 : W ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f k h) h_1) =
CategoryTheory.CategoryStruct.comp k h_1
The theorem `CategoryTheory.Limits.cokernel.π_desc_assoc` states that in a category `C` with zero morphisms, for any morphism `f` from object `X` to object `Y` that has a cokernel, and for any morphism `k` from `Y` to an object `W` such that the composition `f` followed by `k` is a zero morphism, then for any object `Z` and any morphism `h_1` from `W` to `Z`, the composition of the cokernel projection of `f` followed by the composition of a morphism (which is described by `k` and makes the diagram commute) and `h_1`, is equal to the composition of `k` followed by `h_1`. In other words, it guarantees the associativity of morphism composition in the context of cokernels.
More concisely: In a category with zero morphisms, for any morphism `f` with cokernel and any morphism `k` such that `f ∘ k` is a zero morphism, the composition of the cokernel projection of `f` with `h ∘ k` equals `h ∘ k`'s composition with the cokernel projection of `h`, for any morphism `h`.
|
CategoryTheory.Limits.kernel.lift_ι_assoc
theorem CategoryTheory.Limits.kernel.lift_ι_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0) {Z : C} (h_1 : X ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f k h)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h_1) =
CategoryTheory.CategoryStruct.comp k h_1
The theorem `CategoryTheory.Limits.kernel.lift_ι_assoc` states that in a category `C` with zero morphisms, for any objects `X`, `Y`, `W`, and `Z`, and for any morphism `f` from `X` to `Y` which has a kernel, there is a morphism `k` from `W` to `X` such that the composition of `k` and `f` is zero. Then for any morphism `h_1` from `X` to `Z`, the composition of `k` and `h_1` is equal to the composition of the lift of `f` with respect to `k` and the composition of the kernel of `f` and `h_1`. This theorem captures the property of kernels in the context of category theory, which reflects the abstract structure of mathematical concepts.
More concisely: For any morphism `f: X -> Y` with kernel in a category `C` with zero morphisms, the composition of the kernel of `f` with any morphism `h_1: X -> Z` equals the composition of the lift of `f` with respect to `h_1` and `k`, where `k` is the morphism from `W` to `X` such that `f ∘ k = 0`.
|
CategoryTheory.Limits.KernelFork.condition_assoc
theorem CategoryTheory.Limits.KernelFork.condition_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.KernelFork f) {Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) (CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.CategoryStruct.comp 0 h
The theorem `CategoryTheory.Limits.KernelFork.condition_assoc` states that for any category `C` that has zero morphisms, given objects `X`, `Y`, and `Z` in the category `C`, a morphism `f` from `X` to `Y`, and a kernel fork `s` of `f`, if we take another morphism `h` from `Y` to `Z`, the composition of the morphism from the fork `s` to `Y` with the composition of `f` and `h` is equal to the composition of the zero morphism and `h`. In mathematical terms, it states that $(\text{Fork}.ι \, s) \circ (f \circ h) = 0 \circ h$.
More concisely: For any category with zero morphisms, given a morphism `f: X → Y`, a kernel fork `s` of `f`, and a morphism `h: Y → Z`, we have `(s ∘ f) ∘ h = 0 ∘ h`.
|
CategoryTheory.Limits.kernel.lift_map
theorem CategoryTheory.Limits.kernel.lift_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') (g' : Y' ⟶ Z')
[inst_3 : CategoryTheory.Limits.HasKernel g'] (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X')
(q : Y ⟶ Y') (r : Z ⟶ Z'),
CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
∀ (h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w)
(CategoryTheory.Limits.kernel.map g g' q r h₂) =
CategoryTheory.CategoryStruct.comp p (CategoryTheory.Limits.kernel.lift g' f' w')
The theorem `CategoryTheory.Limits.kernel.lift_map` states that given a commutative diagram in a category `C` with zero morphisms, where the horizontal arrows compose to zero, i.e.,
```
X --f--> Y --g--> Z
| | |
v v v
X' -f'-> Y' -g'-> Z'
```
we obtain a commutative square involving the kernels of `g` and `g'`
```
X ---> kernel g
| |
v v
X' --> kernel g'
```
This means that if `f` followed by `g` and `f'` followed by `g'` both equal zero (`f ≫ g = 0` and `f' ≫ g' = 0`), and we have morphisms `p : X ⟶ X'`, `q : Y ⟶ Y'` and `r : Z ⟶ Z'` such that `f ≫ q = p ≫ f'` and `g ≫ r = q ≫ g'`, then the compound of `kernel.lift g f w` and `kernel.map g g' q r h₂` equals the compound of `p` and `kernel.lift g' f' w'`. Here `kernel.lift g f w` and `kernel.lift g' f' w'` are morphisms from `X` and `X'` to the kernels of `g` and `g'` respectively (which exist because `g` and `g'` have kernels), and `kernel.map g g' q r h₂` is a morphism from `kernel g` to `kernel g'`.
More concisely: Given a commutative diagram in a category with zero morphisms where the horizontal compositions are zero, the induced morphisms between the kernels commute up to composition with given morphisms from the domain and codomain.
|
CategoryTheory.Limits.cokernel.condition_assoc
theorem CategoryTheory.Limits.cokernel.condition_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {Z : C}
(h : CategoryTheory.Limits.cokernel f ⟶ Z),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h) =
CategoryTheory.CategoryStruct.comp 0 h
The theorem `CategoryTheory.Limits.cokernel.condition_assoc` states that for any category `C` with zero morphisms, given any objects `X`, `Y`, and `Z` in `C`, and a morphism `f` from `X` to `Y` that has a cokernel, if we have a morphism `h` from the cokernel of `f` to `Z`, then the composition of `f` with the composition of the cokernel projection of `f` and `h` is equal to the composition of the zero morphism and `h`. Essentially, this is the associativity condition for the cokernel in the context of category theory.
More concisely: For any object X, Y, Z in a category with zero morphisms and any morphism f : X → Y having a cokernel, the composition of f with h · k, where h is a morphism from the cokernel of f to Z and k is the cokernel projection, equals the composition of the zero morphism with h.
|
CategoryTheory.Limits.π_comp_cokernelComparison
theorem CategoryTheory.Limits.π_comp_cokernelComparison :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
[inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
[inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (G.map f))
(CategoryTheory.Limits.cokernelComparison f G) =
G.map (CategoryTheory.Limits.cokernel.π f)
This theorem, `CategoryTheory.Limits.π_comp_cokernelComparison`, states that for any categories `C` and `D`, where `C` and `D` have zero morphisms, and for any functor `G` from `C` to `D` that preserves zero morphisms, if a morphism `f` from `X` to `Y` in `C` has a cokernel and the same morphism `f` mapped by `G` also has a cokernel in `D`, then the composition of the map from the target of the mapped `f` to its cokernel and the cokernel comparison of `f` and `G` is equal to the map of the cokernel projection of `f` under `G`. In terms of category theory, this is about the commutativity of the cokernel in the presence of a functor that preserves zero morphisms.
More concisely: For functors G between categories C and D preserving zero morphisms, if morphism f in C has a cokernel and G(f) also has a cokernel in D, then the composition of the map from the cokernel of G(f) to its cokernel and the cokernel comparison of f and G is equal to the map of the cokernel projection of f under G.
|
CategoryTheory.Limits.kernel.condition
theorem CategoryTheory.Limits.kernel.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) f = 0
The theorem `CategoryTheory.Limits.kernel.condition` states that for any category `C` with zero morphisms, given any morphisms `f` from object `X` to object `Y` in `C` which has a kernel, the composition of the morphism from the kernel of `f` to `X` with `f` is a zero morphism. In mathematical terms, if `f : X -> Y` is a morphism in a category with zero morphisms and it has a kernel, then the following equation is satisfied: `(kernel.ι f) ∘ f = 0`, where `kernel.ι f` is the morphism from the kernel of `f` to `X`, and `0` represents the zero morphism.
More concisely: If `f : X -> Y` is a morphism in a category with zero morphisms and has a kernel, then the composition of the kernel's inclusion morphism `kernel.ι f` with `f` is the zero morphism.
|
CategoryTheory.Limits.kernel.condition_assoc
theorem CategoryTheory.Limits.kernel.condition_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.CategoryStruct.comp 0 h
The theorem `CategoryTheory.Limits.kernel.condition_assoc` states that for any category `C` with zero morphisms, given objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y` which has a kernel, and for any object `Z` in `C` with a morphism `h` from `Y` to `Z`, the composition of the kernel of `f` with the composition of `f` and `h` equals the composition of the zero morphism and `h`. This theorem is essentially formalising the property that the kernel of a morphism is the equalizer of that morphism and a zero morphism, and the composed morphisms associated with the kernel preserve this equality.
More concisely: For any morphism `f` in a category with zero morphisms having a kernel, and any morphism `h`, the kernel of `f` is the equalizer of `f` and the composition of `h` and `f`, and the zero morphism composed with `h` is also in the equalizer, i.e., (kernel `f`) = (equalizer `(f ∘ h)` ∩ {x | zero `(h x)`}).
|
CategoryTheory.Limits.kernel.ι_of_zero
theorem CategoryTheory.Limits.kernel.ι_of_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : C), CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι 0)
The theorem `CategoryTheory.Limits.kernel.ι_of_zero` states that in a category `C` (which is assumed to be a category with zero morphisms), for any two objects `X` and `Y` in `C`, the kernel morphism of a zero morphism is an isomorphism. In other words, the morphism from the kernel of the zero morphism to the source object `X` is an isomorphism, meaning that it has an inverse morphism. This connects the properties of kernels, zero morphisms, and isomorphisms in the context of category theory.
More concisely: In a category with zero morphisms, the kernel morphism of a zero morphism is an isomorphism.
|
CategoryTheory.Limits.cokernel.condition
theorem CategoryTheory.Limits.cokernel.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f],
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π f) = 0
The theorem `CategoryTheory.Limits.cokernel.condition` states that for any type `C` that has a category structure and zero morphisms, given any objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y` that has a cokernel, the composition of `f` and the map from `Y` to the cokernel of `f` is a zero morphism. This is a generalisation of the algebraic concept of a cokernel, where the composition of the map and the cokernel map is the zero map.
More concisely: For any object `X`, `Y` in a category `C` with zero morphisms and any morphism `f` from `X` to `Y` having a cokernel, the composition `f` ∘ cokernel(`f`) is a zero morphism.
|
CategoryTheory.Limits.CokernelCofork.condition
theorem CategoryTheory.Limits.CokernelCofork.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π s) = 0
The theorem `CategoryTheory.Limits.CokernelCofork.condition` states that for any category `C` that has zero morphisms, and for any objects `X` and `Y` in `C` with a morphism `f` from `X` to `Y`, if `s` is a cokernel cofork of `f`, then the composition of `f` and the cofork projection (`π`) of `s` equals the zero morphism. In other words, in such a category, cokernel coforks have the property that when you follow the morphism `f` and then the morphism `π s`, you end up at the same place as if you had followed the zero morphism.
More concisely: In a category with zero morphisms, the composition of a morphism and its cokernel cofork projection is equal to the zero morphism.
|
CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι
theorem CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : CategoryTheory.Limits.KernelFork f)
{kf' : CategoryTheory.Limits.KernelFork f'} (hf' : CategoryTheory.Limits.IsLimit kf')
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
CategoryTheory.CategoryStruct.comp (kf.mapOfIsLimit hf' φ) (CategoryTheory.Limits.Fork.ι kf') =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) φ.left
This theorem states that given a category `C` with zero morphisms, for any two objects `X, Y` in `C` and a morphism `f` between them, let's say we have a kernel fork `kf` of `f`. Similarly, for any other two objects `X', Y'` in `C` and a morphism `f'` between them, if `kf'` is a kernel fork of `f'` and is a limit, and `φ` is a morphism between the arrows of `f` and `f'`, then the composition of the map of kernel fork `kf` of limit `hf'` with `φ` and the canonical projection `ι` of `kf'` is equal to the composition of the `ι` of `kf` and the left component of `φ`. In other words, this theorem is establishing a commutative property in the context of category theory, specifically around the concept of kernel forks in a category with zero morphisms.
More concisely: Given categories `C` with zero morphisms, kernel forks `kf` and `kf'` of morphisms `f` and `f'` between objects `X, Y` and `X', Y'` respectively, if `kf` is the limit of `f'` and `φ` is a morphism between `f` and `f'`, then the composition of `kf`, `hf'`, `φ`, and `ι` is equal to the composition of `ι` and the left component of `φ`.
|
CategoryTheory.Limits.kernelComparison_comp_ι
theorem CategoryTheory.Limits.kernelComparison_comp_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
[inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
[inst_6 : CategoryTheory.Limits.HasKernel (G.map f)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
(CategoryTheory.Limits.kernel.ι (G.map f)) =
G.map (CategoryTheory.Limits.kernel.ι f)
The theorem `CategoryTheory.Limits.kernelComparison_comp_ι` states that for any categories `C` and `D` with zero morphisms, a morphism `f : X ⟶ Y` in `C`, and a functor `G : C → D` that preserves zero morphisms, if `f` and `G.map f` both have kernels, then the composition of the kernel comparison of `f` under `G` with the kernel injection of `G.map f` is equal to the image under `G` of the kernel injection of `f`. In simpler terms, this theorem describes a certain commutativity condition involving kernels and a functor between categories.
More concisely: For functors preserving zero morphisms between categories with zero morphisms, if a morphism in the source category has a kernel and its image under the functor also has a kernel, then the comparison morphism between their kernel injections is equal to the image under the functor of the kernel injection of the original morphism.
|
CategoryTheory.Limits.cokernel.map_desc
theorem CategoryTheory.Limits.cokernel.map_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z X' Y' Z' : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] (g : Y ⟶ Z)
(w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') [inst_3 : CategoryTheory.Limits.HasCokernel f']
(g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z')
(h₁ : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'),
CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g' →
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map f f' p q h₁)
(CategoryTheory.Limits.cokernel.desc f' g' w') =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f g w) r
This theorem from Category theory, specifically from the subfield of Limit theory, states that given a commutative diagram where `X` maps to `Y` via `f`, `Y` maps to `Z` via `g`, `X'` maps to `Y'` via `f'`, and `Y'` maps to `Z'` via `g'`, such that horizontal arrows compose to zero (representing that the composition of `f` and `g`, and the composition of `f'` and `g'` are both zero), we can create a commutative square involving the cokernels of `f` and `f'`.
This commutative square maps the cokernel of `f` to `Z` and the cokernel of `f'` to `Z'` via `cokernel.map` and `cokernel.desc` respectively. The theorem asserts that the composition of `cokernel.map` and `cokernel.desc` in one path of this square is equal to the composition in the other. This is contingent upon the condition that the composition of `f` and `q` is equal to the composition of `p` and `f'`, and the composition of `g` and `r` is equal to the composition of `q` and `g'`. The theorem is significant since it provides a connection between the original diagram and a derived square involving cokernels.
More concisely: Given commutative diagrams where the horizontal arrows compose to zero, the maps between the cokernels of the horizontal arrows via `cokernel.map` and `cokernel.desc` respectively form a commutative square if and only if the corresponding vertical compositions of arrows are equal.
|