Lemma 11.4: a coefficient criterion for supported representatives

integral-deformations.tex (lem:supported-bockstein): "Let p be a prime, let C^* be a complex of free ℤ/p²-modules, and put C̄^* = C^*/pC^*. Let U ⊆ C² be spanned by a subset of a fixed basis. Assume: (1) the coefficient-inclusion map H²(C̄^*) → H²(C^*), induced by multiplication by p, is zero; (2) every δ̄ ∈ Z¹(C̄^*) has a lift δ ∈ C¹ with dδ ∈ U. Then every class in H²(C̄^*) has a cocycle representative in the image of U/pU."

Formalized on three terms M₁ → M₂ → M₃ of a complex over a commutative ring, with the consequences of freeness used in the proof: the annihilator of p is pM on M₂ and M₃, and U ∩ pM₂ = pU. A class of C̄ is represented by z ∈ M₂ with dz ∈ pM₃; its representative is u ∈ U with du ∈ pM₃ and z − u ∈ d(M₁) + pM₂.

theorem MultiplicativeBasisDeformations.supported_bockstein {R : Type u_1} [CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] (p : R) (d₁ : M₁ →ₗ[R] M₂) (d₂ : M₂ →ₗ[R] M₃) (hdd : ∀ (m : M₁), d₂ (d₁ m) = 0) (U : Submodule R M₂) (hann₂ : ∀ (m : M₂), p • m = 0 → ∃ (m' : M₂), m = p • m') (hann₃ : ∀ (m : M₃), p • m = 0 → ∃ (m' : M₃), m = p • m') (hU : ∀ (m : M₂), p • m ∈ U → ∃ u ∈ U, p • m = p • u) (h1 : ∀ (z : M₂), (∃ (w : M₃), d₂ z = p • w) → ∃ (δ : M₁), p • z = d₁ δ) (h2 : ∀ (δ : M₁), (∃ (m : M₂), d₁ δ = p • m) → ∃ (ε : M₁), d₁ (δ + p • ε) ∈ U) (z : M₂) (hz : ∃ (w : M₃), d₂ z = p • w) : ∃ u ∈ U, (∃ (w : M₃), d₂ u = p • w) ∧ ∃ (δ : M₁) (m : M₂), z - u = d₁ δ + p • m

Lemma 11.4 (lem:supported-bockstein).