Lemma 10.4 for free ℤ/p²-modules

lem:supported-bockstein (integral-deformations.tex) as stated: C^* a complex of free ℤ/p²-modules and U ⊆ C² spanned by a subset of a fixed basis. The consequences of freeness used by supported_bockstein hold: the annihilator of p is pM (ann_p_free), and U ∩ pC² = pU (smul_mem_span_image). So the lemma holds as stated (supported_bockstein_free).

def MultiplicativeBasisDeformations.divP (p : ℕ) (x : ZMod (p ^ 2)) : ZMod (p ^ 2)

Division by p on representatives.

theorem MultiplicativeBasisDeformations.divP_zero (p : ℕ) [hp : Fact (Nat.Prime p)] : divP p 0 = 0

theorem MultiplicativeBasisDeformations.eq_p_mul_divP (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ZMod (p ^ 2)) (hx : ↑p * x = 0) : x = ↑p * divP p x

In ℤ/p², an element killed by p is p times its quotient by p.

theorem MultiplicativeBasisDeformations.ann_p_free (p : ℕ) [hp : Fact (Nat.Prime p)] {M : Type u_1} [AddCommGroup M] [Module (ZMod (p ^ 2)) M] [Module.Free (ZMod (p ^ 2)) M] (m : M) (hm : ↑p • m = 0) : ∃ (m' : M), m = ↑p • m'

In a free ℤ/p²-module the annihilator of p is pM.

theorem MultiplicativeBasisDeformations.smul_mem_span_image (p : ℕ) [hp : Fact (Nat.Prime p)] {M : Type u_1} [AddCommGroup M] [Module (ZMod (p ^ 2)) M] {ι : Type u_2} (b : Module.Basis ι (ZMod (p ^ 2)) M) (S : Set ι) (m : M) (hm : ↑p • m ∈ Submodule.span (ZMod (p ^ 2)) (⇑b '' S)) : ∃ u ∈ Submodule.span (ZMod (p ^ 2)) (⇑b '' S), ↑p • m = ↑p • u

U ∩ pM = pU for U spanned by part of a basis.

theorem MultiplicativeBasisDeformations.supported_bockstein_free (p : ℕ) [hp : Fact (Nat.Prime p)] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [AddCommGroup M₁] [Module (ZMod (p ^ 2)) M₁] [AddCommGroup M₂] [Module (ZMod (p ^ 2)) M₂] [AddCommGroup M₃] [Module (ZMod (p ^ 2)) M₃] [Module.Free (ZMod (p ^ 2)) M₂] [Module.Free (ZMod (p ^ 2)) M₃] (d₁ : M₁ →ₗ[ZMod (p ^ 2)] M₂) (d₂ : M₂ →ₗ[ZMod (p ^ 2)] M₃) (hdd : ∀ (m : M₁), d₂ (d₁ m) = 0) {ι : Type u_5} (b : Module.Basis ι (ZMod (p ^ 2)) M₂) (S : Set ι) (h1 : ∀ (z : M₂), (∃ (w : M₃), d₂ z = ↑p • w) → ∃ (δ : M₁), ↑p • z = d₁ δ) (h2 : ∀ (δ : M₁), (∃ (m : M₂), d₁ δ = ↑p • m) → ∃ (ε : M₁), d₁ (δ + ↑p • ε) ∈ Submodule.span (ZMod (p ^ 2)) (⇑b '' S)) (z : M₂) (hz : ∃ (w : M₃), d₂ z = ↑p • w) : ∃ u ∈ Submodule.span (ZMod (p ^ 2)) (⇑b '' S), (∃ (w : M₃), d₂ u = ↑p • w) ∧ ∃ (δ : M₁) (m : M₂), z - u = d₁ δ + ↑p • m

Lemma 10.4 (lem:supported-bockstein) as stated: for a complex M₁ → M₂ → M₃ of free ℤ/p²-modules (the terms C¹ → C² → C³) and U spanned by a subset S of a basis of C², if (1) multiplication by p kills the classes of H²(C̄) in H²(C), and (2) every cocycle of C̄¹ lifts to δ with dδ ∈ U, then every class of H²(C̄) (a z with dz ∈ pC³) has a representative u ∈ U (with du ∈ pC³ and z − u ∈ dC¹ + pC²).