Lifting a graded module to ℤ/4 (Proposition 10.1)

integral-deformations.tex: "Lift the action matrices arbitrarily to free graded 𝒪-modules. Their associativity defect is even. Division by two, followed by reduction, gives an Ext² class of degree zero. … Since (2𝒪)² = 0, this single correction makes the action associative."

For a graded Λ-module M with a homogeneous basis β and Ext²_0(M, M) = 0, the free module ι → 𝒪 carries a graded Λ̃-action lifting that of M (exists_liftMod). The unit is automatic: the action of 1 is an idempotent congruent to the identity.

The free lift of a graded module with a homogeneous basis

def MultiplicativeBasisDeformations.WLift.grF {ι : Type u_4} [Fintype ι] (dβ : ι → ℤ) : GExt.ZGr (ι → ZMod 4)

The grading of ι → 𝒪 by the degrees of the basis.

theorem MultiplicativeBasisDeformations.WLift.grF_isHom {ι : Type u_4} [Fintype ι] [DecidableEq ι] (dβ : ι → ℤ) {p : ℤ} {m : ι → ZMod 4} : (grF dβ).IsHom p m ↔ ∀ (i : ι), dβ i ≠ p → m i = 0

noncomputable def MultiplicativeBasisDeformations.WLift.ρF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] (β : Module.Basis ι (ZMod 2) M) : (ι → ZMod 4) →+ M

The reduction ι → 𝒪 → M.

theorem MultiplicativeBasisDeformations.WLift.ρF_apply {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (m : ι → ZMod 4) : (ρF β) m = ∑ i : ι, Z4.red (m i) • β i

theorem MultiplicativeBasisDeformations.WLift.ρF_eq_equivFun {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (m : ι → ZMod 4) : (ρF β) m = β.equivFun.symm fun (i : ι) => Z4.red (m i)

theorem MultiplicativeBasisDeformations.WLift.ρF_smul {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (a : ZMod 4) (m : ι → ZMod 4) : (ρF β) (a • m) = Z4.red a • (ρF β) m

theorem MultiplicativeBasisDeformations.WLift.ρF_single {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (i : ι) (a : ZMod 4) : (ρF β) (Pi.single i a) = Z4.red a • β i

noncomputable def MultiplicativeBasisDeformations.WLift.lv {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} (β : Module.Basis ι (ZMod 2) M) (m : M) : ι → ZMod 4

The coordinatewise lift.

theorem MultiplicativeBasisDeformations.WLift.ρF_lv {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (m : M) : (ρF β) (lv β m) = m

theorem MultiplicativeBasisDeformations.WLift.repr_eq_zero_of_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p : ℤ} {m : M} (hm : MM.gr.IsHom p m) {i : ι} (hi : dβ i ≠ p) : (β.repr m) i = 0

theorem MultiplicativeBasisDeformations.WLift.lv_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p : ℤ} {m : M} (hm : MM.gr.IsHom p m) : (grF dβ).IsHom p (lv β m)

theorem MultiplicativeBasisDeformations.WLift.ρF_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p : ℤ} {m : ι → ZMod 4} (hm : (grF dβ).IsHom p m) : MM.gr.IsHom p ((ρF β) m)

theorem MultiplicativeBasisDeformations.WLift.ρF_eq_zero {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m : ι → ZMod 4} (h : (ρF β) m = 0) (i : ι) : Z4.red (m i) = 0

theorem MultiplicativeBasisDeformations.WLift.ker_ρF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m : ι → ZMod 4} (h : (ρF β) m = 0) : ∃ (m' : ι → ZMod 4), m = 2 • m'

theorem MultiplicativeBasisDeformations.WLift.ann_ρF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m : ι → ZMod 4} (h : 2 • m = 0) : (ρF β) m = 0

Twice and half on the free lift

noncomputable def MultiplicativeBasisDeformations.WLift.twF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} (β : Module.Basis ι (ZMod 2) M) : M →+ ι → ZMod 4

Twice a lift: v ↦ 2ṽ.

