Lemma 3.7 for the categorical filtration #
projective-rays.tex (lem:ray-degree): "Write F^nA(x,y) = J^n(P_y,P_x) […] Every
space A₀(x,y)_d of degree d has dimension at most one, and initial forms give a bijection
between the nonzero rays of A and the nonzero spaces A₀(x,y)_d. If the endpoint
subbimodules satisfy U_{r'} ⊊ U_r, then deg_J(r') > deg_J(r)."
The proof only uses that the filtration is multiplicative, starts at A, ends at zero, and
contains the radical in degree one ("endpoint radicals belong to J"). We prove the lemma for
every positive filtered deformation P of a graded algebra Λ with this property
(PosFiltration.RadOne): the corner layers have dimension at most one
(finrank_corner_le), elements of one degree lie in one ray (ray_eq_of_degree), a smaller
subbimodule has a larger degree (degree_lt_of_lt), and the initial form σ_d maps the
corner F^dA(x,y) onto the corner Λ(x,y)_d of Λ cut out by the idempotents
σ₀(e_x), with kernel F^{d+1}A(x,y) (σ_piece_surj, finrank_piece_le).
For A itself, posFiltA is the filtration J^n of the source (FilteredA.lean), and the
radical lies in J¹ because the degree-zero part of A₀ has no nonzero nilpotents
(lenA0_noNil). This gives the literal Lemma 3.7 (IndSkeleton.rayDegree_J).
def
MultiplicativeBasisDeformations.PosFiltration.RadOne
{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)
:
The radical lies in degree one.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.σ_zero_mul
{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)
(a b : B)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.σ_zero_pow_succ
{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)
(a : B)
(n : ℕ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.radOne_of
{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)
[FiniteDimensional k B]
(h : ∀ (z : Λ), G.IsHom 0 z → IsNilpotent z → z = 0)
:
P.RadOne
The radical lies in F¹ when the degree-zero part of Λ has no nonzero nilpotents.
theorem
MultiplicativeBasisDeformations.PosFiltration.rad_mul_F
{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)
(hP : P.RadOne)
(d : ℕ)
{a z : B}
(ha : a ∈ algebraRadical k B)
(hz : z ∈ P.F d)
:
a * z ∈ P.F (d + 1)
theorem
MultiplicativeBasisDeformations.PosFiltration.F_mul_rad
{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)
(hP : P.RadOne)
(d : ℕ)
{a z : B}
(ha : a ∈ algebraRadical k B)
(hz : z ∈ P.F d)
:
z * a ∈ P.F (d + 1)
theorem
MultiplicativeBasisDeformations.PosFiltration.isEndpoint_F
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
:
F.IsEndpointSubbimodule x y (F.corner x y ⊓ P.F d)
theorem
MultiplicativeBasisDeformations.PosFiltration.endpointRadical_le_F
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
{x y : Fin F.m}
{g : B}
(hg : g ∈ F.corner x y)
{d : ℕ}
(hgd : g ∈ P.F d)
:
F.endpointRadical x y g ≤ F.corner x y ⊓ P.F (d + 1)
R(g) ⊆ F^{d+1} for g ∈ F^d: endpoint radicals belong to F¹.
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_corner_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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
(hA : IsRepresentationFinite k B)
(x y : Fin F.m)
(d : ℕ)
:
Each layer of the filtration of a corner has dimension at most one.
theorem
MultiplicativeBasisDeformations.PosFiltration.ray_eq_of_degree
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
{f g : B}
(hf : f ∈ F.corner x y)
(hg : g ∈ F.corner x y)
{d : ℕ}
(hfd : f ∈ P.F d)
(hfd' : f ∉ P.F (d + 1))
(hgd : g ∈ P.F d)
(hgd' : g ∉ P.F (d + 1))
:
Elements of the same degree lie in the same ray.
theorem
MultiplicativeBasisDeformations.PosFiltration.degree_lt_of_lt
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
{f g : B}
(hf : f ∈ F.corner x y)
(hg : g ∈ F.corner x y)
(hlt : F.endpointSpan x y g < F.endpointSpan x y f)
{d d' : ℕ}
(hfd : f ∈ P.F d)
(hgd' : g ∈ P.F d')
(hgd'' : g ∉ P.F (d' + 1))
:
d < d'
A strictly smaller subbimodule has a strictly larger degree.
theorem
MultiplicativeBasisDeformations.PosFiltration.exists_degree
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
{f : B}
(hf0 : f ≠ 0)
:
Every nonzero element has a degree.
theorem
MultiplicativeBasisDeformations.PosFiltration.mem_F_of_ray
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{f g : B}
(hg : g ∈ F.ray x y f)
{d : ℕ}
(hf : f ∈ P.F d)
:
g ∈ P.F d
The initial forms on corners #
def
MultiplicativeBasisDeformations.PosFiltration.piece
{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)
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
:
Submodule k Λ
The corner Λ(x, y)_d: degree-d elements of σ₀(e_x) Λ σ₀(e_y).
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.σ_corner_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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{d : ℕ}
{a : B}
(ha : a ∈ F.corner x y)
(had : a ∈ P.F d)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.σ_piece_surj
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{d : ℕ}
{z : Λ}
(hz : z ∈ P.piece F x y d)
:
Initial forms map the corner layers onto the corner pieces.
def
MultiplicativeBasisDeformations.PosFiltration.σCorner
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
:
The initial form on a corner layer.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.σCorner_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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
:
Function.Surjective ⇑(P.σCorner F x y d)
theorem
MultiplicativeBasisDeformations.PosFiltration.σCorner_ker
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
(a : ↥(F.corner x y ⊓ P.F d))
:
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_piece
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(x y : Fin F.m)
(d : ℕ)
:
dim Λ(x,y)_d = dim F^dA(x,y) - dim F^{d+1}A(x,y).
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_piece_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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
(hA : IsRepresentationFinite k B)
(x y : Fin F.m)
(d : ℕ)
:
Module.finrank k ↥(P.piece F x y d) ≤ 1
Lemma 3.7, first assertion: every piece Λ(x,y)_d has dimension at most one.
theorem
MultiplicativeBasisDeformations.PosFiltration.rayDegree
{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)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(hP : P.RadOne)
(hA : IsRepresentationFinite k B)
(x y : Fin F.m)
:
(∀ (d : ℕ), Module.finrank k ↥(P.piece F x y d) ≤ 1) ∧ (∀ (f : B) (d : ℕ),
f ∈ F.corner x y → f ∈ P.F d → f ∉ P.F (d + 1) → (P.σ d) f ≠ 0 ∧ P.piece F x y d = k ∙ (P.σ d) f) ∧ (∀ (f g : B) (d d' : ℕ),
f ∈ F.corner x y →
g ∈ F.corner x y →
f ∈ P.F d → f ∉ P.F (d + 1) → g ∈ P.F d' → g ∉ P.F (d' + 1) → (F.ray x y f = F.ray x y g ↔ d = d')) ∧ (∀ (d : ℕ), P.piece F x y d ≠ ⊥ → ∃ f ∈ F.corner x y, f ∈ P.F d ∧ f ∉ P.F (d + 1)) ∧ ∀ (f g : B),
f ∈ F.corner x y →
g ∈ F.corner x y →
F.endpointSpan x y g < F.endpointSpan x y f →
∀ (d d' : ℕ), f ∈ P.F d → g ∈ P.F d' → g ∉ P.F (d' + 1) → d < d'
Lemma 3.7, the bijection: a nonzero f of the corner of degree d has nonzero initial
form, which spans Λ(x,y)_d; two nonzero elements of a corner have the same ray iff they have
the same degree, and every nonzero piece is the initial form of a nonzero element.
The degree-zero part of A₀ #
def
MultiplicativeBasisDeformations.MeshWalk.IsDiag
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(z : (CatAlg.Alg D.F0)ᵐᵒᵖ)
(t : D.PV → k)
:
A diagonal scalar element ∑ t_p e_p of A₀.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.isDiag_mul
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{z w : (CatAlg.Alg D.F0)ᵐᵒᵖ}
{t s : D.PV → k}
(hz : IsDiag D z t)
(hw : IsDiag D w s)
:
IsDiag D (z * w) (s * t)
theorem
MultiplicativeBasisDeformations.MeshWalk.isDiag_pow
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
{z : (CatAlg.Alg D.F0)ᵐᵒᵖ}
{t : D.PV → k}
(hz : IsDiag D z t)
(n : ℕ)
:
IsDiag D (z ^ (n + 1)) (t ^ (n + 1))
theorem
MultiplicativeBasisDeformations.MeshWalk.isDiag_of_isHom
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{z : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hz : (lenA0 D hfin).IsHom 0 z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.lenA0_noNil
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(z : (CatAlg.Alg D.F0)ᵐᵒᵖ)
(hz : (lenA0 D hfin).IsHom 0 z)
(hn : IsNilpotent z)
:
z = 0
The degree-zero part of A₀ has no nonzero nilpotents.
Lemma 3.7 for A #
theorem
MultiplicativeBasisDeformations.IndSkeleton.posFiltA_radOne
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{n : ℕ}
{e : Fin n → A}
(he : CompleteOrthogonalIdempotents e)
(hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i))
(hbasic :
∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j)
:
The radical of A lies in J¹.
theorem
MultiplicativeBasisDeformations.IndSkeleton.rayDegree_J
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{n : ℕ}
{e : Fin n → A}
(he : CompleteOrthogonalIdempotents e)
(hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i))
(hbasic :
∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j)
(hA : IsRepresentationFinite k A)
(F : PrimitiveIdempotents A)
(x y : Fin F.m)
:
have P := S.posFiltA b he hprim hbasic;
(∀ (d : ℕ), Module.finrank k ↥(P.piece F x y d) ≤ 1) ∧ (∀ (f : A) (d : ℕ),
f ∈ F.corner x y → f ∈ P.F d → f ∉ P.F (d + 1) → (P.σ d) f ≠ 0 ∧ P.piece F x y d = k ∙ (P.σ d) f) ∧ (∀ (f g : A) (d d' : ℕ),
f ∈ F.corner x y →
g ∈ F.corner x y →
f ∈ P.F d → f ∉ P.F (d + 1) → g ∈ P.F d' → g ∉ P.F (d' + 1) → (F.ray x y f = F.ray x y g ↔ d = d')) ∧ (∀ (d : ℕ), P.piece F x y d ≠ ⊥ → ∃ f ∈ F.corner x y, f ∈ P.F d ∧ f ∉ P.F (d + 1)) ∧ ∀ (f g : A),
f ∈ F.corner x y →
g ∈ F.corner x y →
F.endpointSpan x y g < F.endpointSpan x y f →
∀ (d d' : ℕ), f ∈ P.F d → g ∈ P.F d' → g ∉ P.F (d' + 1) → d < d'
Lemma 3.7 (lem:ray-degree) for the categorical filtration F^dA(x,y) = J^d(P_y,P_x)
(posFiltA): in every corner, the pieces A₀(x,y)_d (cut out by the initial forms of the
idempotents) have dimension at most one; a nonzero element of degree d has nonzero initial
form spanning A₀(x,y)_d; two nonzero elements have the same ray iff they have the same
degree; every nonzero piece is reached; and U_{r'} ⊊ U_r forces deg_J r' > deg_J r.