CategoryTheory.ShortComplex.zero_assoc
theorem CategoryTheory.ShortComplex.zero_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(self : CategoryTheory.ShortComplex C) {Z : C} (h : self.X₃ ⟶ Z),
CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp self.g h) =
CategoryTheory.CategoryStruct.comp 0 h
The theorem `CategoryTheory.ShortComplex.zero_assoc` states that for any category `C` with zero morphisms and a `ShortComplex` in that category `C`, for any object `Z` in `C` and a morphism `h` from `self.X₃` to `Z`, the composition of `self.f` with the composition of `self.g` and `h` is equal to the composition of the zero morphism and `h`. This theorem is essentially about the associativity property in the category theory context where the use of zero morphisms is involved.
More concisely: For any category with zero morphisms and a ShortComplex in it, the composition of the zero morphism with a morphism from X₃ to any object is equal to the composition of the zero morphism from X₂ to X₃ with that morphism. (In the context of the theorem, self.f is the morphism from X₂ to X₃ and self.g is the morphism from X₃ to X₂.)
|
CategoryTheory.ShortComplex.Hom.comm₂₃
theorem CategoryTheory.ShortComplex.Hom.comm₂₃ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂),
CategoryTheory.CategoryStruct.comp self.τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g self.τ₃
The theorem `CategoryTheory.ShortComplex.Hom.comm₂₃` states that for any type `C` which is a category and has zero morphisms, and for any two short complexes `S₁` and `S₂` within this category, any morphism `self` from `S₁` to `S₂` satisfies the property that the composition of `self.τ₂` and `S₂.g` is equal to the composition of `S₁.g` and `self.τ₃`. In other words, the theorem asserts the equality of two composed morphisms in the context of a short complex, hence ensuring the right commutative square property of a morphism in the short complex.
More concisely: For any category `C` with zero morphisms and short complexes `S₁` and `S₂`, the composition `S₁.g ∘ self.τ₃` equals `self.τ₂ ∘ S₂.g`.
|
CategoryTheory.ShortComplex.Hom.comm₁₂_assoc
theorem CategoryTheory.ShortComplex.Hom.comm₁₂_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂) {Z : C} (h : S₂.X₂ ⟶ Z),
CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp S₂.f h) =
CategoryTheory.CategoryStruct.comp S₁.f (CategoryTheory.CategoryStruct.comp self.τ₂ h)
The theorem `CategoryTheory.ShortComplex.Hom.comm₁₂_assoc` states that for any category `C` that has zero morphisms, for any two short complexes `S₁` and `S₂` within this category, and for any morphism `h` from `S₂.X₂` to some object `Z` in `C`, the composition of the morphism `self.τ₁` with the composition of `S₂.f` and `h` is equal to the composition of `S₁.f` with the composition of `self.τ₂` and `h`.
In more formal terms, it states that `(self.τ₁ ≫ (S₂.f ≫ h)) = (S₁.f ≫ (self.τ₂ ≫ h))`, where `≫` denotes the composition of morphisms in the category. This theorem asserts the associativity of morphism composition within the context of short complexes in a category.
More concisely: For any category with zero morphisms, the composition of `self.τ₁` with `S₂.f` and any morphism `h` is equal to the composition of `S₁.f` with `self.τ₂` and `h`, i.e., `(self.τ₁ ≫ S₂.f ≫ h) = (S₁.f ≫ self.τ₂ ≫ h)` for short complexes `S₁` and `S₂`.
|
CategoryTheory.ShortComplex.comp_τ₂
theorem CategoryTheory.ShortComplex.comp_τ₂ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
The theorem `CategoryTheory.ShortComplex.comp_τ₂` states that for a category `C` (of a certain type `u_1`) with zero morphisms and for any three short complexes `S₁`, `S₂`, and `S₃` in `C`, the composition of two morphisms `φ₁₂` (from `S₁` to `S₂`) and `φ₂₃` (from `S₂` to `S₃`) has its second homological component (`τ₂`) equal to the composition of the second homological components of `φ₁₂` and `φ₂₃` individually. In other words, (φ₁₂ ∘ φ₂₃).τ₂ = φ₁₂.τ₂ ∘ φ₂₃.τ₂, where "∘" denotes the composition of morphisms.
More concisely: For any three short complexes `S₁`, `S₂`, and `S₃` in a category `C` with zero morphisms, the second homological component of their composition is equal to the composition of their second homological components: (φ₁₂ ∘ φ₂₃).τ₂ = φ₁₂.τ₂ ∘ φ₂₃.τ₂.
|
CategoryTheory.ShortComplex.zero_τ₃
theorem CategoryTheory.ShortComplex.zero_τ₃ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₃ 0 = 0
This theorem states that in the context of Category Theory, given any two short complexes `S₁` and `S₂` in a category `C` that has zero morphisms, the `τ₃` function of the zero object is equal to zero.
More concisely: In the category with zero morphisms, the `τ₃` function of the zero object equals zero for any two short complexes `S₁` and `S₂`.
|
CategoryTheory.ShortComplex.zero
theorem CategoryTheory.ShortComplex.zero :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(self : CategoryTheory.ShortComplex C), CategoryTheory.CategoryStruct.comp self.f self.g = 0
The theorem `CategoryTheory.ShortComplex.zero` states that, for any category `C` that has zero morphisms, in a given 'short complex' structure over `C`, the composition of the two morphisms `f` and `g` in the short complex is a zero morphism. Here a 'short complex' is a specific structure related to Homological Algebra and Category Theory, and a zero morphism is a special kind of morphism in category theory that behaves like the number zero in algebra.
More concisely: In a short complex over a category with zero morphisms, the composition of any two zero morphisms is a zero morphism.
|
CategoryTheory.ShortComplex.zero_τ₂
theorem CategoryTheory.ShortComplex.zero_τ₂ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₂ 0 = 0
This theorem states that in the context of category theory, given any category `C` which has zero morphisms, and any two short complexes `S₁` and `S₂` in `C`, the second boundary map `τ₂` of the zero object is always equal to zero.
More concisely: In any category with zero morphisms, the second boundary map of any short complex at the zero object is equal to the identity morphism, but since the category has zero morphisms, this identity is effectively equal to the zero morphism.
|
CategoryTheory.ShortComplex.comp_τ₃
theorem CategoryTheory.ShortComplex.comp_τ₃ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
The theorem `CategoryTheory.ShortComplex.comp_τ₃` states that for any category `C` that has zero morphisms, and for any three short complexes `S₁`, `S₂`, and `S₃` in this category, the τ₃-component of the composition of two morphisms φ₁₂ from `S₁` to `S₂` and φ₂₃ from `S₂` to `S₃`, denoted `(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃`, is equal to the composition of the τ₃-components of the two morphisms, denoted `CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃`. In other words, the τ₃-component of the composition of two morphisms is the composition of the τ₃-components of the two morphisms.
More concisely: For any category with zero morphisms, the τ₃-component of the composition of two short complex morphisms is equal to the composition of their τ₃-components.
|
CategoryTheory.ShortComplex.comp_τ₁
theorem CategoryTheory.ShortComplex.comp_τ₁ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
(CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
This theorem, `CategoryTheory.ShortComplex.comp_τ₁`, is part of category theory in mathematics. It states that for any category `C`, that has zero morphisms, and any three short complexes `S₁`, `S₂`, and `S₃` in `C`, if there are morphisms `φ₁₂` from `S₁` to `S₂` and `φ₂₃` from `S₂` to `S₃`, then the `τ₁` component of the composition of `φ₁₂` and `φ₂₃` is equal to the composition of the `τ₁` components of `φ₁₂` and `φ₂₃`. In other words, the operation of taking the `τ₁` component commutes with the operation of taking compositions of morphisms.
More concisely: For any category with zero morphisms `C` and short complexes `S₁`, `S₂`, `S₃`, the diagram `τ₁(φ₁₂ ∘ φ₂₃) = τ₁(φ₁₂) ∘ τ₁(φ₂₃)` commutes, where `φ₁₂` is a morphism from `S₁` to `S₂` and `φ₂₃` is a morphism from `S₂` to `S₃`.
|
CategoryTheory.ShortComplex.Hom.comm₂₃_assoc
theorem CategoryTheory.ShortComplex.Hom.comm₂₃_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂) {Z : C} (h : S₂.X₃ ⟶ Z),
CategoryTheory.CategoryStruct.comp self.τ₂ (CategoryTheory.CategoryStruct.comp S₂.g h) =
CategoryTheory.CategoryStruct.comp S₁.g (CategoryTheory.CategoryStruct.comp self.τ₃ h)
The theorem `CategoryTheory.ShortComplex.Hom.comm₂₃_assoc` states that in a given category `C` with zero morphisms, for any two short complexes `S₁` and `S₂` in this category, and any homomorphism `self` between `S₁` and `S₂`, and for any object `Z` in `C` and any morphism `h` from `S₂.X₃` to `Z`, the composition of the morphism `self.τ₂` with the composition of `S₂.g` and `h` is equal to the composition of `S₁.g` with the composition of `self.τ₃` and `h`. This theorem describes a commutative property of morphisms in category theory complex and is part of the framework for working with homological algebra in Lean.
More concisely: For any short complexes $S\_1$, $S\_2$ in a zero-morphism category $C$, and any homomorphism $f$ from $S\_1$ to $S\_2$ and morphism $h$ from $S\_2.X\_3$ to an object $Z$ in $C$, we have $f.τ\_2 \circ S\_2.g \circ h = S\_1.g \circ f.τ\_3 \circ h$.
|
CategoryTheory.ShortComplex.zero_τ₁
theorem CategoryTheory.ShortComplex.zero_τ₁ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S₁ S₂ : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.Hom.τ₁ 0 = 0
This theorem states that for any category `C` with zero morphisms and any two short complexes `S₁` and `S₂` in `C`, the τ₁ morphism of the zero object is equal to zero. Here, `CategoryTheory.ShortComplex` refers to a short exact sequence in the category `C`, `τ₁` is a specific morphism within such a sequence, and `0` represents the zero object in the category.
More concisely: For any short complexes $S\_1$ and $S\_2$ in a category $C$ with zero morphisms, the morphism $\tau\_1$ in their respective short exact sequences is equal to the zero morphism.
|
CategoryTheory.ShortComplex.Hom.comm₁₂
theorem CategoryTheory.ShortComplex.Hom.comm₁₂ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂),
CategoryTheory.CategoryStruct.comp self.τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f self.τ₂
This theorem, named `CategoryTheory.ShortComplex.Hom.comm₁₂`, states that in the context of a category `C`, which has zero morphisms, and given two objects `S₁` and `S₂` of type `ShortComplex C` and a morphism `self` from `S₁` to `S₂`, the composition of `self.τ₁` and `S₂.f` is the same as the composition of `S₁.f` and `self.τ₂`. Here, `self.τ₁` and `self.τ₂` are morphisms associated with `self`, and `S₁.f` and `S₂.f` are specific morphisms associated with `S₁` and `S₂` respectively. This is essentially saying that for these particular morphisms, the square defined by them in the category commutes. That is, two different paths in the category's diagram lead to the same result.
More concisely: In the context of a zero-object category `C` with objects `S₁` and `S₂` in `ShortComplex C`, and a morphism `self : S₁ -> S₂`, the compositions `S₂.f ∘ self.τ₁` and `self.τ₂ ∘ S₁.f` are equal.
|
CategoryTheory.ShortComplex.hom_ext
theorem CategoryTheory.ShortComplex.hom_ext :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (f g : S₁ ⟶ S₂), f.τ₁ = g.τ₁ → f.τ₂ = g.τ₂ → f.τ₃ = g.τ₃ → f = g
This theorem states in the context of category theory that for any category `C` with zero morphisms, and any two short complexes `S₁` and `S₂` within that category, if two morphisms `f` and `g` from `S₁` to `S₂` have the same τ₁, τ₂, and τ₃ components, then `f` and `g` are indeed the same morphism.
More concisely: In the category with zero morphisms `C`, if two complex morphisms `f` and `g` from complex `S₁` to complex `S₂` have equal componentwise truncations `τ₁`, `τ₂`, and `τ₃`, then `f` equals `g`.
|
CategoryTheory.ShortComplex.Hom.ext
theorem CategoryTheory.ShortComplex.Hom.ext :
∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
{S₁ S₂ : CategoryTheory.ShortComplex C} (x y : S₁.Hom S₂), x.τ₁ = y.τ₁ → x.τ₂ = y.τ₂ → x.τ₃ = y.τ₃ → x = y
This theorem states that in a category `C` that has zero morphisms, given any two short complexes `S₁` and `S₂`, if two morphisms `x` and `y` from `S₁` to `S₂` have equal components `τ₁`, `τ₂`, and `τ₃`, then the morphisms `x` and `y` are identical. In other words, a morphism in a short complex is uniquely determined by its components `τ₁`, `τ₂`, and `τ₃`.
More concisely: In a category with zero morphisms, two morphisms between short complexes have equal components if and only if they are identical.
|