Homogeneous rays of a length-graded algebra

Proposition 3.8 (projective-rays.tex), for a length-graded representation-finite algebra with idempotents in degree zero and deg 0 corners k e_x (the case of A₀):

1. "each nonzero ray contains the nonzero vectors of a unique homogeneous line" (exists_hom_mem_ray, mem_span_of_ray_eq);
2. "For homogeneous f, g of degrees p, q, every element of M(f,g) has homogeneous components only in degrees greater than p+q. Thus fg ∈ M(f,g) exactly when fg = 0" (mul_mem_insertionSpan_iff);
3. "Associativity of A₀ now gives (3)" (rayProduct_assoc, for arbitrary representatives, through Lemma 3.6).

Then a homogeneous normed multiplicative basis containing the e_x is, after reindexing, a ray transversal killing zero ray products (hasRayBasis_of_graded): this is the "ray basis" of Corollary 5.5(2).

theorem MultiplicativeBasisDeformations.IsNormedMultiplicativeBasis.reindex {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {ι : Type u_1} {ι' : Type u_2} {b : Module.Basis ι k B} (hb : IsNormedMultiplicativeBasis b) (e : ι ≃ ι') : IsNormedMultiplicativeBasis (b.reindex e)

A normed multiplicative basis stays normed after reindexing.

def MultiplicativeBasisDeformations.PrimitiveIdempotents.HasRayBasis (k : Type u) [Field k] {B : Type v} [Ring B] [Algebra k B] (F : PrimitiveIdempotents B) : Prop

B has a ray basis for F: a normed multiplicative basis indexed by the nonzero rays, a ray transversal, with zero ray products giving zero products (Corollary 5.5(2), Theorem 11.7(2)(3)).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_ge {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 z : Fin F.m} {f h : B} {p q : ℕ} (hfp : G.IsHom p f) (hhq : G.IsHom q h) {w : B} (hw : w ∈ F.insertionSpan x y z f h) : G.Ge (p + q + 1) w

M(f, h) lies in degrees above p + q.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mul_mem_insertionSpan_iff {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 z : Fin F.m} {f h : B} {p q : ℕ} (hfp : G.IsHom p f) (hhq : G.IsHom q h) : f * h ∈ F.insertionSpan x y z f h ↔ f * h = 0

Proposition 3.8(2): for homogeneous f, h, fh ∈ M(f,h) iff fh = 0.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.hom_mem_endpointSpan {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 g' : B} (hg : g ∈ F.corner x y) {d d' : ℕ} (hgd : G.IsHom d g) (hg'd : G.IsHom d' g') (hg'0 : g' ≠ 0) (hg' : g' ∈ F.endpointSpan x y g) : d ≤ d' ∧ (d' = d → g' ∈ k ∙ g)

A homogeneous element of U(g) has degree at least that of g, and the same degree only on the line of g.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.mem_span_of_ray_eq {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 g' : B} (hg : g ∈ F.corner x y) (hg' : g' ∈ F.corner x y) (hg'0 : g' ≠ 0) {d d' : ℕ} (hgd : G.IsHom d g) (hg'd : G.IsHom d' g') (h : F.ray x y g' = F.ray x y g) : g' ∈ k ∙ g

Proposition 3.8(1), uniqueness: homogeneous elements of one ray lie on one line.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_hom_mem_ray {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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} {f : B} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) : ∃ (g : B) (d : ℕ), G.IsHom d g ∧ g ≠ 0 ∧ g ∈ F.ray x y f

Proposition 3.8(1), existence: every nonzero ray contains a homogeneous element.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.notMem_insertionSpan_iff {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 z : Fin F.m} {f h f₀ h₀ : B} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hh : h ∈ F.corner y z) (hh0 : h ≠ 0) (hf₀ : f₀ ∈ F.ray x y f) (hh₀ : h₀ ∈ F.ray y z h) {p q : ℕ} (hfp : G.IsHom p f₀) (hhq : G.IsHom q h₀) : (f * h ∉ F.insertionSpan x y z f h ↔ f₀ * h₀ ≠ 0) ∧ (f * h ∉ F.insertionSpan x y z f h → f₀ * h₀ ∈ F.ray x z (f * h))

With homogeneous representatives, fh ∉ M(f,h) iff f₀h₀ ≠ 0, and then f₀h₀ ∈ [fh].

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayProduct_assoc {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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 z w : Fin F.m} {f g h : B} (hf : f ∈ F.corner x y) (hf0 : f ≠ 0) (hg : g ∈ F.corner y z) (hg0 : g ≠ 0) (hh : h ∈ F.corner z w) (hh0 : h ≠ 0) : f * g ∉ F.insertionSpan x y z f g ∧ f * g * h ∉ F.insertionSpan x z w (f * g) h ↔ g * h ∉ F.insertionSpan y z w g h ∧ f * (g * h) ∉ F.insertionSpan x y w f (g * h)

Proposition 3.8(3): the ray table is associative. For nonzero representatives, ([f][g])[h] ≠ 0 iff [f]([g][h]) ≠ 0 (and then both are the ray of fgh).

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isCornerUnit_smul_e {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (F : PrimitiveIdempotents B) [Infinite k] (x : Fin F.m) {c : k} (hc : c ≠ 0) : F.IsCornerUnit x (c • F.e x)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.isHom_unique {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading k B) [Infinite k] {d d' : ℕ} {a : B} (ha0 : a ≠ 0) (h : G.IsHom d a) (h' : G.IsHom d' a) : d = d'

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.exists_basis_line {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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} {d : ℕ} {g : B} (hg : g ∈ F.corner x y) (hgd : G.IsHom d g) (hg0 : g ≠ 0) : ∃ (i : ι) (c : k), c ≠ 0 ∧ g = c • b i ∧ b i ∈ F.corner x y

A homogeneous nonzero element of a corner is a nonzero multiple of a basis vector of that corner.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.hasRayBasis_of_graded {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] (G : LenGrading 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)) (hnorm : IsNormedMultiplicativeBasis b) (hid : ∀ (x : Fin F.m), ∃ (i : ι), b i = F.e x) : HasRayBasis k F

The ray basis of a length-graded algebra: a homogeneous normed multiplicative basis containing the e_x is a ray transversal killing zero ray products (Proposition 3.8, Corollary 3.3).