Multiplicative bases

MultiplicativeBasisDeformations.Refinements.ResolutionForms

Proposition 6.5 and Lemma 6.6 with Ext from graded projective resolutions #

The Ext hypotheses of prop:positive-module-lifting and lem:square-zero-selected-lifts are stated in the manuscript with Ext in its own sense (positive-deformations.tex: degree-t maps from a graded projective resolution). Here the Lean statements are given with exactly these hypotheses, for a chosen graded projective resolution of the source module, through the comparison GRes.extVanish_iff:

source
theorem MultiplicativeBasisDeformations.GExt.proj_pieces_of_projective {R : Type u_1} [CommRing R] {X : Type u_2} [AddCommGroup X] [Module R X] [Module.Projective R X] (g : ZGr X) (q : ℤ) :
Module.Projective R ↥(g.proj q).range

The graded pieces of a module projective over R are projective (they are direct summands).

source
theorem MultiplicativeBasisDeformations.GExt.res_bar {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [Module.Projective R Λ] {M N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Projective R M] [Module.Projective R N] {MM : GMod GΛ M} (Rs : GRes MM) (XX : GMod GΛ N) (n : ℕ) (t : ℤ) :
Rs.ExtVanish XX n t ↔ ExtVanish MM XX n t
source
theorem MultiplicativeBasisDeformations.GExt.res_bar_self {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [Module.Projective R Λ] {M : Type w} [AddCommGroup M] [Module R M] [Module.Projective R M] {MM : GMod GΛ M} (Rs : GRes MM) (n : ℕ) (t : ℤ) :
Rs.ExtVanish MM n t ↔ ExtVanish MM MM n t
source
theorem MultiplicativeBasisDeformations.GExt.exists_muMod_res {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [Module.Projective R Λ] {M : Type w} [AddCommGroup M] [Module R M] [Module.Projective R M] {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : GMod GΛ M} (hq : HDeg GΛ μ q) (hμ : IsHCocycle μ) (h11 : (μ 1) 1 = 0) (Rs : GRes MM) (h : Rs.ExtVanish MM 1 q) :
Nonempty (MuMod μ q MM (M × M))

Lemma 6.6, existence, with Ext²_Λ(M, M)_q = 0 computed from a graded projective resolution of M.

source
theorem MultiplicativeBasisDeformations.GExt.muMod_unique_res {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [Module.Projective R Λ] {M : Type w} [AddCommGroup M] [Module R M] [Module.Projective R M] {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : GMod GΛ M} (Rs : GRes MM) (h : Rs.ExtVanish MM 0 q) {L : Type u_1} {L' : Type u_2} [AddCommGroup L] [Module R L] [AddCommGroup L'] [Module R L'] (X : MuMod μ q MM L) (Y : MuMod μ q MM L') :
∃ (Φ : L ≃ₗ[R] L'), (∀ (l : L) (a : Λ), Φ ((X.act l) a) = (Y.act (Φ l)) a) ∧ (∀ (l : L), Φ (X.ε l) = Y.ε (Φ l)) ∧ (∀ (l : L), Y.red (Φ l) = X.red l) ∧ ∀ (p : ℤ) (l : L), X.gr.IsHom p l → Y.gr.IsHom p (Φ l)

Lemma 6.6, uniqueness, with Ext¹_Λ(M, M)_q = 0 computed from a graded projective resolution of M.

source
theorem MultiplicativeBasisDeformations.GExt.muMod_mapLift_res {R : Type v} [CommRing R] {Λ : Type u} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} [Module.Projective R Λ] {M N : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Projective R M] [Module.Projective R N] {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : GMod GΛ M} {NN : GMod GΛ N} {r : ℤ} (Rs : GRes MM) (h : Rs.ExtVanish NN 0 (r + q)) {L : Type u_1} {L' : Type u_2} [AddCommGroup L] [Module R L] [AddCommGroup L'] [Module R L'] (X : MuMod μ q MM L) (Y : MuMod μ q NN L') (f : M →ₗ[R] N) (hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) (hfdeg : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) :
∃ (F : L →ₗ[R] L'), (∀ (l : L) (a : Λ), F ((X.act l) a) = (Y.act (F l)) a) ∧ (∀ (l : L), F (X.ε l) = Y.ε (F l)) ∧ (∀ (l : L), Y.red (F l) = f (X.red l)) ∧ ∀ (p : ℤ) (l : L), X.gr.IsHom p l → Y.gr.IsHom (p + r) (F l)

Lemma 6.6, maps lift, with Ext¹_Λ(M, N)_{r+q} = 0 computed from a graded projective resolution of M.

source
theorem MultiplicativeBasisDeformations.GExt.lemma66_Z4 {Λ : Type u} [Ring Λ] [Algebra (ZMod 4) Λ] {GΛ : GAlg Λ} [Module.Free (ZMod 4) Λ] {M N : Type w} [AddCommGroup M] [Module (ZMod 4) M] [AddCommGroup N] [Module (ZMod 4) N] [Module.Free (ZMod 4) M] [Module.Free (ZMod 4) N] {μ : Λ →ₗ[ZMod 4] Λ →ₗ[ZMod 4] Λ} {q : ℤ} {MM : GMod GΛ M} {NN : GMod GΛ N} (hq : HDeg GΛ μ q) (hμ : IsHCocycle μ) (h11 : (μ 1) 1 = 0) (Rs : GRes MM) :
(Rs.ExtVanish MM 1 q → Nonempty (MuMod μ q MM (M × M))) ∧ (Rs.ExtVanish MM 0 q → ∀ {L L' : Type w} [inst : AddCommGroup L] [inst_1 : Module (ZMod 4) L] [inst_2 : AddCommGroup L'] [inst_3 : Module (ZMod 4) L'] (X : MuMod μ q MM L) (Y : MuMod μ q MM L'), ∃ (Φ : L ≃ₗ[ZMod 4] L'), (∀ (l : L) (a : Λ), Φ ((X.act l) a) = (Y.act (Φ l)) a) ∧ (∀ (l : L), Φ (X.ε l) = Y.ε (Φ l)) ∧ (∀ (l : L), Y.red (Φ l) = X.red l) ∧ ∀ (p : ℤ) (l : L), X.gr.IsHom p l → Y.gr.IsHom p (Φ l)) ∧ ∀ {r : ℤ}, Rs.ExtVanish NN 0 (r + q) → ∀ {L L' : Type w} [inst : AddCommGroup L] [inst_1 : Module (ZMod 4) L] [inst_2 : AddCommGroup L'] [inst_3 : Module (ZMod 4) L'] (X : MuMod μ q MM L) (Y : MuMod μ q NN L') (f : M →ₗ[ZMod 4] N), (∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) → (∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) → ∃ (F : L →ₗ[ZMod 4] L'), (∀ (l : L) (a : Λ), F ((X.act l) a) = (Y.act (F l)) a) ∧ (∀ (l : L), F (X.ε l) = Y.ε (F l)) ∧ (∀ (l : L), Y.red (F l) = f (X.red l)) ∧ ∀ (p : ℤ) (l : L), X.gr.IsHom p l → Y.gr.IsHom (p + r) (F l)

Lemma 6.6 over ℤ/4, as stated: Λ a graded ℤ/4-algebra free over ℤ/4, M, N graded modules free over ℤ/4, Ext computed from graded projective resolutions of M. Under Ext²(M, M)_q = 0 the lift exists, under Ext¹(M, M)_q = 0 it is unique up to a graded isomorphism reducing to the identity, and under Ext¹(M, N)_{r+q} = 0 maps lift.

source
theorem MultiplicativeBasisDeformations.PosFiltration.exists_genLift_res {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {M : Type u_1} [AddCommGroup M] [Module k M] {h1 : G.IsHom 0 1} {MM : GExt.GMod (GExt.GAlg.ofLen G h1) M} (hS : Nonempty P.Split) (Rs : GExt.GRes MM) (hExt : ∀ (t : ℕ), 0 < t → Rs.ExtVanish MM 1 ↑t) :
Nonempty (P.GenLift h1 MM M)

Proposition 6.5(1), existence, with Ext²_Λ(M, M)_t = 0 (t > 0) computed from a graded projective resolution of M.

source
theorem MultiplicativeBasisDeformations.PosFiltration.genLift_unique_res {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {M : Type u_1} [AddCommGroup M] [Module k M] {h1 : G.IsHom 0 1} {MM : GExt.GMod (GExt.GAlg.ofLen G h1) M} (hS : Nonempty P.Split) (Rs : GExt.GRes MM) (hExt : ∀ (t : ℕ), 0 < t → Rs.ExtVanish MM 0 ↑t) {L : Type u_3} {L' : Type u_4} [AddCommGroup L] [Module k L] [AddCommGroup L'] [Module k L'] (X : P.GenLift h1 MM L) (Y : P.GenLift h1 MM L') :
∃ (Ψ : L ≃ₗ[k] L'), (∀ (n : L) (x : B), Ψ ((X.act n) x) = (Y.act (Ψ n)) x) ∧ ∀ (p : ℤ), ∀ n ∈ X.F p, Ψ n ∈ Y.F p ∧ (Y.ι p) (Ψ n) = (X.ι p) n

Proposition 6.5(1), uniqueness, with Ext¹_Λ(M, M)_t = 0 (t > 0) computed from a graded projective resolution of M.

source
theorem MultiplicativeBasisDeformations.PosFiltration.fLift_map_res {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {h1 : G.IsHom 0 1} {MM : GExt.GMod (GExt.GAlg.ofLen G h1) M} {NN : GExt.GMod (GExt.GAlg.ofLen G h1) N} (hS : Nonempty P.Split) (Rs : GExt.GRes MM) (A : P.FLift h1 MM) (A' : P.FLift h1 NN) (r : ℕ) (f : M →ₗ[k] 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 → Rs.ExtVanish NN 0 (↑r + ↑t)) :
∃ (Φ : M →ₗ[k] N), (∀ (m : M) (x : B), Φ ((A.act m) x) = (A'.act (Φ m)) x) ∧ GExt.OrderGe MM NN (↑r) Φ ∧ MM.gr.comp NN.gr (↑r) Φ = f

Proposition 6.5(2), maps lift, with Ext¹_Λ(M, N)_{r+t} = 0 (t > 0) computed from a graded projective resolution of M.