Graded Ext by the bar complex and graded extensions

Lemma 6.3 and Propositions 6.5, 6.6 use the graded groups Ext^n_Λ(M, N)_t. The formalization works with their vanishing in the bar form (GExt.ExtVanish): every degree-t bar (n+1)-cocycle M ⊗ Λ^{⊗(n+1)} → N is a coboundary. Over a field the bar complex M ⊗ Λ^{⊗•} ⊗ Λ is a graded free resolution of M and Hom_Λ(M ⊗ Λ^{⊗n} ⊗ Λ, N) = Hom(M ⊗ Λ^{⊗n}, N), so this is the usual graded Ext (Cartan–Eilenberg, Chapter IX). The identification with the paper's definition (degree-t maps out of any graded projective resolution) is proved in ExtResolutions.lean (GRes.extVanish_iff); this file records the extension form the paper uses.

• Ext¹ is the group of graded extensions: Ext¹(M, N)_t = 0 in the bar sense if and only if every graded extension 0 → N⟨−t⟩ → E → M → 0 splits (split_of_extVanish, extVanish_of_split, extVanish_zero_iff). The paper's proof of Lemma 6.3 for n = 1 argues with such extensions (ExtOne.lean).
• Higher Ext by dimension shifting: along an R-split exact sequence 0 → K → P → M → 0 with Ext^{n+1}(P, −) = 0, Ext^{n+1}(K, N)_t = 0 gives Ext^{n+2}(M, N)_t = 0 (extVanish_shift), and graded cyclic projectives have no higher Ext (CycProj.extVanish); these are the two properties used in the paper's proof of Lemma 6.3(2) (ExtHigher.lean).

structure MultiplicativeBasisDeformations.GExt.GExtn {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) (t : ℤ) (E : Type u_5) [AddCommGroup E] [Module R E] : Type (max (max (max u_2 u_3) u_4) u_5)

A graded extension 0 → N⟨−t⟩ → E → M → 0 of graded right Λ-modules.

• EE : GMod GΛ E
• i : N →ₗ[R] E
• p : E →ₗ[R] M
• i_act (n : N) (a : Λ) : self.i ((NN.act n) a) = (self.EE.act (self.i n)) a
• p_act (e : E) (a : Λ) : self.p ((self.EE.act e) a) = (MM.act (self.p e)) a
• i_inj : Function.Injective ⇑self.i
• p_surj : Function.Surjective ⇑self.p
• exact : self.i.range = self.p.ker
• i_hom (q : ℤ) (n : N) : NN.gr.IsHom (q + t) n → self.EE.gr.IsHom q (self.i n)
• p_hom (q : ℤ) (e : E) : self.EE.gr.IsHom q e → MM.gr.IsHom q (self.p e)

def MultiplicativeBasisDeformations.GExt.GExtn.Splits {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) : Prop

The extension splits: a graded Λ-linear section of p.

theorem MultiplicativeBasisDeformations.GExt.ZGr.map_proj' {R : Type u_1} [CommRing R] {X : Type u_5} {Y : Type u_6} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (gX : ZGr X) (gY : ZGr Y) (f : X →ₗ[R] Y) (hf : ∀ (p : ℤ) (x : X), gX.IsHom p x → gY.IsHom p (f x)) (p : ℤ) (x : X) : f ((gX.proj p) x) = (gY.proj p) (f x)

A graded linear map commutes with the projections.

theorem MultiplicativeBasisDeformations.GExt.ZGr.mem_range_proj' {R : Type u_1} [CommRing R] {X : Type u_5} [AddCommGroup X] [Module R X] (g : ZGr X) {p : ℤ} {x : X} : x ∈ (g.proj p).range ↔ g.IsHom p x

theorem MultiplicativeBasisDeformations.GExt.exists_graded_section {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} {E : Type u_5} [AddCommGroup E] [Module R E] (gE : ZGr E) (p : E →ₗ[R] M) (hp : Function.Surjective ⇑p) (hph : ∀ (q : ℤ) (e : E), gE.IsHom q e → MM.gr.IsHom q (p e)) (hproj : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) : ∃ (s : M →ₗ[R] E), (∀ (m : M), p (s m) = m) ∧ ∀ (q : ℤ) (m : M), MM.gr.IsHom q m → gE.IsHom q (s m)

