Square-zero lifts of modules and maps (Lemma 6.6) #
positive-deformations.tex (lem:square-zero-selected-lifts): for a
Hochschild two-cocycle μ of internal degree q > 0 of a graded algebra Λ
over R (a field or ℤ/4), put Λ_μ = (Λ ⊗ R[ε]/(ε²), m + εμ). "Write a
lifted action as ma + εν_i(m,a). Its equation is
ν_i(ma,b) − ν_i(m,ab) + ν_i(m,a)b = mμ(a,b). […] The degree-q Ext²
vanishing supplies ν_i. […] The difference of two solutions is a bar
one-cocycle of degree q; the Ext¹ vanishing makes it the coboundary of a
degree-q coordinate change. […] For a degree-r map f, write its lift as
f + εg. Its equation is g(ma) − g(m)a = ν_j(f(m),a) − f(ν_i(m,a)). […] Since
r ≥ 0, the Ext¹ vanishing supplies g. […] Let F_1, …, F_h lift a basis
f_1, …, f_h of an original Hom module […] This proves freeness."
Formalization: the lifted module and maps are recorded by their first-order
equations (ActLift, IsLiftHom), with R[ε]-linear structure
ε·(f, g) = (0, f); the regular lift at a cyclic projective is ν = μ
(CycProj.actLift, the paper's "If M_i = e_xΛ, the regular module e_xΛ_μ
is such a lift"). The additional gradings of the lemma are in SquareZeroWeight.lean.
def
MultiplicativeBasisDeformations.GExt.IsHCocycle
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
(μ : Λ →ₗ[R] Λ →ₗ[R] Λ)
:
The Hochschild cocycle equation aμ(b,c) − μ(ab,c) + μ(a,bc) − μ(a,b)c = 0.
Instances For
def
MultiplicativeBasisDeformations.GExt.muCochain
{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] Λ)
(MM : GMod GΛ M)
:
Bar.Cochain Λ (M →ₗ[R] M)
The bar two-cochain (m, a, b) ↦ m μ(a, b).
Instances For
Lifted actions #
structure
MultiplicativeBasisDeformations.GExt.ActLift
{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)
:
Type (max u_2 u_3)
A first-order lift of the action of M to Λ_μ: m * a = ma + εν(m,a).
- ν : Bar.Cochain Λ (M →ₗ[R] M)
Instances For
theorem
MultiplicativeBasisDeformations.GExt.exists_actLift
{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 : ℤ}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
(MM : GMod GΛ M)
(h : ExtVanish MM MM 1 q)
:
Nonempty (ActLift μ q MM)
def
MultiplicativeBasisDeformations.GExt.ActLift.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 : ActLift μ q MM)
(m : M)
(a : Λ)
:
M
The correction ν(m, a).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ActLift.act_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 : ActLift μ q MM)
{p d : ℤ}
{m : M}
{a : Λ}
(hm : MM.gr.IsHom p m)
(ha : GΛ.gr.IsHom d a)
:
theorem
MultiplicativeBasisDeformations.GExt.ActLift.equation
{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)
(m : M)
(a b : Λ)
:
The lifted action equation ν(ma,b) − ν(m,ab) + ν(m,a)b = mμ(a,b).
theorem
MultiplicativeBasisDeformations.GExt.ActLift.exists_iso
{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 L' : ActLift μ q MM)
(h : ExtVanish MM MM 0 q)
:
Uniqueness of lifted actions up to a coordinate change 1 + εh of degree q.
Linearity in the cocycle #
theorem
MultiplicativeBasisDeformations.GExt.d_homAct_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}
(n : ℕ)
(t : R)
(F : Bar.Cochain Λ (M →ₗ[R] N))
:
def
MultiplicativeBasisDeformations.GExt.ActLift.add
{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)
(L' : ActLift μ' q MM)
:
ActLift (μ + μ') q MM
The sum of lifted actions for μ and μ' is one for μ + μ'.
Instances For
def
MultiplicativeBasisDeformations.GExt.ActLift.smul
{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)
(t : R)
:
ActLift (t • μ) q MM
A scalar multiple of a lifted action.
Instances For
def
MultiplicativeBasisDeformations.GExt.hcobdry
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
(h : Λ →ₗ[R] Λ)
:
Λ →ₗ[R] Λ →ₗ[R] Λ
The coboundary dh(a,b) = a h(b) − h(ab) + h(a) b.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.hcobdry_apply
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
(h : Λ →ₗ[R] Λ)
(a b : Λ)
:
((hcobdry h) a) b = a * h b - h (a * b) + h a * b
def
MultiplicativeBasisDeformations.GExt.ActLift.cobdry
{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] Λ}
(h : Λ →ₗ[R] Λ)
{q : ℤ}
{MM : GMod GΛ M}
(L : ActLift μ q MM)
(hdeg : ∀ (p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom (p + q) (h a))
:
Transport of a lifted action along a coboundary: ν'(m, a) = ν(m, a) + m h(a).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.ActLift.cobdry_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] Λ}
(h : Λ →ₗ[R] Λ)
{q : ℤ}
{MM : GMod GΛ M}
(L : ActLift μ q MM)
(hdeg : ∀ (p : ℤ) (a : Λ), GΛ.gr.IsHom p a → GΛ.gr.IsHom (p + q) (h a))
(m : M)
(a : Λ)
:
Regular lifts of cyclic projectives #
def
MultiplicativeBasisDeformations.GExt.CycProj.actLift
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{P : Type u_5}
[AddCommGroup P]
[Module R P]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
{PP : GMod GΛ P}
(C : CycProj PP)
:
ActLift μ q PP
The regular lift ν(m, a) = g·μ(ψ m, a) of a cyclic projective eΛ⟨b⟩.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.CycProj.actLift_act
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{P : Type u_5}
[AddCommGroup P]
[Module R P]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
(hq : HDeg GΛ μ q)
(hμ : IsHCocycle μ)
{PP : GMod GΛ P}
(C : CycProj PP)
(m : P)
(a : Λ)
:
Lifted maps #
def
MultiplicativeBasisDeformations.GExt.IsLiftHom
{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] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q : ℤ}
(L : ActLift μ q MM)
(L' : ActLift μ q NN)
(f g : M →ₗ[R] N)
:
A lifted map f + εg : M^μ → N^μ.
Instances For
theorem
MultiplicativeBasisDeformations.GExt.isLiftHom_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]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q : ℤ}
(L : ActLift μ q MM)
(L' : ActLift μ q NN)
(g : M →ₗ[R] N)
:
theorem
MultiplicativeBasisDeformations.GExt.IsLiftHom.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]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q : ℤ}
{L : ActLift μ q MM}
{L' : ActLift μ q NN}
{f g f' g' : M →ₗ[R] N}
(h : IsLiftHom L L' f g)
(h' : IsLiftHom L L' f' g')
:
IsLiftHom L L' (f + f') (g + g')
theorem
MultiplicativeBasisDeformations.GExt.IsLiftHom.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]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q : ℤ}
{L : ActLift μ q MM}
{L' : ActLift μ q NN}
{f g : M →ₗ[R] N}
(h : IsLiftHom L L' f g)
(c : R)
:
IsLiftHom L L' (c • f) (c • g)
theorem
MultiplicativeBasisDeformations.GExt.IsLiftHom.comp
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup P]
[Module R P]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{PP : GMod GΛ P}
{q : ℤ}
{L : ActLift μ q MM}
{L' : ActLift μ q NN}
{L'' : ActLift μ q PP}
{f g : M →ₗ[R] N}
{f' g' : N →ₗ[R] P}
(h' : IsLiftHom L' L'' f' g')
(h : IsLiftHom L L' f g)
:
IsLiftHom L L'' (f' ∘ₗ f) (f' ∘ₗ g + g' ∘ₗ f)
Composition of lifted maps: (f' + εg')(f + εg) = f'f + ε(f'g + g'f).
theorem
MultiplicativeBasisDeformations.GExt.exists_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] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q r : ℤ}
(L : ActLift μ q MM)
(L' : ActLift μ q NN)
(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))
:
Existence of map lifts (r ≥ 0, using Ext¹_{r+q} = 0).
theorem
MultiplicativeBasisDeformations.GExt.liftHom_basis
{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] Λ}
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{q : ℤ}
{L : ActLift μ q MM}
{L' : ActLift μ q NN}
{ι : Type u_6}
[Fintype ι]
(fs gs : ι → M →ₗ[R] N)
(hbasis :
∀ (f : M →ₗ[R] N), (∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) → ∃! c : ι → R, f = ∑ l : ι, c l • fs l)
(hgs : ∀ (l : ι), IsLiftHom L L' (fs l) (gs l))
{f g : M →ₗ[R] N}
(hfg : IsLiftHom L L' f g)
:
∃! cc : (ι → R) × (ι → R), f = ∑ l : ι, cc.1 l • fs l ∧ g = ∑ l : ι, cc.1 l • gs l + ∑ l : ι, cc.2 l • fs l
Freeness of lifted Hom modules: lifts (f_l, g_l) of a basis f_l of the
original Hom module form an R[ε]-basis, i.e. every lifted map is uniquely
Σ c_l (f_l, g_l) + Σ c'_l ε(f_l, g_l) with ε(f, g) = (0, f).
Trivializing derivations #
The algebra step of the injectivity in Proposition 7.6 (weights-and-parameters.tex):
a lift of the left multiplications to the lifted regular module, written through its value
Δ on the regular module and split by a complete family of idempotents, makes μ a
coboundary.
theorem
MultiplicativeBasisDeformations.GExt.hcocycle_sum_one
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{ι : Type u_6}
[Fintype ι]
(e : ι → Λ)
(he : ∀ (i : ι), e i * e i = e i)
(h1 : ∑ i : ι, e i = 1)
(hμ : IsHCocycle μ)
(a b : Λ)
:
∑ i : ι, ((μ (e i)) (e i * (a * b)) - (μ (e i)) (e i * a) * b + e i * (μ (e i * a)) b) = (μ a) b
theorem
MultiplicativeBasisDeformations.GExt.hcocycle_sum_two
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{ι : Type u_6}
[Fintype ι]
(e : ι → Λ)
(he : ∀ (i : ι), e i * e i = e i)
(h1 : ∑ i : ι, e i = 1)
(hμ : IsHCocycle μ)
(b : Λ)
:
∑ i : ι, ((μ (e i)) (e i * b) + e i * (μ (e i)) b) = ((μ 1) 1 + ∑ i : ι, (μ (e i)) (e i)) * b
theorem
MultiplicativeBasisDeformations.GExt.eq_hcobdry_of_derivation
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{ι : Type u_6}
[Fintype ι]
(e : ι → Λ)
(he : ∀ (i : ι), e i * e i = e i)
(h1 : ∑ i : ι, e i = 1)
(hμ : IsHCocycle μ)
(Δ : Λ →ₗ[R] Λ)
(hΔ :
∀ (x c : Λ),
Δ (x * c) - x * Δ c - (Δ x - x * Δ 1) * c = ∑ i : ι, e i * (μ (e i * x)) c - x * ∑ i : ι, e i * (μ (e i)) c)
:
μ = hcobdry
(LinearMap.mulLeft R ((μ 1) 1 + ∑ i : ι, (μ (e i)) (e i) + Δ 1) - ∑ i : ι, μ (e i) ∘ₗ LinearMap.mulLeft R (e i) - Δ)
A trivializing derivation makes μ a coboundary.