Constructions on chain homotopies #
Three constructions of chain homotopies: two produce new homotopies from old ones, and the third assembles a null-homotopy from components given all at once.
Homotopy.descCokernel descends a homotopy along a degreewise cokernel. Let p : L ⟶ M exhibit
M in each degree as the cokernel of u : K ⟶ L, and let p' : L' ⟶ M' be any morphism of
complexes. A chain homotopy between morphisms L ⟶ L' whose components send the image of u
into the kernel of p' then descends to a chain homotopy between the induced morphisms M ⟶ M'.
Only the source side is assumed to be a degreewise cokernel; on the target side the hypothesis is
the bare vanishing u.f i ≫ HL.hom i j ≫ p'.f j = 0, which is what the universal property needs.
This is the mechanism behind homotopy invariance of relative homology, where M is the relative
chain complex of a pair, that is, the degreewise cokernel of the chains of the subspace, and the
vanishing holds because the homotopy restricts to the subspace.
Homotopy.idPow iterates a chain homotopy from the identity of K to an endomorphism s: it
exhibits every power sᵐ as homotopic to the identity, through the explicit operator
∑_{k < m} sᵏ ≫ h. Its components are needed, and not just the existence of some homotopy, when
m is allowed to vary from one summand of K to another, as in the proof that small singular
chains for an open cover include as a chain homotopy equivalence.
Homotopy.mkChainComplex builds a null-homotopy of a chain map between ℕ-indexed chain
complexes from its components h n : P.X n ⟶ Q.X (n + 1), given all at once together with the
homotopy identities in degree zero and in positive degrees. It is the non-inductive counterpart of
Mathlib's Homotopy.mkInductive, for the situation where the components are constructed by a
recursion of their own rather than one degree at a time from the previous two.
The components of the chain homotopy that Homotopy.descCokernel obtains on the quotient
complex M.
Equations
- HL.descCokernelHom u p p' hw hp hcomm i j = ↑(CategoryTheory.Limits.CokernelCofork.IsColimit.desc' (hp i) (CategoryTheory.CategoryStruct.comp (HL.hom i j) (p'.f j)) ⋯)
Instances For
A chain homotopy on the total complexes whose components kill the subcomplex after composing
with p' descends to a chain homotopy on the quotient complex M.
Equations
- HL.descCokernel u p p' hw hp hcomm hf hg = { hom := HL.descCokernelHom u p p' hw hp hcomm, zero := ⋯, comm := ⋯ }
Instances For
Iterating a chain homotopy from the identity. If h is a chain homotopy from the identity of
K to a chain endomorphism s, then h.idPow m is a chain homotopy from the identity to the
m-th power of s, whose operator in bidegree (i, j) is ∑_{k < m} (sᵏ)ᵢ ≫ hᵢⱼ.
Equations
- h.idPow m = { hom := fun (i j : ι) => ∑ k ∈ Finset.range m, CategoryTheory.CategoryStruct.comp ((CategoryTheory.End.of s ^ k).f i) (h.hom i j), zero := ⋯, comm := ⋯ }
Instances For
A null-homotopy of a chain map e : P ⟶ Q between ℕ-indexed chain complexes, from its
components h n : P.X n ⟶ Q.X (n + 1) and the homotopy identities e.f 0 = h 0 ≫ d and
e.f (n + 1) = d ≫ h n + h (n + 1) ≫ d. The components are given all at once; compare
Homotopy.mkInductive, which constructs them one degree at a time.
Equations
- One or more equations did not get rendered due to their size.