Proposition 6.5(1) for arbitrary filtered lifts #
prop:positive-module-lifting(1): "Each M_i has a filtered lift M_i^B with gr M_i^B = M_i,
unique up to an isomorphism with prescribed leading identity."
FLift is a B-action on the graded space M itself. Here a filtered lift is any right
B-module N with a finite decreasing filtration F^p N, compatible with the filtration of B,
and an identification gr N = M of graded Λ-modules: symbols ι_p : F^p N → M_p, onto, with
kernel F^{p+1} N, and ι_{p+d}(n x) = ι_p(n) σ_d(x) (GenLift). As in the source, choosing
linear sections of the ι_p identifies N with M as filtered spaces and carries the action to
an FLift (GenLift.exists_model). Hence a lift exists (exists_genLift) and two filtered lifts
are isomorphic by a B-linear isomorphism preserving the filtrations with leading term the
identity (genLift_unique).
structure
MultiplicativeBasisDeformations.PosFiltration.GenLift
{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)
(N : Type u_2)
[AddCommGroup N]
[Module k N]
:
Type (max (max u_1 u_2) w)
A filtered lift of M to B: a right B-module N with a finite decreasing filtration
compatible with that of B and an identification gr N = M of graded Λ-modules, given by
symbols ι_p : F^p N → M_p, onto, with kernel F^{p+1} N, and multiplicative.
- act : N →ₗ[k] B →ₗ[k] N
- one (n : N) : (self.act n) 1 = n
- F : ℤ → Submodule k N
- top : ∃ (p₀ : ℤ), self.F p₀ = ⊤
- bot : ∃ (p₁ : ℤ), self.F p₁ = ⊥
- ι : ℤ → N →ₗ[k] M
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.F_anti
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
{p q : ℤ}
(h : p ≤ q)
:
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.PosFiltration.GenLift.Mp
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(p : ℤ)
:
Submodule k M
The homogeneous part M_p.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.GenLift.ιr
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
:
The symbol on F^p N, onto M_p.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ιr_surjective
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
:
(L.ιr p).range = ⊤
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.GenLift.sec
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
:
M →ₗ[k] N
A linear section of ι_p on the degree-p part.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.sec_mem
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
(m : M)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ι_sec
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
(m : M)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.sec_eq_zero
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(p : ℤ)
{m : M}
(hm : (MM.gr.proj p) m = 0)
:
(L.sec p) m = 0
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.GenLift.ψ
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
:
M →ₗ[k] N
The identification M ≅ N assembled from the sections.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.GenLift.Ge
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(p : ℤ)
(m : M)
:
M_{≥ p}: the elements with no components below p.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ψ_mem_ι
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
{p : ℤ}
{m : M}
(hm : Ge p m)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ge_of_le
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{p q : ℤ}
{m : M}
(h : p ≤ q)
(hm : Ge q m)
:
Ge p m
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.exists_lowest
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{m : M}
(hm : m ≠ 0)
:
An element with a nonzero component has a lowest one.
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ge_of_ψ_mem
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
{p : ℤ}
{m : M}
(h : L.ψ m ∈ L.F p)
:
Ge p m
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ψ_injective
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
:
Function.Injective ⇑L.ψ
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.ψ_surjective
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
:
Function.Surjective ⇑L.ψ
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.GenLift.ψe
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
:
M ≃ₗ[k] N
ψ as a linear isomorphism.
Instances For
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.GenLift.model
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
:
P.FLift h1 MM
The model of a filtered lift on M (exists_model).
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.GenLift.model_act
{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}
{N : Type u_2}
[AddCommGroup N]
[Module k N]
(L : P.GenLift h1 MM N)
(m : M)
(x : B)
:
def
MultiplicativeBasisDeformations.PosFiltration.FLift.toGenLift
{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}
(A : P.FLift h1 MM)
:
P.GenLift h1 MM M
A lift on M is a filtered lift, with the degree filtration.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.exists_genLift
{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)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 1 ↑t)
:
Nonempty (P.GenLift h1 MM M)
Proposition 6.5(1), existence: under Ext²_Λ(M, M)_t = 0 for t > 0, M has a filtered
lift (on M itself, with the degree filtration).
theorem
MultiplicativeBasisDeformations.PosFiltration.genLift_unique
{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)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 0 ↑t)
{N : Type u_2}
{N' : Type u_3}
[AddCommGroup N]
[Module k N]
[AddCommGroup N']
[Module k N']
(L : P.GenLift h1 MM N)
(L' : P.GenLift h1 MM N')
:
Proposition 6.5(1), uniqueness for arbitrary filtered lifts: under Ext¹_Λ(M, M)_t = 0
for t > 0, two filtered lifts N, N' of M are isomorphic by a B-linear isomorphism
preserving the filtrations with leading term the identity: ι'_p(Ψ n) = ι_p(n) on F^p N.