theorem MultiplicativeBasisDeformations.WLift.twF_apply {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (v : M) (i : ι) : (twF β) v i = Z4.tw ((β.repr v) i)

theorem MultiplicativeBasisDeformations.WLift.twF_eq {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (v : M) : (twF β) v = 2 • lv β v

theorem MultiplicativeBasisDeformations.WLift.ρF_twF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (v : M) : (ρF β) ((twF β) v) = 0

theorem MultiplicativeBasisDeformations.WLift.twF_ρF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (m : ι → ZMod 4) : (twF β) ((ρF β) m) = 2 • m

theorem MultiplicativeBasisDeformations.WLift.twF_smul {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (a : ZMod 4) (v : M) : (twF β) (Z4.red a • v) = a • (twF β) v

theorem MultiplicativeBasisDeformations.WLift.twF_injective {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) : Function.Injective ⇑(twF β)

noncomputable def MultiplicativeBasisDeformations.WLift.halfF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] (β : Module.Basis ι (ZMod 2) M) (m : ι → ZMod 4) : M

Half on the kernel of the reduction.

theorem MultiplicativeBasisDeformations.WLift.twF_halfF {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m : ι → ZMod 4} (h : (ρF β) m = 0) : (twF β) (halfF β m) = m

theorem MultiplicativeBasisDeformations.WLift.halfF_eq {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m : ι → ZMod 4} {v : M} (h : (twF β) v = m) : halfF β m = v

theorem MultiplicativeBasisDeformations.WLift.halfF_add {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m n : ι → ZMod 4} (hm : (ρF β) m = 0) (hn : (ρF β) n = 0) : halfF β (m + n) = halfF β m + halfF β n

theorem MultiplicativeBasisDeformations.WLift.halfF_sub {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {m n : ι → ZMod 4} (hm : (ρF β) m = 0) (hn : (ρF β) n = 0) : halfF β (m - n) = halfF β m - halfF β n

theorem MultiplicativeBasisDeformations.WLift.halfF_smul {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (a : ZMod 4) {m : ι → ZMod 4} (hm : (ρF β) m = 0) : halfF β (a • m) = Z4.red a • halfF β m

theorem MultiplicativeBasisDeformations.WLift.halfF_two_smul {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (m : ι → ZMod 4) : halfF β (2 • m) = (ρF β) m

The lifted action

noncomputable def MultiplicativeBasisDeformations.WLift.act0 {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] (π : Λ' →+* Λ) {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] (β : Module.Basis ι (ZMod 2) M) (MM : GExt.GMod GΛ M) {κ : Type u_5} (bΛ : Module.Basis κ (ZMod 4) Λ') : (ι → ZMod 4) →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] ι → ZMod 4

The arbitrary lift of the action matrices, through the bases.

theorem MultiplicativeBasisDeformations.WLift.act0_single {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (i : ι) (κ' : κ) : ((act0 π β MM bΛ) (Pi.single i 1)) (bΛ κ') = lv β ((MM.act (β i)) (π (bΛ κ')))

theorem MultiplicativeBasisDeformations.WLift.act0_apply {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (m : ι → ZMod 4) (b : Λ') : ((act0 π β MM bΛ) m) b = ∑ i : ι, ∑ κ' : κ, (m i * (bΛ.repr b) κ') • lv β ((MM.act (β i)) (π (bΛ κ')))

theorem MultiplicativeBasisDeformations.WLift.π_eq_sum {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (b : Λ') : π b = ∑ κ' : κ, Z4.red ((bΛ.repr b) κ') • π (bΛ κ')

theorem MultiplicativeBasisDeformations.WLift.ρF_act0 {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (m : ι → ZMod 4) (b : Λ') : (ρF β) (((act0 π β MM bΛ) m) b) = (MM.act ((ρF β) m)) (π b)

theorem MultiplicativeBasisDeformations.WLift.act0_twF {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (v : M) (b : Λ') : ((act0 π β MM bΛ) ((twF β) v)) b = (twF β) ((MM.act v) (π b))

theorem MultiplicativeBasisDeformations.WLift.halfF_act0 {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) {m : ι → ZMod 4} (hm : (ρF β) m = 0) (b : Λ') : halfF β (((act0 π β MM bΛ) m) b) = (MM.act (halfF β m)) (π b)

noncomputable def MultiplicativeBasisDeformations.WLift.defect {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] (π : Λ' →+* Λ) {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] (β : Module.Basis ι (ZMod 2) M) (MM : GExt.GMod GΛ M) {κ : Type u_5} (bΛ : Module.Basis κ (ZMod 4) Λ') (m : ι → ZMod 4) (a b : Λ') : ι → ZMod 4

The associativity defect of the arbitrary lift.

theorem MultiplicativeBasisDeformations.WLift.ρF_defect {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (m : ι → ZMod 4) (a b : Λ') : (ρF β) (defect π β MM bΛ m a b) = 0

theorem MultiplicativeBasisDeformations.WLift.halfF_defect_indep {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) {m₁ m₂ : ι → ZMod 4} {a₁ a₂ b₁ b₂ : Λ'} (hm : (ρF β) m₁ = (ρF β) m₂) (ha : π a₁ = π a₂) (hb : π b₁ = π b₂) : halfF β (defect π β MM bΛ m₁ a₁ b₁) = halfF β (defect π β MM bΛ m₂ a₂ b₂)

The halved defect does not depend on the lifts.

theorem MultiplicativeBasisDeformations.WLift.defect_add_left {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (m n : ι → ZMod 4) (a b : Λ') : defect π β MM bΛ (m + n) a b = defect π β MM bΛ m a b + defect π β MM bΛ n a b

theorem MultiplicativeBasisDeformations.WLift.defect_smul_left {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (c : ZMod 4) (m : ι → ZMod 4) (a b : Λ') : defect π β MM bΛ (c • m) a b = c • defect π β MM bΛ m a b

theorem MultiplicativeBasisDeformations.WLift.defect_add_mid {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (m : ι → ZMod 4) (a a' b : Λ') : defect π β MM bΛ m (a + a') b = defect π β MM bΛ m a b + defect π β MM bΛ m a' b

theorem MultiplicativeBasisDeformations.WLift.defect_smul_mid {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (c : ZMod 4) (m : ι → ZMod 4) (a b : Λ') : defect π β MM bΛ m (c • a) b = c • defect π β MM bΛ m a b

theorem MultiplicativeBasisDeformations.WLift.defect_add_right {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (m : ι → ZMod 4) (a b b' : Λ') : defect π β MM bΛ m a (b + b') = defect π β MM bΛ m a b + defect π β MM bΛ m a b'

theorem MultiplicativeBasisDeformations.WLift.defect_smul_right {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (c : ZMod 4) (m : ι → ZMod 4) (a b : Λ') : defect π β MM bΛ m a (c • b) = c • defect π β MM bΛ m a b

noncomputable def MultiplicativeBasisDeformations.WLift.cbar {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (a b : Λ) : M →ₗ[ZMod 2] M

The halved defect as a 𝔽₂-linear map.

theorem MultiplicativeBasisDeformations.WLift.cbar_spec {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (m : ι → ZMod 4) (a b : Λ') : (cbar β bΛ hπ (π a) (π b)) ((ρF β) m) = halfF β (defect π β MM bΛ m a b)

theorem MultiplicativeBasisDeformations.WLift.cbar_add_left {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (a a' b : Λ) : cbar β bΛ hπ (a + a') b = cbar β bΛ hπ a b + cbar β bΛ hπ a' b

theorem MultiplicativeBasisDeformations.WLift.cbar_smul_left {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (c : ZMod 2) (a b : Λ) : cbar β bΛ hπ (c • a) b = c • cbar β bΛ hπ a b

theorem MultiplicativeBasisDeformations.WLift.cbar_add_right {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (a b b' : Λ) : cbar β bΛ hπ a (b + b') = cbar β bΛ hπ a b + cbar β bΛ hπ a b'

theorem MultiplicativeBasisDeformations.WLift.cbar_smul_right {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (c : ZMod 2) (a b : Λ) : cbar β bΛ hπ a (c • b) = c • cbar β bΛ hπ a b

noncomputable def MultiplicativeBasisDeformations.WLift.cochainF {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) : Bar.Cochain Λ (M →ₗ[ZMod 2] M)

The (negated) halved defect as a bar two-cochain.

theorem MultiplicativeBasisDeformations.WLift.defect_pentagon {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (m : ι → ZMod 4) (a₀ a₁ a₂ : Λ') : defect π β MM bΛ (((act0 π β MM bΛ) m) a₀) a₁ a₂ - defect π β MM bΛ m (a₀ * a₁) a₂ + defect π β MM bΛ m a₀ (a₁ * a₂) - ((act0 π β MM bΛ) (defect π β MM bΛ m a₀ a₁)) a₂ = 0

theorem MultiplicativeBasisDeformations.WLift.reprΛ_eq_zero {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) {q : ℤ} {b : Λ'} (hb : GΛ'.gr.IsHom q b) {κ' : κ} (h : dΛ κ' ≠ q) : (bΛ.repr b) κ' = 0

theorem MultiplicativeBasisDeformations.WLift.act0_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p q : ℤ} {m : ι → ZMod 4} {b : Λ'} (hm : (grF dβ).IsHom p m) (hb : GΛ'.gr.IsHom q b) : (grF dβ).IsHom (p + q) (((act0 π β MM bΛ) m) b)

theorem MultiplicativeBasisDeformations.WLift.defect_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p q r : ℤ} {m : ι → ZMod 4} {a b : Λ'} (hm : (grF dβ).IsHom p m) (ha : GΛ'.gr.IsHom q a) (hb : GΛ'.gr.IsHom r b) : (grF dβ).IsHom (p + q + r) (defect π β MM bΛ m a b)

theorem MultiplicativeBasisDeformations.WLift.halfF_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) {p : ℤ} {m : ι → ZMod 4} (hm : (grF dβ).IsHom p m) (h0 : (ρF β) m = 0) : MM.gr.IsHom p (halfF β m)

theorem MultiplicativeBasisDeformations.WLift.cochainF_good {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) : GExt.Good MM MM 2 0 (cochainF β bΛ hπ)

theorem MultiplicativeBasisDeformations.WLift.cochainF_d {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) : (Bar.d (GExt.homAct MM MM) 2) (cochainF β bΛ hπ) = 0

The corrected action

noncomputable def MultiplicativeBasisDeformations.WLift.act1 {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {β : Module.Basis ι (ZMod 2) M} {MM : GExt.GMod GΛ M} {κ : Type u_5} {bΛ : Module.Basis κ (ZMod 4) Λ'} {hπ : IsRed GΛ' GΛ π} (H : Bar.Cochain Λ (M →ₗ[ZMod 2] M)) (hH : GExt.Good MM MM 1 0 H) : (ι → ZMod 4) →ₗ[ZMod 4] Λ' →ₗ[ZMod 4] ι → ZMod 4

The corrected action m ⋆ b = m·b + 2·H(b̄)(m̄), for a cochain H.

theorem MultiplicativeBasisDeformations.WLift.act1_apply {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (H : Bar.Cochain Λ (M →ₗ[ZMod 2] M)) (hH : GExt.Good MM MM 1 0 H) (m : ι → ZMod 4) (b : Λ') : ((act1 H hH) m) b = ((act0 π β MM bΛ) m) b + (twF β) ((H (GExt.single (π b))) ((ρF β) m))

theorem MultiplicativeBasisDeformations.WLift.ρF_act1 {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (H : Bar.Cochain Λ (M →ₗ[ZMod 2] M)) (hH : GExt.Good MM MM 1 0 H) (m : ι → ZMod 4) (b : Λ') : (ρF β) (((act1 H hH) m) b) = (MM.act ((ρF β) m)) (π b)

theorem MultiplicativeBasisDeformations.WLift.act1_assoc {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (H : Bar.Cochain Λ (M →ₗ[ZMod 2] M)) (hH : GExt.Good MM MM 1 0 H) (hdH : (Bar.d (GExt.homAct MM MM) 1) H = cochainF β bΛ hπ) (m : ι → ZMod 4) (a b : Λ') : ((act1 H hH) (((act1 H hH) m) a)) b = ((act1 H hH) m) (a * b)

The corrected action is associative when dH is the negated halved defect.

theorem MultiplicativeBasisDeformations.WLift.act1_one {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (H : Bar.Cochain Λ (M →ₗ[ZMod 2] M)) (hH : GExt.Good MM MM 1 0 H) (hdH : (Bar.d (GExt.homAct MM MM) 1) H = cochainF β bΛ hπ) (m : ι → ZMod 4) : ((act1 H hH) m) 1 = m

The action of one is the identity: an idempotent congruent to the identity.

theorem MultiplicativeBasisDeformations.WLift.exists_liftMod {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {Λ' : Type u_2} [Ring Λ'] [Algebra (ZMod 4) Λ'] {GΛ' : GExt.GAlg Λ'} {π : Λ' →+* Λ} {M : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (β : Module.Basis ι (ZMod 2) M) (dβ : ι → ℤ) {MM : GExt.GMod GΛ M} {κ : Type u_5} [Fintype κ] (bΛ : Module.Basis κ (ZMod 4) Λ') (hπ : IsRed GΛ' GΛ π) (dΛ : κ → ℤ) (hbΛ : ∀ (κ' : κ), GΛ'.gr.IsHom (dΛ κ') (bΛ κ')) (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) (hExt : GExt.ExtVanish MM MM 1 0) : ∃ (MM' : GExt.GMod GΛ' (ι → ZMod 4)), IsLift MM' MM π (ρF β) ∧ MM'.gr = grF dβ

Proposition 10.1, the module lifts: a graded Λ-module with a homogeneous basis and Ext²_0(M, M) = 0 lifts to a graded Λ̃-module structure on ι → ℤ/4.