Products and transports of filtered lifts (toward Corollary 12.1) #
Filtered lifts in the sense of Proposition 6.5 (FLift) are stable under finite products with
shifted gradings (FLift.pi), and a B-stable subspace which is the image of an injective
filtered map with injective Λ-linear leading term carries a transported filtered lift
(FLift.transport): the leading-term arguments of deformation-refinements.tex.
theorem
MultiplicativeBasisDeformations.GExt.geAt_of_lead
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{r : ℤ}
{g : M →ₗ[k] N}
(hg : OrderGe MM NN r g)
(hinj : Function.Injective ⇑(MM.gr.comp NN.gr r g))
{t : ℤ}
{m : M}
(h : NN.gr.GeAt (t + r) (g m))
:
Reflecting filtration levels along a filtered map with injective leading term.
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.geAt_act
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{U : Type u_5}
[AddCommGroup U]
[Module k U]
{UU : GExt.GMod (GExt.GAlg.ofLen G h1) U}
(A : P.FLift h1 UU)
{t : ℤ}
{u : U}
(hu : UU.gr.GeAt t u)
{d : ℕ}
{x : B}
(hx : x ∈ P.F d)
:
The action of F^d B raises filtration levels by d.
def
MultiplicativeBasisDeformations.PosFiltration.FLift.pi
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{Ms : ι → Type u_7}
[(a : ι) → AddCommGroup (Ms a)]
[(a : ι) → Module k (Ms a)]
{MMs : (a : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms a)}
(A : (a : ι) → P.FLift h1 (MMs a))
(s : ι → ℤ)
:
P.FLift h1 (GExt.GMod.pi MMs s)
The product of filtered lifts, with shifted gradings.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.σ_isHom
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
(d : ℕ)
(x : B)
:
(GExt.GAlg.ofLen G h1).gr.IsHom (↑d) ((P.σ d) x)
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.transAct
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{M : Type u_4}
{U : Type u_5}
[AddCommGroup M]
[Module k M]
[AddCommGroup U]
[Module k U]
{UU : GExt.GMod (GExt.GAlg.ofLen G h1) U}
(A : P.FLift h1 UU)
(ι : M →ₗ[k] U)
(hι : Function.Injective ⇑ι)
(hstab : ∀ (m : M) (x : B), (A.act (ι m)) x ∈ ι.range)
(m : M)
(x : B)
:
M
The transported action.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.ι_transAct
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{M : Type u_4}
{U : Type u_5}
[AddCommGroup M]
[Module k M]
[AddCommGroup U]
[Module k U]
{UU : GExt.GMod (GExt.GAlg.ofLen G h1) U}
(A : P.FLift h1 UU)
(ι : M →ₗ[k] U)
(hι : Function.Injective ⇑ι)
(hstab : ∀ (m : M) (x : B), (A.act (ι m)) x ∈ ι.range)
(m : M)
(x : B)
:
noncomputable def
MultiplicativeBasisDeformations.PosFiltration.FLift.transport
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{M : Type u_4}
{U : Type u_5}
[AddCommGroup M]
[Module k M]
[AddCommGroup U]
[Module k U]
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{UU : GExt.GMod (GExt.GAlg.ofLen G h1) U}
(A : P.FLift h1 UU)
(ι : M →ₗ[k] U)
(hι : Function.Injective ⇑ι)
(hstab : ∀ (m : M) (x : B), (A.act (ι m)) x ∈ ι.range)
{r : ℤ}
(hord : GExt.OrderGe MM UU r ι)
(hlin : ∀ (m : M) (a : Λ), (MM.gr.comp UU.gr r ι) ((MM.act m) a) = (UU.act ((MM.gr.comp UU.gr r ι) m)) a)
(hinj : Function.Injective ⇑(MM.gr.comp UU.gr r ι))
:
P.FLift h1 MM
The transported filtered lift on a B-stable image of an injective filtered map with
injective Λ-linear leading term.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.transport_act
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type u_3}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{h1 : G.IsHom 0 1}
{M : Type u_4}
{U : Type u_5}
[AddCommGroup M]
[Module k M]
[AddCommGroup U]
[Module k U]
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{UU : GExt.GMod (GExt.GAlg.ofLen G h1) U}
(A : P.FLift h1 UU)
(ι : M →ₗ[k] U)
(hι : Function.Injective ⇑ι)
(hstab : ∀ (m : M) (x : B), (A.act (ι m)) x ∈ ι.range)
{r : ℤ}
(hord : GExt.OrderGe MM UU r ι)
(hlin : ∀ (m : M) (a : Λ), (MM.gr.comp UU.gr r ι) ((MM.act m) a) = (UU.act ((MM.gr.comp UU.gr r ι) m)) a)
(hinj : Function.Injective ⇑(MM.gr.comp UU.gr r ι))
(m : M)
(x : B)
: