Graded Ext from graded projective resolutions (Lemma 6.3)

positive-deformations.tex: "Internal degree t in Hom or Ext means maps from a graded projective resolution to the target which raise degree by t." This file defines that Ext and compares it with the bar Ext (ExtVanish) used in the rest of the formalization.

• GProj: a graded projective module (degree-zero graded module maps lift along graded surjections). Finitely generated ones are retracts of finite sums of shifted regular modules (exists_free_cover), so their bar Ext vanishes (GProj.extVanish).
• GRes: a graded projective resolution ⋯ → P₁ → P₀ → M → 0 (finitely generated graded projectives, maps of degree 0, exact). GRes.ExtVanish: Ext^{n+1}(M, N)_t = 0 computed from it, i.e. every degree-t graded module map P_{n+1} → N vanishing on the image of P_{n+2} factors through P_{n+1} → P_n by a degree-t graded module map.
• GRes.extVanish_iff: for every graded projective resolution, this vanishing is the bar vanishing. In particular it does not depend on the resolution. Over a commutative ring R (a field, or ℤ/4 in Lemma 6.6) it assumes the graded pieces of Λ and M projective over R (for the free modules of Lemma 6.6, and automatically over a field: GRes.extVanish_iff_field).
• exists_gres: a finitely generated graded module over a module-finite graded algebra over a noetherian ring has a graded projective resolution.

So every Ext vanishing hypothesis or conclusion stated in the bar form (Lemma 6.3, Propositions 6.5, 10.1, Lemma 6.6) is equivalent to the manuscript's form for any graded projective resolution.

