HomologicalComplex.Hom.comm
theorem HomologicalComplex.Hom.comm :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
(f : A.Hom B) (i j : ι),
CategoryTheory.CategoryStruct.comp (f.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f.f j)
The theorem `HomologicalComplex.Hom.comm` states that for any category `V` with zero morphisms, any complex shape `c`, any two homological complexes `A` and `B` over `V` with shape `c`, and a morphism `f` from `A` to `B`, for all indices `i` and `j`, the composition of the morphism `f.f i` and the differential `B.d i j` is equal to the composition of the differential `A.d i j` and the morphism `f.f j`. This theorem expresses a fundamental commutativity property in the theory of homological complexes in the category theory context.
More concisely: For any homological complexes A and B over a category with zero morphisms and any morphism f between them, the order of composing their differentials and the morphism f is commutative for all indices, i.e., f.fi * B.dij = A.dij * f.fj.
|
HomologicalComplex.hom_ext
theorem HomologicalComplex.hom_ext :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c}
(f g : C ⟶ D), (∀ (i : ι), f.f i = g.f i) → f = g
This theorem states that for any two morphisms ("f" and "g") between two Homological Complexes ("C" and "D"), in a given category ("V") with a specific complex shape ("c"), if the morphisms "f" and "g" coincide on every index "i" (i.e., `f.f i = g.f i` for all "i"), then the two morphisms "f" and "g" are essentially the same (i.e., `f = g`). The category "V" is assumed to have zero morphisms, which are important in the theory of Homological Complexes.
More concisely: If two morphisms between Homological Complexes in a category with zero morphisms have the same action on every index, then they are equal.
|
CochainComplex.next
theorem CochainComplex.next :
∀ (α : Type u_2) [inst : AddRightCancelSemigroup α] [inst_1 : One α] (i : α), (ComplexShape.up α).next i = i + 1
This theorem, `CochainComplex.next`, states that for any type `α` which has an `AddRightCancelSemigroup` and `One` structure, and for any element `i` of type `α`, the `next` operation of the `ComplexShape.up` on `i` will always yield `i + 1`. In simpler terms, when we move to the 'next' element in the cochain complex structure, we are essentially incrementing the current index by one.
More concisely: For any type `α` with an `AddRightCancelSemigroup` and `One` structure, the operation `next (ComplexShape.up i)` equals `i + One`.
|
ChainComplex.next_nat_zero
theorem ChainComplex.next_nat_zero : (ComplexShape.down ℕ).next 0 = 0
This theorem states that when we consider the "down" direction ComplexShape, which is suitable for homology and in which a morphism `d : X i ⟶ X j` exists only when `i = j + 1`, the "next" index after `0` remains `0`. In other words, if we are at the start (`0`) of a chain complex defined over natural numbers (`ℕ`), the next index, according to the down direction ComplexShape, is also `0`.
More concisely: In the context of a chain complex over natural numbers with the "down" direction, the successor index is equal to zero.
|
CochainComplex.prev_nat_succ
theorem CochainComplex.prev_nat_succ : ∀ (i : ℕ), (ComplexShape.up ℕ).prev (i + 1) = i
The theorem `CochainComplex.prev_nat_succ` states that for any natural number `i`, the function `ComplexShape.prev` applied to the cohomology-appropriate `ComplexShape.up` of natural numbers and the successor of `i` (i.e., `i + 1`) returns `i`. In other words, given a chain complex with natural number indices and a differential going from `X[i]` to `X[i+1]`, when we try to find the predecessor of an index `i + 1`, we will always get `i`. This aligns with the idea that in cohomology, differentials increase the index by one.
More concisely: For any chain complex with natural number indices, `ComplexShape.prev (ComplexShape.up i) = i` for all natural numbers `i`.
|
HomologicalComplex.d_comp_d
theorem HomologicalComplex.d_comp_d :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι),
CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0
This theorem, named "HomologicalComplex.d_comp_d", states that for any category 'V' with zero morphisms, and for any complex shape 'c' in a homological complex 'C', the composition of morphisms from 'i' to 'j' and from 'j' to 'k' (denoted as `C.d i j` and `C.d j k` respectively) is equal to zero. This is a fundamental property in homological algebra, as it reflects the fact that the composition of two consecutive boundary mappings in a chain complex is always zero.
More concisely: In a homological complex with zero morphisms, the composition of two consecutive boundary morphisms is zero.
|
HomologicalComplex.d_comp_d_assoc
theorem HomologicalComplex.d_comp_d_assoc :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι)
{Z : V} (h : C.X k ⟶ Z),
CategoryTheory.CategoryStruct.comp (C.d i j) (CategoryTheory.CategoryStruct.comp (C.d j k) h) =
CategoryTheory.CategoryStruct.comp 0 h
The theorem `HomologicalComplex.d_comp_d_assoc` states that for any type `ι`, category `V` that has zero morphisms, a complex shape `c`, a homological complex `C` of `V` and `c`, and any three objects `i`, `j`, `k` of type `ι` and an object `Z` of type `V`, the composition of the morphism from `i` to `j` (denoted as `C.d i j`) and the composition of the morphism from `j` to `k` (denoted as `C.d j k`) and `h` (from `k` to `Z`) is the same as the composition of the zero morphism and `h`. In other words, the composition of consecutive differential morphisms in a homological complex is zero, which is a key property in homological algebra.
More concisely: For any homological complex `C` in a category `V` with zero morphisms, the composition of consecutive differential morphisms is zero: `C.d i j ∘ C.d j k = 0`.
|
HomologicalComplex.eqToHom_comp_d
theorem HomologicalComplex.eqToHom_comp_d :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i i' j : ι}
(rij : c.Rel i j) (rij' : c.Rel i' j),
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C.d i' j) = C.d i j
This theorem states that in a homological complex `C` of a category `V` with zero morphisms and a complex shape `c`, if two differentials `C.d i j` and `C.d i' j` both exist (i.e., the relations `c.Rel i j` and `c.Rel i' j` are true), then the indices `i` and `i'` must be equal. This means that the differentials only differ by an `eqToHom` morphism. In more concrete terms, the composition of the `eqToHom` morphism and the differential `C.d i' j` is equal to the differential `C.d i j`.
More concisely: In a homological complex of a zero-morphism category with a given complex shape, if two differentials between the same pair of indices exist, then they are equal up to an `eqToHom` morphism.
|
HomologicalComplex.eqToHom_f
theorem HomologicalComplex.eqToHom_f :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
(h : C₁ = C₂) (n : ι), (CategoryTheory.eqToHom h).f n = CategoryTheory.eqToHom ⋯
This theorem, `HomologicalComplex.eqToHom_f`, states that for any type `ι`, any type `V` forming a category with zero morphisms, any `ComplexShape ι`, and any two `HomologicalComplex` objects `C₁` and `C₂` in `V` shaped by `c`, if `C₁` equals `C₂` represented by an equality `h`, then for any `n` in `ι`, the function `f` applied to `n` on the morphism from `C₁` to `C₂` induced by the equality `h` (expressed as `CategoryTheory.eqToHom h`), equals to the morphism induced by some other equality. In other words, the morphism generated by the equality of two homological complexes behaves nicely with the structure of the complexes themselves.
More concisely: Given two equivalent HomologicalComplexes `C₁` and `C₂` in a category `V` with zero morphisms, the induced morphism by the equivalence between them equals the morphism induced by some other equality.
|
HomologicalComplex.comp_f
theorem HomologicalComplex.comp_f :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c}
(f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι),
(CategoryTheory.CategoryStruct.comp f g).f i = CategoryTheory.CategoryStruct.comp (f.f i) (g.f i)
The theorem `HomologicalComplex.comp_f` says that for any category `V` that has zero morphisms, and for any complex shape `c`, if we have three homological complexes `C₁`, `C₂`, and `C₃` over the category `V` with the complex shape `c`, and if `f` is a morphism from `C₁` to `C₂` and `g` is a morphism from `C₂` to `C₃`, then the composition of `f` and `g` at an index `i` is the same as the composition of `f` at index `i` and `g` at index `i`. In other words, the composition operation for morphisms in a homological complex is compatible with the indexing operation.
More concisely: For any homological complexes $C\_1$, $C\_2$, $C\_3$ over a category with zero morphisms and complex shape $c$, and morphisms $f : C\_1 \to C\_2$ and $g : C\_2 \to C\_3$ in degree $i$, we have $g \circ f = f \circ_i g$, where $f \circ_i g$ denotes the composition of $f$ and $g$ at index $i$.
|
CochainComplex.prev_nat_zero
theorem CochainComplex.prev_nat_zero : (ComplexShape.up ℕ).prev 0 = 0
The theorem `CochainComplex.prev_nat_zero` states that for the `ComplexShape.up` shape, which is appropriate for cohomology and where the morphism `d : X i ⟶ X j` is only defined when `j = i + 1`, the "previous" index of 0, as defined by the `ComplexShape.prev` function, is 0. This is consistent with the idea that the `ComplexShape.up` shape is modeling cohomology, where there is no "previous" index for the starting point 0.
More concisely: For the `ComplexShape.up` shape in Lean 4 cohomology, the `ComplexShape.prev` function returns 0 for the index 0.
|
HomologicalComplex.Hom.comm_assoc
theorem HomologicalComplex.Hom.comm_assoc :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
(f : A.Hom B) (i j : ι) {Z : V} (h : B.X j ⟶ Z),
CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (B.d i j) h) =
CategoryTheory.CategoryStruct.comp (A.d i j) (CategoryTheory.CategoryStruct.comp (f.f j) h)
The theorem `HomologicalComplex.Hom.comm_assoc` states that for any type `ι`, any category `V` that has zero morphisms, any `ComplexShape` `c`, any two `HomologicalComplex` `A` and `B` over `V` and `c`, any `HomologicalComplex.Hom` `f` from `A` to `B`, any two elements `i` and `j` of `ι`, and any morphism `h` from `B.X j` to `Z` in `V`, the composition of `f.f i` with the composition of `B.d i j` and `h` is equal to the composition of `A.d i j` with the composition of `f.f j` and `h`.
In other words, this theorem is stating a form of the associativity of composition for morphisms in a homological complex in the context of category theory.
More concisely: For any homological complexes A, B over a category V with zero morphisms and any morphism f: A → B, the composition of f with the chain map D (g, h) = g ∘ h between two consecutive complex maps g: B(i) → B(j) and h: B(j) → Z is equal to the chain map D (h, f) = h ∘ f between A(i) and Z: D(f, B.d(i,j) ∘ h) = D(h, f) ∘ A.d(i,j).
|
ChainComplex.prev
theorem ChainComplex.prev :
∀ (α : Type u_2) [inst : AddRightCancelSemigroup α] [inst_1 : One α] (i : α),
(ComplexShape.down α).prev i = i + 1
The theorem `ChainComplex.prev` states that for any type `α` with `AddRightCancelSemigroup` and `One` instances and any element `i` of type `α`, the previous element in the `ComplexShape` defined by `ComplexShape.down α` is `i + 1`. In other words, if we consider a "chain complex" with indices in `α` and with a shape determined by `ComplexShape.down`, then the element before any element `i` is always `i + 1`. It is pertinent to note that this theorem reflects the fundamental concept in homology where the differential operator maps `X i` to `X j` only when `i = j + 1`.
More concisely: For any type `α` with `AddRightCancelSemigroup` and `One` instances, in the complex shape `ComplexShape.down α`, the previous element to `i` is `i + 1`.
|
HomologicalComplex.id_f
theorem HomologicalComplex.id_f :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι),
(CategoryTheory.CategoryStruct.id C).f i = CategoryTheory.CategoryStruct.id (C.X i)
This theorem states that for any type `ι`, any category `V` with zero morphisms, any complex shape `c`, any homological complex `C` of type `V` and shape `c`, and any object `i` of type `ι`, the morphism `f` of the identity morphism on the homological complex `C` at index `i` is equal to the identity morphism on the object at index `i` in the homological complex `C`. In other words, it confirms that the identity morphism on a homological complex respects the identity morphisms on its constituent objects.
More concisely: For any homological complex `C` in a zero-morphism category `V` and type `ι`, the identity morphism on the object `i` in `C` is equal to the identity morphism of the complex `C` at index `i`.
|
HomologicalComplex.zero_f
theorem HomologicalComplex.zero_f :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C D : HomologicalComplex V c) (i : ι),
HomologicalComplex.Hom.f 0 i = 0
This theorem states that for any category `V` with zero morphisms and any `ComplexShape` `c`, for any two homological complexes `C` and `D` over `V` and `c`, and any object `i` in the indexing category `ι`, the morphism `f` at `i` of the zero homological complex is always equal to zero. This essentially asserts the null object property for a homological complex in a category with zero morphisms.
More concisely: For any homological complex `C` and `D` over a category `V` with zero morphisms and any index `i`, the morphism from `C(i)` to `D(i)` in the zero homological complex is the zero morphism.
|
HomologicalComplex.XIsoOfEq.proof_1
theorem HomologicalComplex.XIsoOfEq.proof_1 :
∀ {ι : Type u_2} {V : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p q : ι},
p = q → K.X p = K.X q
This theorem states that for any type `ι`, any category `V` such that `V` is a category with zero morphisms, any complex shape `c`, and any homological complex `K` over `V` and `c`, if two indices `p` and `q` of the homological complex are equal, then the objects of the homological complex at those two indices are also equal. In other words, equality of indices implies equality of corresponding objects in a homological complex.
More concisely: For any homological complex over a zero-morphism category and any equal indices, the corresponding objects are equal.
|
HomologicalComplex.dTo_eq
theorem HomologicalComplex.dTo_eq :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
(r : c.Rel i j), C.dTo j = CategoryTheory.CategoryStruct.comp (C.xPrevIso r).hom (C.d i j)
The theorem `HomologicalComplex.dTo_eq` states that, for any two types `ι` and `V`, given `V` is a category with zero morphisms, and `c` is a complex shape of `ι`, for any homological complex `C` of `V` and `c`, and for any two objects `i` and `j` of type `ι` such that the complex shape `c` establishes a relation `r` between `i` and `j`, the differential mapping into `C.X j` is equal to the composition of the isomorphism from `C.xPrev j` to `C.X i` and the differential mapping from `C.X i` to `C.X j`. In other words, the theorem relates the mapping into a point in a homological complex to the composition of an isomorphism and a differential mapping.
More concisely: For any homological complex over a category with zero morphisms, the differential mapping into a complex's j-th vector is equal to the composition of the isomorphism from the i-th vector to the preceding vector, and the differential mapping from the i-th vector to the j-th vector, for any objects i and j related by the complex's shape.
|
HomologicalComplex.congr_hom
theorem HomologicalComplex.congr_hom :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c}
{f g : C ⟶ D}, f = g → ∀ (i : ι), f.f i = g.f i
This theorem, `HomologicalComplex.congr_hom`, states that for any two homomorphisms `f` and `g` from a homological complex `C` to another homological complex `D` in a category `V` with zero morphisms, if `f` and `g` are the same homomorphism, then for any object `i` in the indexing type `ι`, the component of `f` at `i` is the same as the component of `g` at `i`. This theorem essentially asserts that homomorphisms between homological complexes are determined by their components.
More concisely: Given homological complexes `C` and `D` in a category `V` with zero morphisms, any equal homomorphisms `f` and `g` : `C` --> `D` have equal components `f i` and `g i` for all objects `i` in the indexing type `ι`.
|
HomologicalComplex.dTo_comp_dFrom
theorem HomologicalComplex.dTo_comp_dFrom :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι),
CategoryTheory.CategoryStruct.comp (C.dTo j) (C.dFrom j) = 0
The theorem `HomologicalComplex.dTo_comp_dFrom` states that for any type `ι`, type `V` which is a category with zero morphisms, and complex shape `c`, for any homological complex `C` of type `V` with shape `c` and any `j` of type `ι`, the composition of the differential mapping into `C.X j` and the differential mapping out of `C.X j` (denoted as `HomologicalComplex.dTo C j` and `HomologicalComplex.dFrom C j` respectively in Lean 4) is equal to zero. This is a principle in homological algebra that the differential mappings in a chain complex compose to zero, which is encoded in Lean 4 in this theorem.
More concisely: For any homological complex in a category with zero morphisms, the composition of the differential mappings from and into any complex degree is zero.
|
ChainComplex.of_d
theorem ChainComplex.of_d :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
{α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
(d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0)
(j : α), (ChainComplex.of X d sq).d (j + 1) j = d j
This theorem, `ChainComplex.of_d`, is about chain complexes in the context of category theory. Given a category `V` which has zero morphisms, a type `α` (assumed to have addition and cancellation on the right, a unit element, and decidable equality), a mapping `X` from `α` to objects in `V`, and a morphism `d` which maps each element `n` in `α` to a morphism from `X(n+1)` to `X(n)`, such that the composition of `d(n+1)` and `d(n)` equals zero for all `n` in `α`, the theorem states that for any `j` in `α`, the `d` function of the chain complex formed by `X`, `d`, and `sq` from `j+1` to `j` is equal to the original morphism `d(j)`.
More concisely: Given a chain complex (X, d) in a category with zero morphisms, if for all n in the indexing type α, d(n+1) ∘ d(n) = 0, then d(j) = d | (j+1 ↓ j) for any j in α. (Here, d | (j+1 ↓ j) denotes the morphism from X(j+1) to X(j) in the chain complex.)
|
HomologicalComplex.d_comp_eqToHom
theorem HomologicalComplex.d_comp_eqToHom :
∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j j' : ι}
(rij : c.Rel i j) (rij' : c.Rel i j'),
CategoryTheory.CategoryStruct.comp (C.d i j') (CategoryTheory.eqToHom ⋯) = C.d i j
This theorem states that if `C.d i j` and `C.d i j'` are both allowed in a homological complex `C`, then `j` must be equal to `j'`. As a result, any differences between the differentials are due to an `eqToHom` operation. In more mathematical terms, given a category `V` with zero morphisms, a complex shape `c`, and indices `i`, `j`, and `j'` such that the relations `c.Rel i j` and `c.Rel i j'` hold, the composition of the morphism `C.d i j'` with an equality morphism is equal to the morphism `C.d i j`.
More concisely: In a homological complex with zero morphisms, if two differentials `C.d i j` and `C.d i j'` are both defined for an index `i`, then `j` equals `j'`.
|