Exactness from a contracting homotopy up to lower-order terms

A square-zero endomorphism d of a module is exact, ker d ≤ range d, as soon as some h makes d h + h d invertible: d h + h d commutes with d, so its inverse sends cycles to cycles, and every cycle x = (d h + h d) y with d y = 0 is the boundary d (h y) (LinearMap.ker_le_range_of_isUnit). Invertibility holds when d h + h d differs from the identity by a locally nilpotent endomorphism, and on a free module ι →₀ S that is the case when the difference strictly lowers a weight on the basis whose strict order is well-founded (Module.End.exists_pow_apply_eq_zero_of_forall_mem_support_lt, LinearMap.ker_le_range_of_forall_mem_support_lt).

This is the algebraic core of the discrete Morse theory (algebraic Gaussian elimination) used to compute grid homology: h reverses a matching of generators joined by the leading part of d, and the remaining terms of d h + h d - 1 are of lower order for a filtration.

Main results

• LinearMap.ker_le_range_of_isUnit: a square-zero endomorphism d is exact if d h + h d is a unit for some h.
• LinearMap.ker_le_range_of_forall_mem_support_lt: a square-zero endomorphism d of ι →₀ S is exact if d h + h d - 1 strictly lowers a well-founded weight on the basis.
• LinearMap.ker_le_range_of_matching: a square-zero endomorphism of ι →₀ S is exact if its terms of leading (well-founded) weight form a perfect matching of the generators with unit coefficients.

References

The matching criterion is the case of a perfect matching in algebraic discrete Morse theory: E. Sköldberg, Morse theory from an algebraic viewpoint, Trans. Amer. Math. Soc. 358 (2006), and M. Jöllenbeck, V. Welker, Minimal resolutions via algebraic discrete Morse theory, Mem. Amer. Math. Soc. 197 (2009), no. 923.

theorem LinearMap.ker_le_range_of_isUnit {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) (h : M →ₗ[S] M) (hu : IsUnit (d * h + h * d)) : d.ker ≤ d.range

A contracting homotopy up to a unit makes a square-zero endomorphism exact. If d ∘ d = 0 and d h + h d is invertible for some h, then every element of the kernel of d is in its image.

theorem LinearMap.ker_le_range_of_forall_exists_pow_apply_eq_zero {S : Type u_1} {M : Type u_2} [Ring S] [AddCommGroup M] [Module S M] (d : M →ₗ[S] M) (hd : d ∘ₗ d = 0) (h : M →ₗ[S] M) (hν : ∀ (x : M), ∃ (k : ℕ), ((d * h + h * d - 1) ^ k) x = 0) : d.ker ≤ d.range

A square-zero endomorphism d is exact if d h + h d - 1 is locally nilpotent for some h.

theorem LinearMap.ker_le_range_of_forall_mem_support_lt {S : Type u_1} [Ring S] {ι : Type u_3} {α : Type u_4} [LT α] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (hd : d ∘ₗ d = 0) {h : (ι →₀ S) →ₗ[S] ι →₀ S} (w : ι → α) (hw : WellFounded (InvImage (fun (x1 x2 : α) => x1 < x2) w)) (hlow : ∀ (i j : ι), j ∈ ((d * h + h * d - 1) (Finsupp.single i 1)).support → w j < w i) : d.ker ≤ d.range

Exactness from a contracting homotopy up to lower-order terms. A square-zero endomorphism d of ι →₀ S is exact if for some h the endomorphism d h + h d - 1 sends each basis vector into the span of the basis vectors of strictly smaller weight, for a weight w whose strict order w j < w i is well-founded (for instance any weight when ι is finite).

theorem LinearMap.ker_le_range_of_matching {S : Type u_1} [Ring S] {ι : Type u_3} {α : Type u_4} [LT α] (d : (ι →₀ S) →ₗ[S] ι →₀ S) (hd : d ∘ₗ d = 0) (w : ι → α) (hw : WellFounded (InvImage (fun (x1 x2 : α) => x1 < x2) w)) (p : ι → ι) (src : ι → Prop) (hp : Function.Involutive p) (hwp : ∀ (i : ι), w (p i) = w i) (hsrc : ∀ (i : ι), src i ↔ ¬src (p i)) (hcoef : ∀ (i : ι), src i → IsUnit ((d (Finsupp.single i 1)) (p i))) (hsupp : ∀ (i j : ι), j ∈ (d (Finsupp.single i 1)).support → w j < w i ∨ src i ∧ j = p i) : d.ker ≤ d.range

Exactness from a weight-preserving matching of generators. Let d be a square-zero endomorphism of ι →₀ S, where ι is weighted by w with a well-founded strict order w j < w i (for instance any weight when ι is finite), and let p be an involution of ι preserving w that pairs each generator marked as a source with one that is not. Suppose that every term of d strictly lowers the weight, except the term from each source i to its partner p i, whose coefficient is a unit u. Then d is exact: the homotopy h sending each non-source p i to u⁻¹ • i makes d h + h d - 1 strictly lower the weight.

This is algebraic discrete Morse theory in its simplest form, a perfect matching of the generators by the leading part of d.