imageSubobjectMap_comp_imageToKernel
theorem imageSubobjectMap_comp_imageToKernel :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} {f : A ⟶ B} [inst_2 : CategoryTheory.Limits.HasImage f] {g : B ⟶ C}
[inst_3 : CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {A' B' C' : V}
{f' : A' ⟶ B'} [inst_4 : CategoryTheory.Limits.HasImage f'] {g' : B' ⟶ C'}
[inst_5 : CategoryTheory.Limits.HasKernel g'] (w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') [inst_6 : CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g'),
α.right = β.left →
CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectMap β) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap α) (imageToKernel f' g' w')
In the context of category theory, the theorem `imageSubobjectMap_comp_imageToKernel` states that, given two pairs of morphisms `f, g` and `f', g'` between objects in a category with zero morphisms such that the composition of `f` and `g` as well as `f'` and `g'` yields a zero morphism (i.e., `f ≫ g = 0` and `f' ≫ g' = 0`), and given compatible commutative squares between these pairs, the `imageToKernel` morphisms interleave the induced map on kernels with the induced map on images. In particular, the composition of the `imageToKernel` morphism of `f` and `g` with the `kernelSubobjectMap` of a morphism `β`, equals the composition of the `imageSubobjectMap` associated with a morphism `α` and the `imageToKernel` morphism of `f'` and `g'`, under the condition that the right side of `α` is equal to the left side of `β`.
More concisely: Given morphisms `f ≫ g = 0` and `f' ≫ g' = 0` in a category with zero morphisms, with compatible commutative squares, the `imageToKernel` morphisms interleave the induced maps on kernels and images: `(imageToKernel f g) ∘ kernelSubobjectMap β = imageSubobjectMap α ∘ (imageToKernel f' g')` whenever `α∘g = β∘f`.
|
homology'.ext
theorem homology'.ext :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C)
[inst_3 : CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0)
[inst_4 : CategoryTheory.Limits.HasCokernel (imageToKernel f g w)] {D : V} {k k' : homology' f g w ⟶ D},
CategoryTheory.CategoryStruct.comp (homology'.π f g w) k =
CategoryTheory.CategoryStruct.comp (homology'.π f g w) k' →
k = k'
This theorem, `homology'.ext`, states that for any category `V` with zero morphisms, given objects `A`, `B`, `C`, and `D` in `V`, a morphism `f` from `A` to `B` with an image, a morphism `g` from `B` to `C` with a kernel, such that the composition of `f` and `g` is zero, and another morphism from `homology' f g w` to `D`, if the composition of the projection from `homology' f g w` to the image of `f` and the kernel of `g` with `k` is equal to the composition of the same projection with `k'`, then `k` is equal to `k'`. This essentially tells us that to check if two morphisms out of a homology object are equal, it is sufficient to check their compositions with the projection from the homology object.
More concisely: Given objects `A`, `B`, `C`, `D` in a zero-morphism category `V`, if morphisms `f: A -> B`, `g: B -> C`, `h: homology' f g w -> D`, `k: Ker g -> A`, and `k': Ker g -> A` satisfy `proj_homology' . f . k = proj_homology' . f . k'`, then `k = k'`, where `proj_homology'` is the projection from the homology object `homology' f g w`.
|
homology'.comp_right_eq_comp_left
theorem homology'.comp_right_eq_comp_left :
∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} V] {A₁ B₁ C₁ A₂ B₂ C₂ A₃ B₃ C₃ : V} {f₁ : A₁ ⟶ B₁}
{g₁ : B₁ ⟶ C₁} {f₂ : A₂ ⟶ B₂} {g₂ : B₂ ⟶ C₂} {f₃ : A₃ ⟶ B₃} {g₃ : B₃ ⟶ C₃}
{α₁ : CategoryTheory.Arrow.mk f₁ ⟶ CategoryTheory.Arrow.mk f₂}
{β₁ : CategoryTheory.Arrow.mk g₁ ⟶ CategoryTheory.Arrow.mk g₂}
{α₂ : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk f₃}
{β₂ : CategoryTheory.Arrow.mk g₂ ⟶ CategoryTheory.Arrow.mk g₃},
α₁.right = β₁.left →
α₂.right = β₂.left →
(CategoryTheory.CategoryStruct.comp α₁ α₂).right = (CategoryTheory.CategoryStruct.comp β₁ β₂).left
This theorem, named `homology'.comp_right_eq_comp_left`, is an auxiliary lemma useful for homology computations in category theory. It states that given a category `V` and a set of objects `A₁, B₁, C₁, A₂, B₂, C₂, A₃, B₃, C₃` within `V`, along with morphisms `f₁, g₁, f₂, g₂, f₃, g₃` between these objects, and morphisms `α₁, β₁, α₂, β₂` between the arrows created by these morphisms, if the right object of the arrow `α₁` is the same as the left object of the arrow `β₁`, and the right object of the arrow `α₂` is the same as the left object of the arrow `β₂`, then the right object of the composition of `α₁` and `α₂` is the same as the left object of the composition of `β₁` and `β₂`.
More concisely: Given morphisms `α₁, β₁, α₂, β₂` in a category `V` such that `α₁: A₁ → C₁`, `β₁: B₁ → C₁`, `α₂: A₂ → B₂`, `β₂: B₂ → C₃`, `f₁: A₁ → A₂`, `g₁: B₁ → B₂`, `f₂: A₂ → C₁`, and `g₂: B₂ → C₃` with `g₁ ∘ f₁ = f₂ ∘ α₁` and `g₂ ∘ β₂ = β₁ ∘ α₂`, then `α₁ ∘ α₂` and `β₁ ∘ β₂` have the same right object in `C₃`.
|
imageToKernel'.proof_1
theorem imageToKernel'.proof_1 :
∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V]
[inst_3 : CategoryTheory.Limits.HasImages V],
CategoryTheory.CategoryStruct.comp f g = 0 →
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g = 0
This theorem states that for any category `V` that has zero morphisms, kernels, and images, given three objects `A`, `B`, and `C` in `V` and two morphisms `f: A ⟶ B` and `g: B ⟶ C`, if the composition of `f` and `g` is a zero morphism (i.e., `f ≫ g = 0`), then the composition of the inclusion of the image of `f` into `B` and `g` is also a zero morphism (i.e., `(CategoryTheory.Limits.image.ι f) ≫ g = 0`). Here, `CategoryTheory.Limits.image.ι f` represents the morphism that includes the image of `f` into `B`.
More concisely: If `f: A ➔ B` and `g: B ➔ C` are morphisms in a category with zero morphisms, kernels, and images, and `f ∘ g = 0`, then `(image.ι f) ∘ g = 0`.
|
imageToKernel_arrow
theorem imageToKernel_arrow :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C)
[inst_3 : CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0),
CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow =
(CategoryTheory.Limits.imageSubobject f).arrow
This theorem, `imageToKernel_arrow`, states that for any three objects `A`, `B`, and `C` in a category `V` with zero morphisms, given a morphism `f` from `A` to `B` that has an image, and a morphism `g` from `B` to `C` that has a kernel, if the composition of `f` and `g` is zero, then the composition of `imageToKernel` of `f` and `g` and the arrow of the kernel subobject `g` equals to the arrow of the image subobject `f`. Essentially, it provides a relation between the kernel of one morphism and the image of another in the context of zero morphisms in a category.
More concisely: Given morphisms `f: A → B` with an image and `g: B → C` with a kernel in a category with zero morphisms, if `f ∘ g = 0`, then `imageToKernel(f) ∘ g = f`.
|
image_le_kernel
theorem image_le_kernel :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C)
[inst_3 : CategoryTheory.Limits.HasKernel g],
CategoryTheory.CategoryStruct.comp f g = 0 →
CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
The theorem `image_le_kernel` states that for any category `V` which has zero morphisms, and any objects `A`, `B` and `C` in `V`, if a morphism `f` from `A` to `B` has an image, and a morphism `g` from `B` to `C` has a kernel, then if the composition of `f` and `g` is a zero morphism (denoted by `f ≫ g = 0`), it implies that the image subobject of `f` is less than or equal to the kernel subobject of `g`. In other words, the theorem states a general property of categories: the image of a morphism is always contained in the kernel of the following morphism when their composition is zero.
More concisely: If in a zero-morphism category V, morphisms f from A to B with image and g from B to C with kernel exist such that f ≫ g = 0, then the image of f is contained in the kernel of g.
|
subobject_ofLE_as_imageToKernel
theorem subobject_ofLE_as_imageToKernel :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{A B C : V} (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C)
[inst_3 : CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0)
(h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g),
(CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
This theorem, called `subobject_ofLE_as_imageToKernel`, states that in any category `V` that has zero morphisms, for any three objects `A`, `B`, `C` in `V`, and any morphisms `f: A ⟶ B` and `g: B ⟶ C`, if the composition `f ≫ g` is zero and the image of `f` is a subobject that is less than or equal to (in the subobject order) the kernel of `g`, then the morphism that makes the image of `f` a subobject of the kernel of `g` is equal to the morphism from the image of `f` to the kernel of `g`. This theorem formalizes one of the key equalities in the definition of the exact sequence in category theory.
More concisely: Given objects A, B, C in a Zero-object category V and morphisms f : A ⟶ B and g : B ⟶ C with image(f) ≤ kernel(g) and composition f ≫ g = 0, the morphism from image(f) to kernel(g) is equal to the morphism making image(f) a subobject of kernel(g).
|