Ray presentations

A ray presentation of an algebra B (with primitive idempotents F) by a ray table T is a family of vectors β r, one in each nonzero ray, such that the ray products of B (Definition 3.4: [f][h] = [fh] unless fh ∈ M(f, h)) are the products of T. This is the content of "ray A_t = P with the specified representatives" (Proposition 11.3(3), binary-families.tex) and of Definition 3.9(3).

The transported rays of a fibre of the zero-product family present B by P (fibre_rayPres): "If n ∈ rad R_y, the product rn is a combination of proper rays, so (rn)·s = (rn)s … Each correction r*s = rq_ys belongs to this subspace." With zero coefficients this shows that a representation-finite ray table presents its own linearization.

def MultiplicativeBasisDeformations.RaySys.Mult.Lift2 {V R : Type} (T : Mult V R) : Prop

The weight-lifting property of a ray table: additive weights modulo two lift to integer additive weights (the form in which freeness of W(Q) is used, hW of Theorem 9.1).

def MultiplicativeBasisDeformations.RaySys.Mult.Conn {V R : Type} (T : Mult V R) : Prop

A connected table: every two vertices are joined by a zigzag of rays.

structure MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] (F : PrimitiveIdempotents B) {V R : Type} (T : RaySys.Mult V R) (ι : V ≃ Fin F.m) (β : R → B) : Prop

A ray presentation of B by the table T.

