Proposition 6.5: lifting modules to positive deformations

positive-deformations.tex (prop:positive-module-lifting). After Lemma 6.4 the multiplication of a positive filtered deformation B of Λ is μ₀ + Σ_{q>0} μ_q on the vector space Λ, with μ₀ the product of Λ and μ_q raising internal degree by q (PosDef). "Seek an action ν₀ + ν₁ + ⋯ on M_i […]. Suppose the action identity holds through internal degree t − 1. Its error in internal degree t […] is a bar cocycle of bar degree two. […] Its class belongs to Ext²_Λ(M_i, M_i)_t = 0 by hypothesis. A cochain ν_t of bar degree one therefore removes the error."

Formalization. An action is a family ν n of bilinear maps raising degree by n, with ν 0 the given action; the action identity in internal degree n is the vanishing of the associator assocErr ν μ n (ActFam). The cocycle identity of the error is the degree-n part of the identity A(E(m,a,b),c) − E(A(m,a),b,c) + E(m,a⋆b,c) − E(m,a,b⋆c) = 0, proved by reindexing triple sums (assocErr_identity).

Triple sums

def MultiplicativeBasisDeformations.GExt.tri (j : ℕ) : Finset (ℕ × ℕ × ℕ)

The triples of natural numbers with sum j.

theorem MultiplicativeBasisDeformations.GExt.mem_tri {j : ℕ} {t : ℕ × ℕ × ℕ} : t ∈ tri j ↔ t.1 + t.2.1 + t.2.2 = j