structure MultiplicativeBasisDeformations.GExt.IsGMap {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (XX : GMod GΛ X) (YY : GMod GΛ Y) (t : ℤ) (f : X →ₗ[R] Y) : Prop

A graded module map of degree t.

• act (x : X) (a : Λ) : f ((XX.act x) a) = (YY.act (f x)) a
• deg (p : ℤ) (x : X) : XX.gr.IsHom p x → YY.gr.IsHom (p + t) (f x)

def MultiplicativeBasisDeformations.GExt.GMod.reg {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) : GMod GΛ Λ

The regular graded module Λ.

theorem MultiplicativeBasisDeformations.GExt.GMod.reg_act {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} (m a : Λ) : ((reg GΛ).act m) a = m * a

def MultiplicativeBasisDeformations.GExt.regCyc {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} : CycProj (GMod.reg GΛ)

The regular module is cyclic projective, generated by 1.

def MultiplicativeBasisDeformations.GExt.GMod.free {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) : GMod GΛ (ι → Λ)

The finite free graded module ⊕_i Λ⟨b_i⟩.

theorem MultiplicativeBasisDeformations.GExt.GMod.free_act {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) (x : ι → Λ) (a : Λ) (i : ι) : ((free GΛ b).act x) a i = x i * a

theorem MultiplicativeBasisDeformations.GExt.GMod.free_isHom {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) (p : ℤ) (x : ι → Λ) : (free GΛ b).gr.IsHom p x ↔ ∀ (i : ι), GΛ.gr.IsHom (p - b i) (x i)

theorem MultiplicativeBasisDeformations.GExt.extVanish_free {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) {N : Type u_1} [AddCommGroup N] [Module R N] (NN : GMod GΛ N) (n : ℕ) (t : ℤ) : ExtVanish (GMod.free GΛ b) NN n t

Ext out of a finite free graded module vanishes.

def MultiplicativeBasisDeformations.GExt.GProj {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {P : Type w} [AddCommGroup P] [Module R P] (PP : GMod GΛ P) : Prop

A graded projective module: graded module maps of degree 0 lift along graded surjections from graded modules in the universe of Λ onto graded modules in the universe of P.

structure MultiplicativeBasisDeformations.GExt.Cover {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {X : Type u_1} [AddCommGroup X] [Module R X] (XX : GMod GΛ X) : Type (max (max 1 u) u_1)

A cover of a graded module by a finite free graded module.

• ι : Type
• fi : Fintype self.ι
• de : DecidableEq self.ι
• b : self.ι → ℤ
• c : (self.ι → Λ) →ₗ[R] X
• hc : IsGMap (GMod.free GΛ self.b) XX 0 self.c
• surj : Function.Surjective ⇑self.c

theorem MultiplicativeBasisDeformations.GExt.exists_free_cover {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {X : Type u_1} [AddCommGroup X] [Module R X] (XX : GMod GΛ X) [Module.Finite R X] : Nonempty (Cover XX)

A finitely generated graded module has a finite free graded cover: the homogeneous components of a finite generating set, as generators of shifted copies of Λ.

theorem MultiplicativeBasisDeformations.GExt.gProj_free {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) : GProj (GMod.free GΛ b)

Finite free graded modules are graded projective.

theorem MultiplicativeBasisDeformations.GExt.GProj.extVanish {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {P : Type w} [AddCommGroup P] [Module R P] {PP : GMod GΛ P} (hP : GProj PP) [Module.Finite R P] {N : Type u_1} [AddCommGroup N] [Module R N] (NN : GMod GΛ N) (n : ℕ) (t : ℤ) : ExtVanish PP NN n t

Ext out of a finitely generated graded projective vanishes: it is a retract of a finite free graded module.

theorem MultiplicativeBasisDeformations.GExt.proj_of_retract {R : Type v} [CommRing R] {X : Type u_1} {Y : Type u_2} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (gX : ZGr X) (gY : ZGr Y) (i : X →ₗ[R] Y) (s : Y →ₗ[R] X) (hi : ∀ (p : ℤ) (x : X), gX.IsHom p x → gY.IsHom p (i x)) (hs : ∀ (p : ℤ) (y : Y), gY.IsHom p y → gX.IsHom p (s y)) (hsi : s ∘ₗ i = LinearMap.id) (q : ℤ) [Module.Projective R ↥(gY.proj q).range] : Module.Projective R ↥(gX.proj q).range

A degree-0 graded retract of a module with projective graded pieces has projective graded pieces.

theorem MultiplicativeBasisDeformations.GExt.proj_free {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} (hΛ : ∀ (q : ℤ), Module.Projective R ↥(GΛ.gr.proj q).range) {ι : Type} [Fintype ι] [DecidableEq ι] (b : ι → ℤ) (q : ℤ) : Module.Projective R ↥((GMod.free GΛ b).gr.proj q).range

The graded pieces of a finite free graded module are projective when those of Λ are.

theorem MultiplicativeBasisDeformations.GExt.GProj.proj_pieces {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {P : Type w} [AddCommGroup P] [Module R P] {PP : GMod GΛ P} (hP : GProj PP) [Module.Finite R P] (hΛ : ∀ (q : ℤ), Module.Projective R ↥(GΛ.gr.proj q).range) (q : ℤ) : Module.Projective R ↥(PP.gr.proj q).range

The graded pieces of a finitely generated graded projective module are projective when those of Λ are.

Ext¹ and extensions of maps from the syzygy

theorem MultiplicativeBasisDeformations.GExt.exists_gsection {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_1} [AddCommGroup M] [Module R M] {P : Type u_3} [AddCommGroup P] [Module R P] (PP : GMod GΛ P) (MM : GMod GΛ M) {π : P →ₗ[R] M} (hπ : IsGMap PP MM 0 π) (hs : Function.Surjective ⇑π) (hM : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) : ∃ (s : M →ₗ[R] P), π ∘ₗ s = LinearMap.id ∧ ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → PP.gr.IsHom (p + 0) (s m)

A graded R-linear section of a graded surjection.

theorem MultiplicativeBasisDeformations.GExt.extVanish_zero_iff_extend {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_3} [AddCommGroup P] [Module R P] (PP : GMod GΛ P) (MM : GMod GΛ M) {π : P →ₗ[R] M} (hπ : IsGMap PP MM 0 π) (hs : Function.Surjective ⇑π) (hM : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) (NN : GMod GΛ N) (t : ℤ) (hP : ExtVanish PP NN 0 t) : ExtVanish MM NN 0 t ↔ ∀ (h : ↥π.ker →ₗ[R] N), IsGMap (PP.ker MM ⋯ ⋯) NN t h → ∃ (g : P →ₗ[R] N), IsGMap PP NN t g ∧ g ∘ₗ π.ker.subtype = h

Ext¹(M, N)_t (bar) vanishes iff every degree-t graded module map out of the kernel extends to P, along 0 → K → P → M → 0 with Ext¹(P, N)_t = 0.

Graded projective resolutions

structure MultiplicativeBasisDeformations.GExt.GRes {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) : Type (max (max u v) (w + 1))

A graded projective resolution ⋯ → P₁ → P₀ → M → 0 of a graded module M: finitely generated graded projective modules (in the universe of M), maps of degree 0, exact.

• P : ℕ → Type w
• acg (n : ℕ) : AddCommGroup (self.P n)
• mod (n : ℕ) : Module R (self.P n)
• PP (n : ℕ) : GMod GΛ (self.P n)
• d (n : ℕ) : self.P (n + 1) →ₗ[R] self.P n
• ε : self.P 0 →ₗ[R] M
• d_map (n : ℕ) : IsGMap (self.PP (n + 1)) (self.PP n) 0 (self.d n)
• ε_map : IsGMap (self.PP 0) MM 0 self.ε
• ε_surj : Function.Surjective ⇑self.ε
• exact_zero : self.ε.ker = (self.d 0).range
• exact (n : ℕ) : (self.d n).ker = (self.d (n + 1)).range
• proj (n : ℕ) : GProj (self.PP n)
• fin (n : ℕ) : Module.Finite R (self.P n)

def MultiplicativeBasisDeformations.GExt.GRes.ExtVanish {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (NN : GMod GΛ N) (n : ℕ) (t : ℤ) : Prop

Ext^{n+1}(M, N)_t = 0 computed from the resolution: every degree-t graded module map P_{n+1} → N that vanishes on the image of P_{n+2} is g ∘ d for a degree-t graded module map g : P_n → N (the cocycles of Hom_t(P_•, N) in degree n+1 are coboundaries).

def MultiplicativeBasisDeformations.GExt.GRes.kerMod {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : GMod GΛ ↥Rs.ε.ker

The first syzygy ker ε as a graded module.

def MultiplicativeBasisDeformations.GExt.GRes.ε' {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : Rs.P 1 →ₗ[R] ↥Rs.ε.ker

P₁ → ker ε.

theorem MultiplicativeBasisDeformations.GExt.GRes.ε'_apply {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (x : Rs.P 1) : ↑(Rs.ε' x) = (Rs.d 0) x

theorem MultiplicativeBasisDeformations.GExt.GRes.ε'_surj {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : Function.Surjective ⇑Rs.ε'

theorem MultiplicativeBasisDeformations.GExt.GRes.ε'_map {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : IsGMap (Rs.PP 1) Rs.kerMod 0 Rs.ε'

theorem MultiplicativeBasisDeformations.GExt.GRes.ker_ε' {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : Rs.ε'.ker = (Rs.d 1).range

def MultiplicativeBasisDeformations.GExt.GRes.trunc {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : GRes Rs.kerMod

The truncated resolution ⋯ → P₂ → P₁ → ker ε → 0.

theorem MultiplicativeBasisDeformations.GExt.GRes.trunc_extVanish {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (NN : GMod GΛ N) (n : ℕ) (t : ℤ) : Rs.trunc.ExtVanish NN n t ↔ Rs.ExtVanish NN (n + 1) t

theorem MultiplicativeBasisDeformations.GExt.GRes.extVanish_zero_iff {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (NN : GMod GΛ N) (t : ℤ) : Rs.ExtVanish NN 0 t ↔ ∀ (h : ↥Rs.ε.ker →ₗ[R] N), IsGMap Rs.kerMod NN t h → ∃ (g : Rs.P 0 →ₗ[R] N), IsGMap (Rs.PP 0) NN t g ∧ g ∘ₗ Rs.ε.ker.subtype = h

Ext¹ from the resolution vanishes iff every degree-t graded module map out of ker ε extends to P₀.

theorem MultiplicativeBasisDeformations.GExt.GRes.extVanish_kerMod_iff {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (hM : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) (NN : GMod GΛ N) (n : ℕ) (t : ℤ) : GExt.ExtVanish Rs.kerMod NN n t ↔ GExt.ExtVanish MM NN (n + 1) t

The degree-0 graded R-split sequence 0 → ker ε → P₀ → M → 0, and dimension shifting of the bar Ext along it.

theorem MultiplicativeBasisDeformations.GExt.GRes.kerMod_proj {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) (hΛ : ∀ (q : ℤ), Module.Projective R ↥(GΛ.gr.proj q).range) (hM : ∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) (q : ℤ) : Module.Projective R ↥(Rs.kerMod.gr.proj q).range

The graded pieces of the first syzygy are projective.

theorem MultiplicativeBasisDeformations.GExt.GRes.extVanish_iff {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {N : Type u_2} [AddCommGroup N] [Module R N] (hΛ : ∀ (q : ℤ), Module.Projective R ↥(GΛ.gr.proj q).range) (NN : GMod GΛ N) (n : ℕ) {M : Type w} [AddCommGroup M] [Module R M] {MM : GMod GΛ M} (Rs : GRes MM) : (∀ (q : ℤ), Module.Projective R ↥(MM.gr.proj q).range) → ∀ (t : ℤ), Rs.ExtVanish NN n t ↔ GExt.ExtVanish MM NN n t

The Ext of a graded projective resolution is the bar Ext: for every graded projective resolution of M, Ext^{n+1}(M, N)_t computed from it vanishes iff the bar Ext^{n+1}(M, N)_t vanishes. In particular the vanishing does not depend on the resolution. Over a commutative ring, assuming the graded pieces of Λ and of M projective (automatic over a field, GRes.extVanish_iff_field; true for the free modules over ℤ/4 of Lemma 6.6).

Existence of graded projective resolutions

structure MultiplicativeBasisDeformations.GExt.FinGMod {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} : Type (max (u + 1) v)

A finite-dimensional graded module.

• X : Type u
• acg : AddCommGroup self.X
• mod : Module R self.X
• XX : GMod GΛ self.X
• fin : Module.Finite R self.X

noncomputable def MultiplicativeBasisDeformations.GExt.FinGMod.cov {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) (S : FinGMod) : Cover S.XX

A chosen finite free cover.

noncomputable def MultiplicativeBasisDeformations.GExt.FinGMod.next {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) [IsNoetherianRing R] [Module.Finite R Λ] (S : FinGMod) : FinGMod

The kernel of the chosen cover.

def MultiplicativeBasisDeformations.GExt.syz {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] (GΛ : GAlg Λ) [IsNoetherianRing R] [Module.Finite R Λ] (S : FinGMod) : ℕ → FinGMod

The syzygies.

theorem MultiplicativeBasisDeformations.GExt.exists_gres {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [IsNoetherianRing R] [Module.Finite R Λ] {M : Type u} [AddCommGroup M] [Module R M] [Module.Finite R M] (MM : GMod GΛ M) : Nonempty (GRes MM)

Every finite-dimensional graded module over a finite-dimensional graded algebra has a graded projective resolution (by finite free graded modules).

theorem MultiplicativeBasisDeformations.GExt.GRes.extVanish_iff_field {k : Type v} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {GΛ : GAlg Λ} {N : Type u_1} [AddCommGroup N] [Module k N] (NN : GMod GΛ N) (n : ℕ) {M : Type w} [AddCommGroup M] [Module k M] {MM : GMod GΛ M} (Rs : GRes MM) (t : ℤ) : Rs.ExtVanish NN n t ↔ GExt.ExtVanish MM NN n t

The comparison over a field: no projectivity hypotheses.