• corner (r : R) : β r ∈ F.corner (ι (T.src r)) (ι (T.tgt r))
• ne (r : R) : β r ≠ 0
• inj (r s : R) : β r ∈ F.ray (ι (T.src s)) (ι (T.tgt s)) (β s) → r = s
• surj (x y : Fin F.m) (f : B) : f ∈ F.corner x y → f ≠ 0 → ∃ (r : R), ι (T.src r) = x ∧ ι (T.tgt r) = y ∧ f ∈ F.ray x y (β r)
• mul_some (r s t : R) : T.mul r s = some t → β r * β s ∉ F.insertionSpan (ι (T.src r)) (ι (T.tgt r)) (ι (T.tgt s)) (β r) (β s) ∧ β r * β s ∈ F.ray (ι (T.src t)) (ι (T.tgt t)) (β t)
• mul_none (r s : R) : T.mul r s = none → T.tgt r = T.src s → β r * β s ∈ F.insertionSpan (ι (T.src r)) (ι (T.tgt r)) (ι (T.tgt s)) (β r) (β s)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.exists_match {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') (r : R) : ∃ (r' : R'), ι' (T'.src r') = ι (T.src r) ∧ ι' (T'.tgt r') = ι (T.tgt r) ∧ β r ∈ F.ray (ι (T.src r)) (ι (T.tgt r)) (β' r')

The ray of β r among the rays of the second presentation.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_symm {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {x y : Fin F.m} {f g : B} (hf : f ∈ F.corner x y) (hg : g ∈ F.ray x y f) : f ∈ F.ray x y g

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_trans {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {x y : Fin F.m} {f g h : B} (hg : g ∈ F.corner x y) (h1 : f ∈ F.ray x y g) (h2 : g ∈ F.ray x y h) (hh : h ∈ F.corner x y) : f ∈ F.ray x y h

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.mul_iff {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (hB : IsRepresentationFinite k B) (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') {r s t : R} {r' s' t' : R'} (hr : ι' (T'.src r') = ι (T.src r) ∧ ι' (T'.tgt r') = ι (T.tgt r) ∧ β r ∈ F.ray (ι (T.src r)) (ι (T.tgt r)) (β' r')) (hs : ι' (T'.src s') = ι (T.src s) ∧ ι' (T'.tgt s') = ι (T.tgt s) ∧ β s ∈ F.ray (ι (T.src s)) (ι (T.tgt s)) (β' s')) (ht : ι' (T'.src t') = ι (T.src t) ∧ ι' (T'.tgt t') = ι (T.tgt t) ∧ β t ∈ F.ray (ι (T.src t)) (ι (T.tgt t)) (β' t')) (hrst : T.mul r s = some t) : T'.mul r' s' = some t'

Two ray presentations of the same algebra have isomorphic tables (Lemma 3.6).

noncomputable def MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.matchFn {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') : R → R'

The matching ray of the second presentation, as a function.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.matchFn_spec {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') (r : R) : ι' (T'.src (h.matchFn h' r)) = ι (T.src r) ∧ ι' (T'.tgt (h.matchFn h' r)) = ι (T.tgt r) ∧ β r ∈ F.ray (ι (T.src r)) (ι (T.tgt r)) (β' (h.matchFn h' r))

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.matchFn_left_inv {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') (r : R) : h'.matchFn h (h.matchFn h' r) = r

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.lift2 {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (hB : IsRepresentationFinite k B) (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') (hL : T'.Lift2) : T.Lift2

Weight lifting transfers along ray presentations of one algebra.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.map {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R : Type} {T : RaySys.Mult V R} {ι : V ≃ Fin F.m} {β : R → B} {B' : Type u} [Ring B'] [Algebra k B'] [FiniteDimensional k B'] (ψ : B ≃ₐ[k] B') (F' : PrimitiveIdempotents B') (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (h : F.IsRayPres T ι β) : F'.IsRayPres T (ι.trans σ) (⇑ψ ∘ β)

Ray presentations transport along algebra isomorphisms.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.IsRayPres.conn {k : Type u} [Field k] {B : Type u} [Ring B] [Algebra k B] [IsAlgClosed k] [FiniteDimensional k B] {F : PrimitiveIdempotents B} {V R V' R' : Type} {T : RaySys.Mult V R} {T' : RaySys.Mult V' R'} {ι : V ≃ Fin F.m} {ι' : V' ≃ Fin F.m} {β : R → B} {β' : R' → B} (h : F.IsRayPres T ι β) (h' : F.IsRayPres T' ι' β') (hc : T.Conn) : T'.Conn

Connectivity transfers along ray presentations of one algebra.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_below {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {r : R} {x : ↥(S.P.Lin k)} (hx : x ∈ S.USp k r ⊓ S.P.degSp k (S.P.deg (S.P.wt r) + 1)) (s : R) : ((S.coch k c) x) (S.P.b k s) = 0

Corrections vanish below a ray: on elements of U(r) of degree above r.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_cornerRadical_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (y : V) {z : B} : z ∈ (S.fibreIdem k hfin c Ψ hΨ).cornerRadical ((S.fibreIdx k hfin c Ψ hΨ) y) ↔ Ψ.symm z ∈ S.P.corSp k y y ⊓ S.P.degSp k 1

The corner radical of the fibre is the span of the positive local rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.e_mem_corSp' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (k : Type u) [Field k] [IsAlgClosed k] (P : Tab V R L) {x : V} : P.b k (P.e x) ∈ P.corSp k x x

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_prod5 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {r s : R} (hm : S.P.tgt r = S.P.src s) {a' n' w' : ↥(S.P.Lin k)} (ha : a' ∈ S.P.corSp k (S.P.src r) (S.P.src r)) (hn : n' ∈ S.P.corSp k (S.P.tgt r) (S.P.tgt r) ⊓ S.P.degSp k 1) (hw : w' ∈ S.P.corSp k (S.P.tgt s) (S.P.tgt s)) : Ψ a' * S.βv k Ψ r * Ψ n' * S.βv k Ψ s * Ψ w' = Ψ (a' * S.P.b k r * n' * S.P.b k s * w')

Products through a positive local element are computed in kP.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_insertionSpan_le {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {r s : R} (hm : S.P.tgt r = S.P.src s) : (S.fibreIdem k hfin c Ψ hΨ).insertionSpan ((S.fibreIdx k hfin c Ψ hΨ) (S.P.src r)) ((S.fibreIdx k hfin c Ψ hΨ) (S.P.tgt r)) ((S.fibreIdx k hfin c Ψ hΨ) (S.P.tgt s)) (S.βv k Ψ r) (S.βv k Ψ s) ≤ Submodule.map (↑Ψ) (S.P.degSp k (S.P.deg (S.P.wt r) + S.P.deg (S.P.wt s) + 1))

M(β r, β s) lies in degrees above deg r + deg s.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_rayPres {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : (S.fibreIdem k hfin c Ψ hΨ).IsRayPres S.P.toMult (S.fibreIdx k hfin c Ψ hΨ) (S.βv k Ψ)

The transported rays present the fibre by the ray table P (Proposition 11.3(3)).