theorem MultiplicativeBasisDeformations.GExt.sum_ad_ad_right {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, ∑ y ∈ Finset.HasAntidiagonal.antidiagonal x.2, F x.1 y.1 y.2 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

theorem MultiplicativeBasisDeformations.GExt.sum_ad_ad_left {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, ∑ y ∈ Finset.HasAntidiagonal.antidiagonal x.1, F y.1 y.2 x.2 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

theorem MultiplicativeBasisDeformations.GExt.sum_tri_equiv {X : Type u_1} [AddCommGroup X] (j : ℕ) (f : ℕ × ℕ × ℕ → X) (e : ℕ × ℕ × ℕ ≃ ℕ × ℕ × ℕ) (he : ∀ (t : ℕ × ℕ × ℕ), (e t).1 + (e t).2.1 + (e t).2.2 = t.1 + t.2.1 + t.2.2) : ∑ t ∈ tri j, f (e t) = ∑ t ∈ tri j, f t

Reindexing a triple sum by a sum-preserving bijection.

def MultiplicativeBasisDeformations.GExt.cyc3 : ℕ × ℕ × ℕ ≃ ℕ × ℕ × ℕ

The coordinate permutation (a, b, c) ↦ (b, c, a).

def MultiplicativeBasisDeformations.GExt.swap13 : ℕ × ℕ × ℕ ≃ ℕ × ℕ × ℕ

The coordinate permutation (a, b, c) ↦ (c, b, a).

theorem MultiplicativeBasisDeformations.GExt.sum_tri_cyc {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ t ∈ tri j, F t.2.1 t.2.2 t.1 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

theorem MultiplicativeBasisDeformations.GExt.sum_tri_swap13 {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ t ∈ tri j, F t.2.2 t.2.1 t.1 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

def MultiplicativeBasisDeformations.GExt.swap12 : ℕ × ℕ × ℕ ≃ ℕ × ℕ × ℕ

The coordinate permutation (a, b, c) ↦ (b, a, c).

theorem MultiplicativeBasisDeformations.GExt.sum_tri_swap12 {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ t ∈ tri j, F t.2.1 t.1 t.2.2 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

theorem MultiplicativeBasisDeformations.GExt.sum_tri_cyc' {X : Type u_1} [AddCommGroup X] (j : ℕ) (F : ℕ → ℕ → ℕ → X) : ∑ t ∈ tri j, F t.2.2 t.1 t.2.1 = ∑ t ∈ tri j, F t.1 t.2.1 t.2.2

The associator of an action family

def MultiplicativeBasisDeformations.GExt.assocErr {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m : M) (a b : Λ) : M

The action identity in internal degree n: its error Σ_{i+j=n} ν_j(ν_i(m,a),b) − Σ_{i+j=n} ν_i(m, μ_j(a,b)).

def MultiplicativeBasisDeformations.GExt.μAssoc {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (a b c : Λ) : Λ

The associator of the deformed product in internal degree n.

theorem MultiplicativeBasisDeformations.GExt.assocErr_identity {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (j : ℕ) (m : M) (a b c : Λ) : ∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, (((ν x.1) (assocErr ν μ x.2 m a b)) c - assocErr ν μ x.2 (((ν x.1) m) a) b c + assocErr ν μ x.2 m (((μ x.1) a) b) c - assocErr ν μ x.2 m a (((μ x.1) b) c)) = -∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, ((ν x.1) m) (μAssoc μ x.2 a b c)

The cocycle identity of the action error, in every internal degree j: the degree-j part of A(E(m,a,b),c) − E(A(m,a),b,c) + E(m,a⋆b,c) − E(m,a,b⋆c) = −A(m, assoc(a,b,c)).

theorem MultiplicativeBasisDeformations.GExt.assocErr_congr {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] {ν ν' : ℕ → M →ₗ[R] Λ →ₗ[R] M} (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) {n : ℕ} (h : ∀ i ≤ n, ν' i = ν i) (m : M) (a b : Λ) : assocErr ν' μ n m a b = assocErr ν μ n m a b

theorem MultiplicativeBasisDeformations.GExt.assocErr_update {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) {n : ℕ} (hn : 0 < n) (h0 : ν n = 0) (D : M →ₗ[R] Λ →ₗ[R] M) (m : M) (a b : Λ) : assocErr (Function.update ν n D) μ n m a b = assocErr ν μ n m a b + ((D (((ν 0) m) a)) b + ((ν 0) ((D m) a)) b - (D m) (((μ 0) a) b))

Adding a correction D in a positive degree n to a family vanishing in degree n.

theorem MultiplicativeBasisDeformations.GExt.assocErr_add_left {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m m' : M) (a b : Λ) : assocErr ν μ n (m + m') a b = assocErr ν μ n m a b + assocErr ν μ n m' a b

theorem MultiplicativeBasisDeformations.GExt.assocErr_add_mid {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m : M) (a a' b : Λ) : assocErr ν μ n m (a + a') b = assocErr ν μ n m a b + assocErr ν μ n m a' b

theorem MultiplicativeBasisDeformations.GExt.assocErr_add_right {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m : M) (a b b' : Λ) : assocErr ν μ n m a (b + b') = assocErr ν μ n m a b + assocErr ν μ n m a b'

theorem MultiplicativeBasisDeformations.GExt.assocErr_smul_left {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (c : R) (m : M) (a b : Λ) : assocErr ν μ n (c • m) a b = c • assocErr ν μ n m a b

theorem MultiplicativeBasisDeformations.GExt.assocErr_smul_mid {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (c : R) (m : M) (a b : Λ) : assocErr ν μ n m (c • a) b = c • assocErr ν μ n m a b

theorem MultiplicativeBasisDeformations.GExt.assocErr_smul_right {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (c : R) (m : M) (a b : Λ) : assocErr ν μ n m a (c • b) = c • assocErr ν μ n m a b

def MultiplicativeBasisDeformations.GExt.assocErrL {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (a b : Λ) : M →ₗ[R] M

The error as a linear map in m.

def MultiplicativeBasisDeformations.GExt.assocErrL₁ {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m : M) (b : Λ) : Λ →ₗ[R] M

The error as a linear map in the first algebra input.

def MultiplicativeBasisDeformations.GExt.assocErrL₂ {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (m : M) (a : Λ) : Λ →ₗ[R] M

The error as a linear map in the second algebra input.

Positive deformations and lifted actions

structure MultiplicativeBasisDeformations.GExt.PosDef {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) : Type u_2

A positive deformation of Λ in split form (Lemma 6.4): the multiplication μ₀ + Σ_{q>0} μ_q, with μ₀ the product of Λ and μ_q of internal degree q.

• μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ
• μ_zero (a b : Λ) : ((self.μ 0) a) b = a * b
• deg (q : ℕ) : HDeg GΛ (self.μ q) ↑q
• assoc (n : ℕ) (a b c : Λ) : μAssoc self.μ n a b c = 0
• unit_left (q : ℕ) : 0 < q → ∀ (a : Λ), ((self.μ q) 1) a = 0
• unit_right (q : ℕ) : 0 < q → ∀ (a : Λ), ((self.μ q) a) 1 = 0

def MultiplicativeBasisDeformations.GExt.IsShift {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (n : ℤ) (f : M →ₗ[R] Λ →ₗ[R] M) : Prop

A bilinear map M × Λ → M raising internal degree by n.

structure MultiplicativeBasisDeformations.GExt.ActFam {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (P : PosDef GΛ) (MM : GMod GΛ M) : Type (max u_2 u_3)

A filtered lift of the action of M to the deformation (Proposition 6.5(1)): m · a = Σ_n ν_n(m, a) with ν₀ the given action and the action identity in every internal degree.

• ν : ℕ → M →ₗ[R] Λ →ₗ[R] M
• ν_zero (m : M) (a : Λ) : ((self.ν 0) m) a = (MM.act m) a
• deg (n : ℕ) : IsShift MM (↑n) (self.ν n)
• assoc (n : ℕ) (m : M) (a b : Λ) : assocErr self.ν P.μ n m a b = 0

def MultiplicativeBasisDeformations.GExt.errCoch {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) : Bar.Cochain Λ (M →ₗ[R] M)

The error cochain of a family in internal degree n, a bar two-cochain.

theorem MultiplicativeBasisDeformations.GExt.errCoch_apply {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} [AddCommGroup M] [Module R M] (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (a : ℕ → Λ) (m : M) : (errCoch ν μ n a) m = assocErr ν μ n m (a 0) (a 1)

theorem MultiplicativeBasisDeformations.GExt.assocErr_isHom {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} (hν : ∀ (i : ℕ), IsShift MM (↑i) (ν i)) (P : PosDef GΛ) (n : ℕ) {p q r : ℤ} {m : M} {a b : Λ} (hm : MM.gr.IsHom p m) (ha : GΛ.gr.IsHom q a) (hb : GΛ.gr.IsHom r b) : MM.gr.IsHom (p + q + r + ↑n) (assocErr ν P.μ n m a b)

theorem MultiplicativeBasisDeformations.GExt.errCoch_good {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} (hν : ∀ (i : ℕ), IsShift MM (↑i) (ν i)) (P : PosDef GΛ) (n : ℕ) : Good MM MM 2 (↑n) (errCoch ν P.μ n)

theorem MultiplicativeBasisDeformations.GExt.errCoch_d {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} (hν0 : ∀ (m : M) (a : Λ), ((ν 0) m) a = (MM.act m) a) (P : PosDef GΛ) (n : ℕ) (hlow : ∀ l < n, ∀ (m : M) (a b : Λ), assocErr ν P.μ l m a b = 0) : (Bar.d (homAct MM MM) 2) (errCoch ν P.μ n) = 0

The error is a cocycle once the action identity holds in lower internal degrees.

def MultiplicativeBasisDeformations.GExt.cochBil {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {t : ℤ} {F : Bar.Cochain Λ (M →ₗ[R] M)} (hF : Good MM MM 1 t F) : M →ₗ[R] Λ →ₗ[R] M

The bilinear map of a good one-cochain.

theorem MultiplicativeBasisDeformations.GExt.cochBil_apply {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {t : ℤ} {F : Bar.Cochain Λ (M →ₗ[R] M)} (hF : Good MM MM 1 t F) (m : M) (a : Λ) : ((cochBil hF) m) a = (F (single a)) m

theorem MultiplicativeBasisDeformations.GExt.exists_partial {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (P : PosDef GΛ) (hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM MM 1 ↑t) (N : ℕ) : ∃ (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M), (∀ (m : M) (a : Λ), ((ν 0) m) a = (MM.act m) a) ∧ (∀ (n : ℕ), IsShift MM (↑n) (ν n)) ∧ (∀ (n : ℕ), N < n → ν n = 0) ∧ ∀ n ≤ N, ∀ (m : M) (a b : Λ), assocErr ν P.μ n m a b = 0

The degree-by-degree construction (proof of Proposition 6.5(1)): a family satisfying the action identity through internal degree N, vanishing above N.

theorem MultiplicativeBasisDeformations.GExt.assocErr_eq_zero_of_hom {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (n : ℕ) (h : ∀ (p q r : ℤ) (m : M) (a b : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom q a → GΛ.gr.IsHom r b → assocErr ν μ n m a b = 0) (m : M) (a b : Λ) : assocErr ν μ n m a b = 0

A trilinear identity holds when it holds on homogeneous inputs.

def MultiplicativeBasisDeformations.GExt.degBound {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (g : ZGr M) : ℕ

A bound for the internal degrees of M.

theorem MultiplicativeBasisDeformations.GExt.le_degBound {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {g : ZGr M} {x : ℤ} (hx : x ∈ g.supp) : |x| ≤ ↑(degBound g)

theorem MultiplicativeBasisDeformations.GExt.exists_actFam {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (P : PosDef GΛ) (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) (hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM MM 1 ↑t) : Nonempty (ActFam P MM)

Proposition 6.5(1), existence: under Ext²_Λ(M, M)_t = 0 for t > 0, the action of M lifts to the positive deformation.

Lifting maps (Proposition 6.5(1) uniqueness and (2))

def MultiplicativeBasisDeformations.GExt.interErr {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) (m : M) (a : Λ) : N

The linearity error of a lifted map in internal degree n: Σ_{i+j=n} F_j(ν_i(m,a)) − Σ_{i+j=n} ν'_i(F_j(m), a).

theorem MultiplicativeBasisDeformations.GExt.interErr_identity {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (μ : ℕ → Λ →ₗ[R] Λ →ₗ[R] Λ) (j : ℕ) (m : M) (a b : Λ) : ∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, (interErr F ν ν' x.2 (((ν x.1) m) a) b - interErr F ν ν' x.2 m (((μ x.1) a) b) + ((ν' x.1) (interErr F ν ν' x.2 m a)) b) = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal j, ((F x.1) (assocErr ν μ x.2 m a b) - assocErr ν' μ x.2 ((F x.1) m) a b)

The cocycle identity of the linearity error.

theorem MultiplicativeBasisDeformations.GExt.interErr_congr {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {F F' : ℕ → M →ₗ[R] N} (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) {n : ℕ} (h : ∀ i ≤ n, F' i = F i) (m : M) (a : Λ) : interErr F' ν ν' n m a = interErr F ν ν' n m a

theorem MultiplicativeBasisDeformations.GExt.interErr_update {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {F : ℕ → M →ₗ[R] N} (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) {n : ℕ} (h0 : F n = 0) (D : M →ₗ[R] N) (m : M) (a : Λ) : interErr (Function.update F n D) ν ν' n m a = interErr F ν ν' n m a + (D (((ν 0) m) a) - ((ν' 0) (D m)) a)

def MultiplicativeBasisDeformations.GExt.interErrL {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) (a : Λ) : M →ₗ[R] N

The linearity error as a linear map in m.

def MultiplicativeBasisDeformations.GExt.interErrL₁ {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) (m : M) : Λ →ₗ[R] N

The linearity error as a linear map in a.

theorem MultiplicativeBasisDeformations.GExt.interErr_eq_zero_of_hom {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) (h : ∀ (p q : ℤ) (m : M) (a : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom q a → interErr F ν ν' n m a = 0) (m : M) (a : Λ) : interErr F ν ν' n m a = 0

theorem MultiplicativeBasisDeformations.GExt.interErr_isHom {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} {F : ℕ → M →ₗ[R] N} {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} {ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N} {r : ℤ} (hF : ∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) (hν : ∀ (i : ℕ), IsShift MM (↑i) (ν i)) (hν' : ∀ (i : ℕ), IsShift NN (↑i) (ν' i)) (n : ℕ) {p q : ℤ} {m : M} {a : Λ} (hm : MM.gr.IsHom p m) (ha : GΛ.gr.IsHom q a) : NN.gr.IsHom (p + q + r + ↑n) (interErr F ν ν' n m a)

def MultiplicativeBasisDeformations.GExt.interCoch {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) : Bar.Cochain Λ (M →ₗ[R] N)

The linearity error cochain, a bar one-cochain.

theorem MultiplicativeBasisDeformations.GExt.interCoch_apply {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ℕ → M →ₗ[R] N) (ν : ℕ → M →ₗ[R] Λ →ₗ[R] M) (ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N) (n : ℕ) (a : ℕ → Λ) (m : M) : (interCoch F ν ν' n a) m = interErr F ν ν' n m (a 0)

theorem MultiplicativeBasisDeformations.GExt.interCoch_good {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} {F : ℕ → M →ₗ[R] N} {ν : ℕ → M →ₗ[R] Λ →ₗ[R] M} {ν' : ℕ → N →ₗ[R] Λ →ₗ[R] N} {r : ℤ} (hF : ∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) (hν : ∀ (i : ℕ), IsShift MM (↑i) (ν i)) (hν' : ∀ (i : ℕ), IsShift NN (↑i) (ν' i)) (n : ℕ) : Good MM NN 1 (r + ↑n) (interCoch F ν ν' n)

theorem MultiplicativeBasisDeformations.GExt.interCoch_d {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} (P : PosDef GΛ) (L : ActFam P MM) (L' : ActFam P NN) {F : ℕ → M →ₗ[R] N} (n : ℕ) (hlow : ∀ l < n, ∀ (m : M) (a : Λ), interErr F L.ν L'.ν l m a = 0) : (Bar.d (homAct MM NN) 1) (interCoch F L.ν L'.ν n) = 0

The linearity error is a cocycle once it vanishes in lower internal degrees.

theorem MultiplicativeBasisDeformations.GExt.exists_partialMap {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} (P : PosDef GΛ) (L : ActFam P MM) (L' : ActFam P NN) {r : ℤ} (f : M →ₗ[R] N) (hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) (hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) (hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM NN 0 (r + ↑t)) (K : ℕ) : ∃ (F : ℕ → M →ₗ[R] N), F 0 = f ∧ (∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) ∧ (∀ (n : ℕ), K < n → F n = 0) ∧ ∀ n ≤ K, ∀ (m : M) (a : Λ), interErr F L.ν L'.ν n m a = 0

The degree-by-degree lift of a map (proof of Proposition 6.5(2)).

theorem MultiplicativeBasisDeformations.GExt.exists_liftMap {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} (P : PosDef GΛ) (L : ActFam P MM) (L' : ActFam P NN) {r : ℤ} (f : M →ₗ[R] N) (hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) (hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) (hExt : ∀ (t : ℕ), 0 < t → ExtVanish MM NN 0 (r + ↑t)) : ∃ (F : ℕ → M →ₗ[R] N), F 0 = f ∧ (∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) ∧ ∀ (n : ℕ) (m : M) (a : Λ), interErr F L.ν L'.ν n m a = 0

Proposition 6.5(2), lifts of maps (and, for M = N, f = id, the uniqueness of lifted actions up to a coordinate change id + (higher)): a homogeneous Λ-linear map of degree r lifts with prescribed leading term, under Ext¹_Λ(M, N)_{r+t} = 0 for t > 0.

Totals

theorem MultiplicativeBasisDeformations.GExt.sum_range_ad {X : Type u_1} [AddCommGroup X] (N : ℕ) (g : ℕ → ℕ → X) : ∑ n ∈ Finset.range N, ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, g x.1 x.2 = ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range (N - i), g i j

Summing the degree-n identities over all n gives the total identity.

theorem MultiplicativeBasisDeformations.GExt.sum_range_ad_box {X : Type u_1} [AddCommGroup X] (A C : ℕ) (g : ℕ → ℕ → X) (hA : ∀ (i j : ℕ), A < i → g i j = 0) (hC : ∀ (i j : ℕ), C < j → g i j = 0) : ∑ n ∈ Finset.range (A + C + 1), ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, g x.1 x.2 = ∑ i ∈ Finset.range (A + 1), ∑ j ∈ Finset.range (C + 1), g i j

Double sums of a function vanishing outside a box.

theorem MultiplicativeBasisDeformations.GExt.sum_range_ad_box' {X : Type u_1} [AddCommGroup X] (A C K : ℕ) (hK : A + C + 1 ≤ K) (g : ℕ → ℕ → X) (hA : ∀ (i j : ℕ), A < i → g i j = 0) (hC : ∀ (i j : ℕ), C < j → g i j = 0) : ∑ n ∈ Finset.range K, ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, g x.1 x.2 = ∑ i ∈ Finset.range (A + 1), ∑ j ∈ Finset.range (C + 1), g i j

The same, over any longer range.

theorem MultiplicativeBasisDeformations.GExt.shift_eq_zero {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) {n : ℕ} {f : M →ₗ[R] Λ →ₗ[R] M} (hf : IsShift MM (↑n) f) (hn : 2 * degBound MM.gr < n) : f = 0

A shift beyond the spread of the degrees of M vanishes.

def MultiplicativeBasisDeformations.GExt.ActFam.tot {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {P : PosDef GΛ} (L : ActFam P MM) : M →ₗ[R] Λ →ₗ[R] M

The total lifted action m · a = Σ_n ν_n(m, a).

def MultiplicativeBasisDeformations.GExt.PosDef.tot {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} (P : PosDef GΛ) : Λ →ₗ[R] Λ →ₗ[R] Λ

The total deformed product a ⋆ b = Σ_q μ_q(a, b).

theorem MultiplicativeBasisDeformations.GExt.PosDef.μ_eq_zero {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} (P : PosDef GΛ) (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) {q : ℕ} (hq : degBound GΛ.gr < q) : P.μ q = 0

A product of internal degree q beyond the degrees of Λ vanishes.

theorem MultiplicativeBasisDeformations.GExt.ActFam.tot_assoc {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) {P : PosDef GΛ} (L : ActFam P MM) (m : M) (a b : Λ) : (L.tot ((L.tot m) a)) b = (L.tot m) ((P.tot a) b)

The total action identity (m · a) · b = m · (a ⋆ b).

theorem MultiplicativeBasisDeformations.GExt.ActFam.ν_one {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {P : PosDef GΛ} (L : ActFam P MM) (n : ℕ) : 0 < n → ∀ (m : M), ((L.ν n) m) 1 = 0

The higher terms of a lifted action vanish on 1.

theorem MultiplicativeBasisDeformations.GExt.ActFam.tot_one {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {P : PosDef GΛ} (L : ActFam P MM) (m : M) : (L.tot m) 1 = m

The unit law m · 1 = m.

Total lifted maps

def MultiplicativeBasisDeformations.GExt.mapBound {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (MM : GMod GΛ M) (NN : GMod GΛ N) (r : ℤ) : ℕ

The bound for the terms of a lifted map.

theorem MultiplicativeBasisDeformations.GExt.map_eq_zero {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} {r : ℤ} {i : ℕ} {g : M →ₗ[R] N} (hg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) (g m)) (hi : mapBound MM NN r < i) : g = 0

def MultiplicativeBasisDeformations.GExt.mapTot {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (MM : GMod GΛ M) (NN : GMod GΛ N) (r : ℤ) (F : ℕ → M →ₗ[R] N) : M →ₗ[R] N

The total lifted map Σ_i F_i.

theorem MultiplicativeBasisDeformations.GExt.mapTot_comm {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) {P : PosDef GΛ} (L : ActFam P MM) (L' : ActFam P NN) {r : ℤ} {F : ℕ → M →ₗ[R] N} (hF : ∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r + ↑i) ((F i) m)) (hFa : ∀ (n : ℕ) (m : M) (a : Λ), interErr F L.ν L'.ν n m a = 0) (m : M) (a : Λ) : (mapTot MM NN r F) ((L.tot m) a) = (L'.tot ((mapTot MM NN r F) m)) a

A lifted map is linear for the lifted actions.

Maps raising degree

def MultiplicativeBasisDeformations.GExt.RaisesBy {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (j : ℤ) (f : M →ₗ[R] M) : Prop

f raises internal degree by at least j.

theorem MultiplicativeBasisDeformations.GExt.RaisesBy.comp {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {j j' : ℤ} {f g : M →ₗ[R] M} (hf : RaisesBy MM j f) (hg : RaisesBy MM j' g) : RaisesBy MM (j + j') (g ∘ₗ f)

theorem MultiplicativeBasisDeformations.GExt.RaisesBy.eq_zero {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {k : ℤ} {f : M →ₗ[R] M} (hf : RaisesBy MM k f) (hk : 2 * ↑(degBound MM.gr) < k) : f = 0

theorem MultiplicativeBasisDeformations.GExt.RaisesBy.pow {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {f : M →ₗ[R] M} (hf : RaisesBy MM 1 f) (k : ℕ) : RaisesBy MM (↑k) (f ^ k)

theorem MultiplicativeBasisDeformations.GExt.RaisesBy.isNilpotent {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {f : M →ₗ[R] M} (hf : RaisesBy MM 1 f) : IsNilpotent f

theorem MultiplicativeBasisDeformations.GExt.mapTot_bijective {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} {F : ℕ → M →ₗ[R] M} (hF0 : F 0 = LinearMap.id) (hF : ∀ (i : ℕ) (p : ℤ) (m : M), MM.gr.IsHom p m → MM.gr.IsHom (p + 0 + ↑i) ((F i) m)) : Function.Bijective ⇑(mapTot MM MM 0 F)

The coordinate change of a lifted identity is invertible.

Leading terms of filtered maps

def MultiplicativeBasisDeformations.GExt.OrderGe {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (MM : GMod GΛ M) (NN : GMod GΛ N) (r : ℤ) (g : M →ₗ[R] N) : Prop

A map M → N of filtration order at least r.

theorem MultiplicativeBasisDeformations.GExt.leading_linear {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : GMod GΛ M} {NN : GMod GΛ N} (hnn : ∀ q ∈ GΛ.gr.supp, 0 ≤ q) {P : PosDef GΛ} (L : ActFam P MM) (L' : ActFam P NN) {r : ℤ} {g : M →ₗ[R] N} (hg : ∀ (m : M) (a : Λ), g ((L.tot m) a) = (L'.tot (g m)) a) (hord : OrderGe MM NN r g) (m : M) (a : Λ) : (MM.gr.comp NN.gr r g) ((MM.act m) a) = (NN.act ((MM.gr.comp NN.gr r g) m)) a

The leading term of a filtered map of the lifts is Λ-linear (proof of Proposition 6.5(2): "the leading term of a nonzero filtered map is a homogeneous Λ-linear map of the same degree").