CochainComplex.HomComplex.Cochain.ext₀
theorem CochainComplex.HomComplex.Cochain.ext₀ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0),
(∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯) → z₁ = z₂
The theorem named `CochainComplex.HomComplex.Cochain.ext₀` states that for any category `C` that is pre-additive, and for any two cochain complexes `F` and `G` over `C`, if we have two zero-degree cochains `z₁` and `z₂` from `F` to `G`, then `z₁` is equal to `z₂` if and only if their morphisms `z₁.v p p` and `z₂.v p p` are equal for all integers `p`. In other words, two zero-degree cochains between the same pair of cochain complexes are considered identical if they correspond to the same family of morphisms.
More concisely: For any pre-additive category $C$, two zero-degree cochains between cochain complexes $F$ and $G$ over $C$ are equal if and only if their corresponding morphisms agree at all degrees.
|
CochainComplex.HomComplex.Cocycle.ext
theorem CochainComplex.HomComplex.Cocycle.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n), ↑z₁ = ↑z₂ → z₁ = z₂
This theorem states that given a category `C` that is also preadditive, two cochain complexes `F` and `G` over integers, and an integer `n`, if two `n`-cocycles `z₁` and `z₂` in the homology complex of `F` and `G` are equal as elements of the underlying type (i.e., their coerced forms `↑z₁` and `↑z₂` are equal), then the original cocycles `z₁` and `z₂` themselves are also equal. This basically asserts that the embedding of cocycles into the larger type is injective, or in other words, no two distinct cocycles get identified under this embedding.
More concisely: In a preadditive category `C` with integer-valued cohomology, equal underlying cohomology classes of degree `n` cocycles in complexes `F` and `G` imply equal cocycles.
|
CochainComplex.HomComplex.Cochain.ofHoms_v
theorem CochainComplex.HomComplex.Cochain.ofHoms_v :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p : ℤ),
(CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p
The theorem `CochainComplex.HomComplex.Cochain.ofHoms_v` states that for any Category `C` with Preadditive structure, and for any two Cochain Complexes `F` and `G` on `C` indexed by integers, given a family of morphisms `ψ` from the `p`th object of `F` to the `p`th object of `G` where `p` is an integer, the value of the `v` method on the `p`-degree cochain constructed from `ψ` is equal to the original morphism `ψ p`. This provides a method for constructing cochains in the homology complex of two cochain complexes.
More concisely: For any two cochain complexes F and G over a preadditive category C, and a family of morphisms ψ between their p-th objects, the p-degree cochain constructed from ψ in the hom complex of Hom(F, G) is equal to ψ itself.
|
CochainComplex.HomComplex.Cochain.ofHom_zero
theorem CochainComplex.HomComplex.Cochain.ofHom_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
(F G : CochainComplex C ℤ), CochainComplex.HomComplex.Cochain.ofHom 0 = 0
This theorem states that for any given category `C` (where `C` is preadditive) and any two cochain complexes `F` and `G` over `C` with integer indexing, the `0`-cochain attached to the zero morphism between these cochain complexes is also a zero morphism. This reflects the property in homological algebra that applying a zero morphism in a chain complex yields a zero morphism.
More concisely: In a preadditive category `C`, the 0-cochain of the zero morphism between two cochain complexes `F` and `G` over `C` with integer indexing is the identity morphism. (This is equivalent to stating that the application of a zero morphism in a cochain complex results in a cochain of zeros.)
|
CochainComplex.HomComplex.Cochain.ext
theorem CochainComplex.HomComplex.Cochain.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n),
(∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq) → z₁ = z₂
This theorem states that for any category 'C' that is preadditive, given two cochain complexes 'F' and 'G' over 'C' and an integer 'n', if we have two cochains 'z₁' and 'z₂' from 'F' to 'G' of degree 'n', then 'z₁' equals 'z₂' if and only if for all pairs of integers 'p' and 'q' for which 'p + n = q', the morphism from 'F.X p' to 'G.X q' in 'z₁' is equal to the corresponding morphism in 'z₂'. This is essentially a uniqueness statement about cochains in a cochain complex in the setting of category theory.
More concisely: Given two cochain complexes over a preadditive category and an integer, two cochain morphisms of degree n are equal if and only if their corresponding morphisms between degree p and q (p = n+q) are equal.
|
CochainComplex.HomComplex.Cochain.comp_zero_cochain_v
theorem CochainComplex.HomComplex.Cochain.comp_zero_cochain_v :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n)
(z₂ : CochainComplex.HomComplex.Cochain G K 0) (p q : ℤ) (hpq : p + n = q),
(z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q ⋯)
This theorem in Lean 4 states that for any category C with preadditive structure and for any three cochain complexes F, G, and K over C, along with an integer n, if there exist two cochains: z1 from F to G of degree n, and z2 from G to K of degree 0, then for any two integers p and q such that p + n equals q, the value at (p, q) for the composition of z1 and z2 is equal to the composition of the values at (p, q) and (q, q) for z1 and z2 respectively. This intuitively represents the idea that the composition of cochain morphisms in a cochain complex corresponds to the composition of the individual morphisms they represent.
More concisely: For any cochain complexes F, G, K in a preadditive category C and integer n, if there exist cochains z1: F[n] -> G[0] and z2: G[0] -> K[n], then for all integers p and q with p + n = q, z1 ∘ z2(p) = z1(p) ∘ z2(q).
|
CochainComplex.HomComplex.Cochain.ofHom_v
theorem CochainComplex.HomComplex.Cochain.ofHom_v :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ), (CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p
This theorem states that for any category `C` with preadditive structure, and for any two cochain complexes `F` and `G` over `C` with integer indexing, if we have a morphism `φ` from `F` to `G`, then the value function `.v` of the `0`-cochain attached to `φ`, when applied to any integer `p` twice, is equal to the application of `φ.f` to `p`. In other words, the `0`-cochain of a morphism between two cochain complexes perfectly encapsulates the morphism's action on each integer index.
More concisely: For any morphism φ between cochain complexes F and G over a preadditive category C with integer indexing, the value of φ's 0-cochain at an integer p is equal to the application of φ.f to p.
|
CochainComplex.HomComplex.Cocycle.mem_iff
theorem CochainComplex.HomComplex.Cocycle.mem_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ} (n m : ℤ),
n + 1 = m →
∀ (z : CochainComplex.HomComplex.Cochain F G n),
z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0
This theorem states that for any category `C` with zero morphisms and any two cochain complexes `F` and `G` over `C`, if we take integers `n` and `m` such that `n + 1 = m`, a cochain `z` of degree `n` from `F` to `G` is a member of the subgroup of cocycles of degree `n` (from `F` to `G`) if and only if the image of `z` under the coboundary map `δ` at degrees `n` and `m` is zero. In other words, a cochain is a cocycle if it is mapped to zero in the cohomology complex.
More concisely: A cochain of degree n in a cochain complex over a category with zero morphisms is a cocycle if and only if its coboundary at degrees n and n+1 is zero.
|
CochainComplex.HomComplex.Cochain.comp_assoc
theorem CochainComplex.HomComplex.Cochain.comp_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
{F G K L : CochainComplex C ℤ} {n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
(z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃)
(h₁₂ : n₁ + n₂ = n₁₂) (h₂₃ : n₂ + n₃ = n₂₃) (h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃),
(z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
This theorem establishes the associativity of the composition of cochains in a cochain complex. Given four cochain complexes F, G, K, L over a category C, and three integer degrees n₁, n₂, n₃ and their sums n₁₂, n₂₃ and n₁₂₃, if we have three cochains z₁, z₂, and z₃ of degrees n₁, n₂, and n₃ respectively, then the composition of z₁ and z₂, followed by the composition with z₃, is the same as the composition of z₁ with the composition of z₂ and z₃. This result holds for any category C that is preadditive (a category with both addition and zero morphisms).
More concisely: Given cochain complexes F, G, K, L and integers n₁, n₂, n₃ in a preadditive category C, the composition of cochains z₁ : F(n₁) → G(n₂), z₂ : G(n₂) → K(n₃), and z₃ : K(n₃) → L(n₁₂₃) satisfies z₁ ∘ z₂ ∘ z₃ = z₁ ∘ (z₂ ∘ z₃).
|
CochainComplex.HomComplex.Cocycle.homOf.proof_1
theorem CochainComplex.HomComplex.Cocycle.homOf.proof_1 : ∀ (i : ℤ), i + 0 = i
This theorem, `CochainComplex.HomComplex.Cocycle.homOf.proof_1`, states that for any integer `i`, adding zero to `i` results in `i` itself. This is essentially the additive identity property, which asserts that the sum of any number and zero is the original number.
More concisely: For all integers i, i + 0 = i.
|
CochainComplex.HomComplex.Triplet.hpq
theorem CochainComplex.HomComplex.Triplet.hpq :
∀ {n : ℤ} (self : CochainComplex.HomComplex.Triplet n), self.p + n = self.q
This theorem, `CochainComplex.HomComplex.Triplet.hpq`, states that for any integer `n` and any object `self` which is an instance of the `CochainComplex.HomComplex.Triplet` class parameterized by `n`, the sum of the value `self.p` and `n` equals the value `self.q`. In other words, in every triplet of the HomComplex in a CochainComplex, the third element (q) is always the sum of the first element (p) and some integer n.
More concisely: For any instance `self` of `CochainComplex.HomComplex.Triplet` of length `n`, `self.p + n = self.q`.
|