Lemma 6.6 for graded Λ_μ-modules #
lem:square-zero-selected-lifts: "Put Λ_μ = (Λ ⊗_R R[ε]/(ε²), m + εμ), with deg ε = −q.
Then each M_i has a graded lift to Λ_μ that is free over R[ε]/(ε²), unique up to a graded
isomorphism reducing to the identity. Every homogeneous original map lifts."
SquareZero.lean records lifts by their first-order equations (ActLift, IsLiftHom). Here a
graded lift is a graded Λ_μ-module in the literal sense (MuMod): an R-module L with
ε of degree −q, ε² = 0, and an action of Λ (the elements a + 0ε of Λ_μ) commuting
with ε, with (l a) b = l(ab) + ε l μ(a, b) (the product of Λ_μ); free over R[ε]/(ε²)
(ker ε = im ε), with a graded Λ-linear identification L/εL = M. An ActLift gives the lift
M ⊕ εM (ActLift.toMuMod); conversely, a graded section of L → M identifies any such L
with the lift of an ActLift (MuMod.exists_model), which gives existence (exists_muMod),
uniqueness up to a graded isomorphism reducing to the identity (muMod_unique) and the lifting
of maps (muMod_mapLift) in this form.
Lifted actions from bilinear maps #
def
MultiplicativeBasisDeformations.GExt.ActLift.ofEq
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
(ν : M →ₗ[R] Λ →ₗ[R] M)
(hdeg : ∀ (p d : ℤ) (m : M) (a : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom d a → MM.gr.IsHom (p + d + q) ((ν m) a))
(heq : ∀ (m : M) (a b : Λ), (ν ((MM.act m) a)) b - (ν m) (a * b) + (MM.act ((ν m) a)) b = (MM.act m) ((μ a) b))
:
ActLift μ q MM
An ActLift from its bilinear correction ν(m, a), homogeneous of degree q and
satisfying ν(ma, b) − ν(m, ab) + ν(m, a)b = mμ(a, b).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ActLift.ofEq_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
(ν : M →ₗ[R] Λ →ₗ[R] M)
(hdeg : ∀ (p d : ℤ) (m : M) (a : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom d a → MM.gr.IsHom (p + d + q) ((ν m) a))
(heq : ∀ (m : M) (a b : Λ), (ν ((MM.act m) a)) b - (ν m) (a * b) + (MM.act ((ν m) a)) b = (MM.act m) ((μ a) b))
(m : M)
(a : Λ)
:
Graded Λ_μ-modules #
structure
MultiplicativeBasisDeformations.GExt.MuMod
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
(μ : Λ →ₗ[R] Λ →ₗ[R] Λ)
(q : ℤ)
(MM : GMod GΛ M)
(L : Type u_5)
[AddCommGroup L]
[Module R L]
:
Type (max (max u_2 u_3) u_5)
A graded lift of M to Λ_μ, free over R[ε]/(ε²): ε of degree −q with ε² = 0,
an action of Λ ⊂ Λ_μ commuting with ε with (l a) b = l(ab) + ε l μ(a, b) (the product
a ⋆ b = ab + εμ(a, b) of Λ_μ), ker ε = im ε, and a graded Λ-linear surjection
red : L → M with kernel εL.
- ε : L →ₗ[R] L
- act : L →ₗ[R] Λ →ₗ[R] L
- act_one (l : L) : (self.act l) 1 = l
- gr : ZGr L
- red : L →ₗ[R] M
- red_surj : Function.Surjective ⇑self.red
Instances For
The lift M ⊕ εM of an ActLift #
def
MultiplicativeBasisDeformations.GExt.ActLift.toMuMod
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
(L₀ : ActLift μ q MM)
(h11 : (μ 1) 1 = 0)
:
MuMod μ q MM (M × M)
The lift of an ActLift: M ⊕ εM as M × M (first coordinate the ε-part, of degree
shifted by q), with ε(n, m) = (m, 0) and (n, m) a = (na + ν(m, a), ma).
Instances For
Graded sections and the model of a lift #
theorem
MultiplicativeBasisDeformations.GExt.MuMod.red_ε
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(l : L)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.red_proj
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(p : ℤ)
(l : L)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.exists_section
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(hproj : ∀ (p : ℤ), Module.Projective R ↥(MM.gr.proj p).range)
:
A graded section of red : L → M, when the graded pieces of M are projective.
def
MultiplicativeBasisDeformations.GExt.MuMod.Ψ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(s : M →ₗ[R] L)
:
M × M →ₗ[R] L
M ⊕ εM → L, (n, m) ↦ s m + ε s n.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_apply
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(x : M × M)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.red_Ψ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(x : M × M)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.ε_eq
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(l : L)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_bijective
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
:
Function.Bijective ⇑(X.Ψ s)
noncomputable def
MultiplicativeBasisDeformations.GExt.MuMod.Ψe
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
:
(M × M) ≃ₗ[R] L
Ψ as a linear isomorphism.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψe_apply
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(x : M × M)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_hom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hsh : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → X.gr.IsHom p (s m))
{p : ℤ}
{x : M × M}
(hx : (twistGr q).IsHom p x)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_symm_hom
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(hsh : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → X.gr.IsHom p (s m))
{p : ℤ}
{l : L}
(hl : X.gr.IsHom p l)
:
noncomputable def
MultiplicativeBasisDeformations.GExt.MuMod.νb
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(s : M →ₗ[R] L)
(hs : ∀ (m : M), X.red (s m) = m)
:
M →ₗ[R] Λ →ₗ[R] M
The correction ν(m, a) of the lift L, read off through Ψ.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_symm_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(m : M)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.Ψ_symm_ε
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(l : L)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.act_Ψ
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(x : M × M)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.νb_deg
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(hsh : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → X.gr.IsHom p (s m))
(p d : ℤ)
(m : M)
(a : Λ)
(hm : MM.gr.IsHom p m)
(ha : GΛ.gr.IsHom d a)
:
theorem
MultiplicativeBasisDeformations.GExt.MuMod.νb_eq
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(m : M)
(a b : Λ)
:
noncomputable def
MultiplicativeBasisDeformations.GExt.MuMod.toActLift
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
{s : M →ₗ[R] L}
(hs : ∀ (m : M), X.red (s m) = m)
(hsh : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → X.gr.IsHom p (s m))
:
ActLift μ q MM
The ActLift of a lift, through a graded section.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.MuMod.exists_model
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{L : Type u_5}
[AddCommGroup L]
[Module R L]
(X : MuMod μ q MM L)
(hproj : ∀ (p : ℤ), Module.Projective R ↥(MM.gr.proj p).range)
:
Every graded Λ_μ-lift is the lift M ⊕ εM of an ActLift: there is a graded linear
isomorphism M × M ≅ L carrying ε(n, m) = (m, 0) to ε and (n, m) a = (na + ν(m,a), ma) to
the action, and reducing to the identity.
Lemma 6.6 for graded Λ_μ-modules #
theorem
MultiplicativeBasisDeformations.GExt.exists_muMod
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
(h11 : (μ 1) 1 = 0)
(h : ExtVanish MM MM 1 q)
:
Nonempty (MuMod μ q MM (M × M))
Lemma 6.6, existence: under Ext²_Λ(M, M)_q = 0, M has a graded lift to Λ_μ, free
over R[ε]/(ε²) (for a normalized cocycle: μ(1, 1) = 0).
theorem
MultiplicativeBasisDeformations.GExt.muMod_unique
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
(hproj : ∀ (p : ℤ), Module.Projective R ↥(MM.gr.proj p).range)
(h : ExtVanish MM MM 0 q)
{L : Type u_5}
{L' : Type u_6}
[AddCommGroup L]
[Module R L]
[AddCommGroup L']
[Module R L']
(X : MuMod μ q MM L)
(Y : MuMod μ q MM L')
:
Lemma 6.6, uniqueness: under Ext¹_Λ(M, M)_q = 0 (and graded pieces of M projective
over R, e.g. M free), two graded lifts of M to Λ_μ free over R[ε]/(ε²) are isomorphic by
a graded Λ_μ-linear isomorphism reducing to the identity.
theorem
MultiplicativeBasisDeformations.GExt.muMod_mapLift
{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]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{r : ℤ}
(hprojM : ∀ (p : ℤ), Module.Projective R ↥(MM.gr.proj p).range)
(hprojN : ∀ (p : ℤ), Module.Projective R ↥(NN.gr.proj p).range)
{L : Type u_5}
{L' : Type u_6}
[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))
(h : ExtVanish MM NN 0 (r + q))
:
Lemma 6.6, maps lift: under Ext¹_Λ(M, N)_{r+q} = 0, a Λ-linear map f : M → N of
degree r lifts to a graded Λ_μ-linear map F : L → L' of degree r between graded lifts,
reducing to f.
theorem
MultiplicativeBasisDeformations.GExt.modelHom_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]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
(L₀ : ActLift μ q MM)
(L₀' : ActLift μ q NN)
(F : M × M →ₗ[R] N × N)
:
Λ_μ-linear maps between lifts M ⊕ εM → N ⊕ εN are exactly (n, m) ↦ (f n + g m, f m)
with f + εg a lifted map (IsLiftHom): so the lifted Hom modules are the equation-form ones,
free over R[ε]/(ε²) on lifts of a basis (liftHom_basis).