Proposition 6.5(3): the radical filtration of the lifted category #
positive-deformations.tex: "Let E be the full category on the lifted modules. The
map-degree filtration has nilpotent positive part, and its degree-zero part is a product of
copies of k, one for each lifted module. Its first term is therefore the categorical radical.
Since the original graded Hom category is generated in degree one, descending induction
through the finite filtration identifies its qth term with the qth radical power."
Formalization. For a family of filtered lifts A i of graded modules M i, a morphism of E
is a B-linear map (IsBLin), the categorical radical is IsRad (1 − hg invertible for all
h), and its powers are radPow (spans of composites). Under the hypotheses of (3) the radical
is the filtration order ≥ 1 (isRad_iff), and the qth radical power is the filtration order
≥ q (mem_radPow_iff).
theorem
MultiplicativeBasisDeformations.GExt.OrderGe.comp
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
{X : Type u_5}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup X]
[Module R X]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{XX : GMod GΛ X}
{r s : ℤ}
{g : M →ₗ[R] N}
{h : N →ₗ[R] X}
(hg : OrderGe MM NN r g)
(hh : OrderGe NN XX s h)
:
OrderGe MM XX (r + s) (h ∘ₗ g)
theorem
MultiplicativeBasisDeformations.GExt.OrderGe.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]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{r : ℤ}
{g g' : M →ₗ[R] N}
(hg : OrderGe MM NN r g)
(hg' : OrderGe MM NN r g')
:
OrderGe MM NN r (g + g')
theorem
MultiplicativeBasisDeformations.GExt.OrderGe.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}
{r : ℤ}
(c : R)
{g : M →ₗ[R] N}
(hg : OrderGe MM NN r g)
:
OrderGe MM NN r (c • g)
theorem
MultiplicativeBasisDeformations.GExt.OrderGe.mono
{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}
{r r' : ℤ}
{g : M →ₗ[R] N}
(hg : OrderGe MM NN r g)
(h : r' ≤ r)
:
OrderGe MM NN r' g
theorem
MultiplicativeBasisDeformations.GExt.comp_comp_lead
{R : Type u_1}
[CommRing R]
{Λ : Type u_2}
[Ring Λ]
[Algebra R Λ]
{GΛ : GAlg Λ}
{M : Type u_3}
{N : Type u_4}
{X : Type u_5}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup X]
[Module R X]
{MM : GMod GΛ M}
{NN : GMod GΛ N}
{XX : GMod GΛ X}
{r s : ℤ}
{g : M →ₗ[R] N}
{h : N →ₗ[R] X}
(hg : OrderGe MM NN r g)
(hh : OrderGe NN XX s h)
:
The leading term of a composite is the composite of the leading terms.
def
MultiplicativeBasisDeformations.PosFiltration.IsBLin
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(i j : ι)
(g : Ms i →ₗ[k] Ms j)
:
A morphism of the lifted category: a B-linear map.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.isBLin_comp
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
{i j l : ι}
{g : Ms i →ₗ[k] Ms l}
{h : Ms l →ₗ[k] Ms j}
(hg : IsBLin A i l g)
(hh : IsBLin A l j h)
:
IsBLin A i j (h ∘ₗ g)
theorem
MultiplicativeBasisDeformations.PosFiltration.isBLin_id
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(i : ι)
:
IsBLin A i i LinearMap.id
def
MultiplicativeBasisDeformations.PosFiltration.IsRad
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(i j : ι)
(g : Ms i →ₗ[k] Ms j)
:
The categorical radical of the lifted category: 1 − hg is invertible for all h.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.bLin
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(i j : ι)
:
Submodule k (Ms i →ₗ[k] Ms j)
The B-linear maps, as a subspace.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.radPow
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
:
ℕ → (i j : ι) → Submodule k (Ms i →ₗ[k] Ms j)
The powers of the radical: rad⁰ = Hom, rad^{q+1} = rad · rad^q.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.IsGrHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(i j : ι)
(r : ℤ)
(f : Ms i →ₗ[k] Ms j)
:
A homogeneous Λ-linear map of degree r.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.grHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(i j : ι)
(r : ℤ)
:
Submodule k (Ms i →ₗ[k] Ms j)
The homogeneous Λ-linear maps of degree r, as a subspace.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.grPow
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
:
ℕ → (i j : ι) → Submodule k (Ms i →ₗ[k] Ms j)
The graded Hom category generated in degree one: grPow n is spanned by composites of
n + 1 homogeneous maps of degree one.
Instances For
structure
MultiplicativeBasisDeformations.PosFiltration.LiftHyp
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{h1 : G.IsHom 0 1}
{ι : Type}
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
(MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i))
:
The hypotheses of Proposition 6.5(3), with the Ext¹ vanishing of (2).
- off (i j : ι) : i ≠ j → ∀ (f : Ms i →ₗ[k] Ms j), IsGrHom i j 0 f → f = 0
- nontriv (i : ι) : Nontrivial (Ms i)
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.orderGe_zero_of_bLin
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
{i j : ι}
{g : Ms i →ₗ[k] Ms j}
(hg : IsBLin A i j g)
:
GExt.OrderGe (MM i) (MM j) 0 g
theorem
MultiplicativeBasisDeformations.PosFiltration.leading_isGrHom
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
{i j : ι}
{g : Ms i →ₗ[k] Ms j}
{r : ℤ}
(hg : IsBLin A i j g)
(hord : GExt.OrderGe (MM i) (MM j) r g)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.isRad_iff
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
(i j : ι)
(g : Ms i →ₗ[k] Ms j)
:
IsRad A i j g ↔ IsBLin A i j g ∧ GExt.OrderGe (MM i) (MM j) 1 g
The radical of the lifted category is the filtration order ≥ 1.
theorem
MultiplicativeBasisDeformations.PosFiltration.radPow_le_bLin
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(q : ℕ)
(i j : ι)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.radPow_succ_le
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(q : ℕ)
(i j : ι)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.orderGe_of_mem_radPow
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
(q : ℕ)
(i j : ι)
(g : Ms i →ₗ[k] Ms j)
:
g ∈ radPow A q i j → GExt.OrderGe (MM i) (MM j) (↑q) g
theorem
MultiplicativeBasisDeformations.PosFiltration.lift_grPow
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
(n : ℕ)
(i j : ι)
(f : Ms i →ₗ[k] Ms j)
:
Homogeneous maps generated in degree one lift into the radical powers.
theorem
MultiplicativeBasisDeformations.PosFiltration.OrderGe.eq_zero'
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
{i j : ι}
{q : ℕ}
{g : Ms i →ₗ[k] Ms j}
(hg : GExt.OrderGe (MM i) (MM j) (↑q) g)
(hq : GExt.degBound (MM i).gr + GExt.degBound (MM j).gr < q)
:
g = 0
theorem
MultiplicativeBasisDeformations.PosFiltration.mem_radPow_iff
{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}
{h1 : G.IsHom 0 1}
{ι : Type}
[DecidableEq ι]
{Ms : ι → Type u_1}
[(i : ι) → AddCommGroup (Ms i)]
[(i : ι) → Module k (Ms i)]
{MM : (i : ι) → GExt.GMod (GExt.GAlg.ofLen G h1) (Ms i)}
(A : (i : ι) → P.FLift h1 (MM i))
(hS : Nonempty P.Split)
(H : LiftHyp MM)
(hgen : ∀ (n : ℕ) (i j : ι) (f : Ms i →ₗ[k] Ms j), IsGrHom i j (↑(n + 1)) f → f ∈ grPow n i j)
(q : ℕ)
(i j : ι)
(g : Ms i →ₗ[k] Ms j)
:
g ∈ radPow A q i j ↔ IsBLin A i j g ∧ GExt.OrderGe (MM i) (MM j) (↑q) g
Proposition 6.5(3), the radical filtration: if the graded Hom category is generated in
degree one, the qth power of the radical of the lifted category consists of the B-linear
maps of filtration order ≥ q.