A graded R-linear section of a graded surjection onto M, when the graded pieces of M are projective (always over a field).

Splitting from Ext¹ = 0

theorem MultiplicativeBasisDeformations.GExt.map_proj_shift {R : Type u_1} [CommRing R] {t : ℤ} {X : Type u_6} {Y : Type u_7} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (gX : ZGr X) (gY : ZGr Y) (f : X →ₗ[R] Y) (hf : ∀ (q : ℤ) (x : X), gX.IsHom (q + t) x → gY.IsHom q (f x)) (q : ℤ) (x : X) : f ((gX.proj (q + t)) x) = (gY.proj q) (f x)

A map of degree −t commutes with the projections, up to the shift.

theorem MultiplicativeBasisDeformations.GExt.GExtn.i_reflect {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {q : ℤ} {n : N} (h : X.EE.gr.IsHom q (X.i n)) : NN.gr.IsHom (q + t) n

noncomputable def MultiplicativeBasisDeformations.GExt.defect {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) (s : M →ₗ[R] E) (hs : ∀ (m : M), X.p (s m) = m) (a : Λ) : M →ₗ[R] N

The defect m ↦ s(m)a − s(ma) of a linear section, as a map to N.

theorem MultiplicativeBasisDeformations.GExt.i_defect {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) (a : Λ) (m : M) : X.i ((defect X s hs a) m) = (X.EE.act (s m)) a - s ((MM.act m) a)

theorem MultiplicativeBasisDeformations.GExt.defect_add {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) (a b : Λ) : defect X s hs (a + b) = defect X s hs a + defect X s hs b

theorem MultiplicativeBasisDeformations.GExt.defect_smul {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) (c : R) (a : Λ) : defect X s hs (c • a) = c • defect X s hs a

noncomputable def MultiplicativeBasisDeformations.GExt.defectCochain {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) : Bar.Cochain Λ (M →ₗ[R] N)

The cocycle of the extension.

theorem MultiplicativeBasisDeformations.GExt.defectCochain_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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) (hsh : ∀ (q : ℤ) (m : M), MM.gr.IsHom q m → X.EE.gr.IsHom q (s m)) : Good MM NN 1 t (defectCochain X hs)

theorem MultiplicativeBasisDeformations.GExt.defectCochain_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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) : (Bar.d (homAct MM NN) 1) (defectCochain X hs) = 0

theorem MultiplicativeBasisDeformations.GExt.split_of_extVanish {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} {t : ℤ} {E : Type u_5} [AddCommGroup E] [Module R E] (X : GExtn MM NN t E) {s : M →ₗ[R] E} (hs : ∀ (m : M), X.p (s m) = m) (hsh : ∀ (q : ℤ) (m : M), MM.gr.IsHom q m → X.EE.gr.IsHom q (s m)) (h : ExtVanish MM NN 0 t) : X.Splits

Ext¹(M, N)_t = 0 makes every graded extension split (given a graded linear section, e.g. over a field).

Ext¹ = 0 from splitting

theorem MultiplicativeBasisDeformations.GExt.extVanish_of_split {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} {t : ℤ} (h : ∀ (X : GExtn MM NN t (N × M)), X.Splits) : ExtVanish MM NN 0 t

If every graded extension of M by N⟨−t⟩ splits, Ext¹(M, N)_t = 0 (the extensions on N × M given by the cocycles suffice).

theorem MultiplicativeBasisDeformations.GExt.extVanish_zero_iff {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} {t : ℤ} (hproj : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) : ExtVanish MM NN 0 t ↔ ∀ (X : GExtn MM NN t (N × M)), X.Splits

Ext¹(M, N)_t in the bar sense vanishes iff every graded extension splits (the graded pieces of M projective over R, e.g. over a field); for extensions on any carrier see split_of_extVanish.