Homogeneous layers of a graded representation-finite algebra #
Proposition 3.8(1) and Corollary 3.3 (projective-rays.tex),
for an algebra graded by path length, as used for A₀ in Proposition 4.14:
"Every endpoint subbimodule is homogeneous: the automorphisms that multiply a
degree-d vector by a^d, for a ∈ k*, preserve its dimension, and the chain
has at most one member of each dimension. Since k is infinite, invariance
under those automorphisms implies homogeneity. A homogeneous lift of the
one-dimensional top generates each cyclic subbimodule, and positive endpoint
degrees make successive layers have strictly increasing degrees." and "In each
corner, the chosen vectors represent the consecutive one-dimensional quotients
of a finite chain. They therefore form a basis adapted to every member of that
chain. The intersection of a two-sided ideal with the corner is one such
member."
LenGrading is a grading of the algebra by ℕ with homogeneous products; the
scaling maps σ_t (scale) are multiplicative.
structure
MultiplicativeBasisDeformations.LenGrading
(k : Type u)
[Field k]
(B : Type v)
[Ring B]
[Algebra k B]
:
Type v
A grading by length with homogeneous products.
- proj : ℕ → B →ₗ[k] B
- N : ℕ
Instances For
def
MultiplicativeBasisDeformations.LenGrading.IsHom
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(d : ℕ)
(a : B)
:
A homogeneous element of degree d.
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.isHom_proj
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(d : ℕ)
(a : B)
:
theorem
MultiplicativeBasisDeformations.LenGrading.proj_of_isHom
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{d e : ℕ}
{a : B}
(h : G.IsHom e a)
:
(G.proj d) a = if e = d then a else 0
theorem
MultiplicativeBasisDeformations.LenGrading.isHom_mul
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{d e : ℕ}
{a b : B}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
:
G.IsHom (d + e) (a * b)
theorem
MultiplicativeBasisDeformations.LenGrading.isHom_zero_of_ge
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{d : ℕ}
{a : B}
(ha : G.IsHom d a)
(hd : G.N ≤ d)
:
a = 0
def
MultiplicativeBasisDeformations.LenGrading.Ge
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(m : ℕ)
(a : B)
:
Components only in degrees ≥ m.
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.ge_zero
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(a : B)
:
G.Ge 0 a
theorem
MultiplicativeBasisDeformations.LenGrading.ge_of_isHom
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{d : ℕ}
{a : B}
(ha : G.IsHom d a)
:
G.Ge d a
theorem
MultiplicativeBasisDeformations.LenGrading.ge_add
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{m : ℕ}
{a b : B}
(ha : G.Ge m a)
(hb : G.Ge m b)
:
G.Ge m (a + b)
theorem
MultiplicativeBasisDeformations.LenGrading.ge_smul
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{m : ℕ}
(c : k)
{a : B}
(ha : G.Ge m a)
:
G.Ge m (c • a)
theorem
MultiplicativeBasisDeformations.LenGrading.ge_mono
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{m m' : ℕ}
(h : m' ≤ m)
{a : B}
(ha : G.Ge m a)
:
G.Ge m' a
theorem
MultiplicativeBasisDeformations.LenGrading.mul_eq_sum
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(a b : B)
:
The decomposition of a product into homogeneous products.
theorem
MultiplicativeBasisDeformations.LenGrading.ge_mul
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{m n : ℕ}
{a b : B}
(ha : G.Ge m a)
(hb : G.Ge n b)
:
G.Ge (m + n) (a * b)
def
MultiplicativeBasisDeformations.LenGrading.scale
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(t : k)
:
B →ₗ[k] B
The scaling map σ_t: degree d is multiplied by t^d.
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.scale_apply
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(t : k)
(a : B)
:
theorem
MultiplicativeBasisDeformations.LenGrading.scale_isHom
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(t : k)
{d : ℕ}
{a : B}
(ha : G.IsHom d a)
:
(G.scale t) a = t ^ d • a
theorem
MultiplicativeBasisDeformations.LenGrading.scale_mul
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(t : k)
(a b : B)
:
The scaling maps are multiplicative.
theorem
MultiplicativeBasisDeformations.LenGrading.scale_scale
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{t s : k}
(a : B)
:
theorem
MultiplicativeBasisDeformations.LenGrading.scale_one
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
(a : B)
:
(G.scale 1) a = a
theorem
MultiplicativeBasisDeformations.LenGrading.scale_inv
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{t : k}
(ht : t ≠ 0)
(a : B)
:
theorem
MultiplicativeBasisDeformations.LenGrading.scale_injective
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
{t : k}
(ht : t ≠ 0)
:
Function.Injective ⇑(G.scale t)
Endpoint subbimodules are homogeneous #
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.scale_e
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(t : k)
(x : Fin F.m)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.scale_corner
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(t : k)
{x y : Fin F.m}
{a : B}
(ha : a ∈ F.corner x y)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_map_scale
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
{t : k}
(ht : t ≠ 0)
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
:
F.IsEndpointSubbimodule x y (Submodule.map (G.scale t) N)
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.scale_mem
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hA : IsRepresentationFinite k B)
{t : k}
(ht : t ≠ 0)
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
{n : B}
(hn : n ∈ N)
:
(G.scale t) n ∈ N
The scaling maps preserve every endpoint subbimodule (the chain has one member of each dimension).
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_mem
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
[Infinite k]
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
{n : B}
(hn : n ∈ N)
(d : ℕ)
:
(G.proj d) n ∈ N
Endpoint subbimodules are homogeneous (k infinite).
The radical lies in positive degrees #
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_hom_mul
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
{m : ℕ}
{e : B}
(he : G.IsHom m e)
(a : B)
(d : ℕ)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_mul_hom
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
{m : ℕ}
{e : B}
(he : G.IsHom m e)
(a : B)
(d : ℕ)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_corner
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
{x y : Fin F.m}
{a : B}
(ha : a ∈ F.corner x y)
(d : ℕ)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.nilpotent_of_ge
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
{n : B}
(hn : G.Ge 1 n)
:
n ^ G.N = 0
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.rad_ge
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
(x : Fin F.m)
{a : B}
(ha : a ∈ F.cornerRadical x)
:
G.Ge 1 a
The corner radicals lie in positive degrees.
Cyclic subbimodules and their radicals #
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_mul_corner
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y z : Fin F.m}
{a b : B}
(ha : a ∈ F.corner x y)
(hb : b ∈ F.corner y z)
:
a * b ∈ F.corner x z
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_endpointSpan_self
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{g : B}
(hg : g ∈ F.corner x y)
:
g ∈ F.endpointSpan x y g
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointSpan_eq
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{g : B}
(hg : g ∈ F.corner x y)
:
F.endpointSpan x y g = k ∙ g ⊔ F.endpointRadical x y g
U(g) = k g + R(g).
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_endpointSpan
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{g : B}
(hg : g ∈ F.corner x y)
:
F.IsEndpointSubbimodule x y (F.endpointSpan x y g)
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.isEndpoint_endpointRadical
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
{x y : Fin F.m}
{g : B}
(hg : g ∈ F.corner x y)
:
F.IsEndpointSubbimodule x y (F.endpointRadical x y g)
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.endpointRadical_ge
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
{x y : Fin F.m}
{g : B}
{d : ℕ}
(hgd : G.IsHom d g)
{r : B}
(hr : r ∈ F.endpointRadical x y g)
:
G.Ge (d + 1) r
R(g) lies in degrees above that of g.
Layers #
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_hom_mem
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
[Infinite k]
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
{n : B}
(hn : n ∈ N)
(hn0 : n ≠ 0)
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.layer
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
[Infinite k]
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
(hN0 : N ≠ ⊥)
:
∃ (g : B) (d : ℕ), G.IsHom d g ∧ g ≠ 0 ∧ g ∈ N ∧ N = F.endpointSpan x y g
A homogeneous generator of minimal degree generates: every nonzero
endpoint subbimodule is U(g) for a homogeneous g.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.lines
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
[Infinite k]
(hA : IsRepresentationFinite k B)
{x y : Fin F.m}
(n : ℕ)
(N : Submodule k B)
:
Module.finrank k ↥N = n → F.IsEndpointSubbimodule x y N → ∀ (d : ℕ), ∃ (w : B), ∀ u ∈ N, G.IsHom d u → u ∈ k ∙ w
One line in each degree: the homogeneous elements of a given degree of an endpoint subbimodule lie on a line (successive layers have strictly increasing degrees).
A homogeneous basis is adapted to every two-sided ideal #
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.proj_corner_basis
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
[Infinite k]
{ι : Type u_1}
(b : Module.Basis ι k B)
{x y : Fin F.m}
{d : ℕ}
(i : ι)
{x' y' : Fin F.m}
{d' : ℕ}
(hi : b i ∈ F.corner x' y')
(hid : G.IsHom d' (b i))
:
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.hom_mem_span
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
[Infinite k]
(hA : IsRepresentationFinite k B)
{ι : Type u_1}
(b : Module.Basis ι k B)
(hb : ∀ (i : ι), ∃ (x : Fin F.m) (y : Fin F.m) (d : ℕ), b i ∈ F.corner x y ∧ G.IsHom d (b i))
{x y : Fin F.m}
{N : Submodule k B}
(hN : F.IsEndpointSubbimodule x y N)
{d : ℕ}
{h : B}
(hhN : h ∈ N)
(hhd : G.IsHom d h)
:
h ∈ Submodule.span k (⇑b '' {i : ι | b i ∈ N})
Each homogeneous element of a corner lying in an endpoint subbimodule is in the span of the basis vectors it contains.
theorem
MultiplicativeBasisDeformations.PrimitiveIdempotents.span_basis_ideal
{k : Type u}
[Field k]
{B : Type v}
[Ring B]
[Algebra k B]
(G : LenGrading k B)
[IsAlgClosed k]
[FiniteDimensional k B]
(F : PrimitiveIdempotents B)
(he0 : ∀ (x : Fin F.m), G.IsHom 0 (F.e x))
(hcorner0 : ∀ (x : Fin F.m), ∀ a ∈ F.corner x x, G.IsHom 0 a → ∃ (c : k), a = c • F.e x)
[Infinite k]
(hA : IsRepresentationFinite k B)
{ι : Type u_1}
(b : Module.Basis ι k B)
(hb : ∀ (i : ι), ∃ (x : Fin F.m) (y : Fin F.m) (d : ℕ), b i ∈ F.corner x y ∧ G.IsHom d (b i))
(I : Submodule k B)
(hIl : ∀ (a z : B), z ∈ I → a * z ∈ I)
(hIr : ∀ (a z : B), z ∈ I → z * a ∈ I)
:
Submodule.span k (⇑b '' {i : ι | b i ∈ I}) = I
Corollary 3.3 for a homogeneous basis: its intersection with a two-sided ideal spans that ideal.