Corners, repeated labels and graded covers of ray tables (Lemma 4.7 for kP)

• restrict P W: the full subtable on a set W of vertices; its linearization is the idempotent corner of kP at ∑_{x ∈ W} e_x (restrictEquiv), so it is representation-finite with kP (Lemma 3.1(1)).
• infl P v: repeated labels v : κ → V; representation-finite with kP by Morita equivalence through a full idempotent (as in Lemma 4.7, first step).
• cover P γ v g: the full subcategory of the graded covering category on the objects (v i, g i), for a grading γ of the rays; representation-finite with kP by the split transfer of Lemma 4.6 (lem:homogeneous-projection).

Restriction to a set of vertices

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Mult.RV {V : Type} (W : Finset V) : Type

Vertices in W.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Mult.RR {V R : Type} (P : Mult V R) (W : Finset V) : Type

Rays with both endpoints in W.

def MultiplicativeBasisDeformations.RaySys.Mult.mulW {V R : Type} (P : Mult V R) (W : Finset V) (r s : P.RR W) : Option (P.RR W)

The product of rays with endpoints in W.

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulW_val {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (W : Finset V) (r s : P.RR W) : Option.map Subtype.val (P.mulW W r s) = P.mul ↑r ↑s

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulW_eq_some {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (W : Finset V) {r s t : P.RR W} (h : P.mulW W r s = some t) : P.mul ↑r ↑s = some ↑t

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulW_eq_some_iff {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (W : Finset V) {r s t : P.RR W} : P.mulW W r s = some t ↔ P.mul ↑r ↑s = some ↑t

def MultiplicativeBasisDeformations.RaySys.Mult.restrict {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (W : Finset V) : Mult (RV W) (P.RR W)

The full subtable on W.

def MultiplicativeBasisDeformations.RaySys.Mult.eW {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : ↥(P.Lin k)

The idempotent ∑_{x ∈ W} e_x.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.inclW {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : ↥((P.restrict W).Lin k) →ₗ[k] ↥(P.Lin k)

The inclusion of the full subtable.

theorem MultiplicativeBasisDeformations.RaySys.Mult.inclW_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (r : P.RR W) : (P.inclW k W) ((P.restrict W).b k r) = P.b k ↑r

theorem MultiplicativeBasisDeformations.RaySys.Mult.restrict_b_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (r s : P.RR W) : (P.restrict W).b k r * (P.restrict W).b k s = (P.mulW W r s).elim 0 ((P.restrict W).b k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.inclW_mul {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (x y : ↥((P.restrict W).Lin k)) : (P.inclW k W) (x * y) = (P.inclW k W) x * (P.inclW k W) y

theorem MultiplicativeBasisDeformations.RaySys.Mult.inclW_one {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : (P.inclW k W) 1 = P.eW k W

theorem MultiplicativeBasisDeformations.RaySys.Mult.isIdempotentElem_eW {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : IsIdempotentElem (P.eW k W)

theorem MultiplicativeBasisDeformations.RaySys.Mult.eW_mul_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (r : R) : P.eW k W * P.b k r = if P.src r ∈ W then P.b k r else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.b_mul_eW {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (r : R) : P.b k r * P.eW k W = if P.tgt r ∈ W then P.b k r else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.inclW_injective {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : Function.Injective ⇑(P.inclW k W)

theorem MultiplicativeBasisDeformations.RaySys.Mult.mem_range_inclW {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (y : ↥(P.Lin k)) (hy : P.eW k W * y * P.eW k W = y) : ∃ (x : ↥((P.restrict W).Lin k)), (P.inclW k W) x = y

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.restrictEquiv {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) : ↥((P.restrict W).Lin k) ≃ₐ[k] ⋯.Corner

The full subtable is the idempotent corner.

theorem MultiplicativeBasisDeformations.RaySys.Mult.restrict_isRepresentationFinite {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] (W : Finset V) (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((P.restrict W).Lin k)

Representation-finiteness passes to full subtables (Lemma 3.1(1)).

Repeated labels

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Mult.IR {V R : Type} (P : Mult V R) {κ : Type} (v : κ → V) : Type

Rays between labelled objects.

def MultiplicativeBasisDeformations.RaySys.Mult.mulI {V R : Type} (P : Mult V R) {κ : Type} [DecidableEq κ] (v : κ → V) (t t' : P.IR v) : Option (P.IR v)

The product of labelled rays.

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulI_val {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (t t' : P.IR v) : Option.map Subtype.val (P.mulI v t t') = if (↑t).2.1 = (↑t').1 then Option.map (fun (m : R) => ((↑t).1, (↑t').2.1, m)) (P.mul (↑t).2.2 (↑t').2.2) else none

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulI_eq_some {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {t t' t'' : P.IR v} (h : P.mulI v t t' = some t'') : (↑t).2.1 = (↑t').1 ∧ P.mul (↑t).2.2 (↑t').2.2 = some (↑t'').2.2 ∧ (↑t'').1 = (↑t).1 ∧ (↑t'').2.1 = (↑t').2.1

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulI_eq_some_iff {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {t t' t'' : P.IR v} : P.mulI v t t' = some t'' ↔ (↑t).2.1 = (↑t').1 ∧ P.mul (↑t).2.2 (↑t').2.2 = some (↑t'').2.2 ∧ (↑t'').1 = (↑t).1 ∧ (↑t'').2.1 = (↑t').2.1

def MultiplicativeBasisDeformations.RaySys.Mult.infl {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) : Mult κ (P.IR v)

Repeated labels.

theorem MultiplicativeBasisDeformations.RaySys.Mult.infl_mul_val {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (t t' : P.IR v) : Option.map Subtype.val ((P.infl v).mul t t') = if (↑t).2.1 = (↑t').1 then Option.map (fun (m : R) => ((↑t).1, (↑t').2.1, m)) (P.mul (↑t).2.2 (↑t').2.2) else none

def MultiplicativeBasisDeformations.RaySys.Mult.lr {V R : Type} (P : Mult V R) {κ : Type} (v : κ → V) (i j : κ) (r : R) (h1 : P.src r = v i) (h2 : P.tgt r = v j) : P.IR v

A labelled ray.

theorem MultiplicativeBasisDeformations.RaySys.Mult.infl_b_mul_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (i j l : κ) (r s : R) (h1 : P.src r = v i) (h2 : P.tgt r = v j) (h3 : P.src s = v j) (h4 : P.tgt s = v l) (t : R) (ht : P.mul r s = some t) : (P.infl v).b k (P.lr v i j r h1 h2) * (P.infl v).b k (P.lr v j l s h3 h4) = (P.infl v).b k (P.lr v i l t ⋯ ⋯)

def MultiplicativeBasisDeformations.RaySys.Mult.Wv {V : Type} [DecidableEq V] {κ : Type} [Fintype κ] (v : κ → V) : Finset V

Vertices hit by the labels.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.sec {V : Type} [DecidableEq V] {κ : Type} [Fintype κ] (v : κ → V) (x : RV (Wv v)) : κ

A chosen label of a hit vertex.

theorem MultiplicativeBasisDeformations.RaySys.Mult.v_sec {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (x : RV (Wv v)) : v (sec v x) = ↑x

theorem MultiplicativeBasisDeformations.RaySys.Mult.mem_Wv {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (i : κ) : v i ∈ Wv v

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.Wk {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) : Finset κ

The chosen labels.

theorem MultiplicativeBasisDeformations.RaySys.Mult.sec_mem {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (x : RV (Wv v)) : sec v x ∈ Wk v

theorem MultiplicativeBasisDeformations.RaySys.Mult.sec_v_of_mem {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {i : κ} (h : i ∈ Wk v) : sec v ⟨v i, ⋯⟩ = i

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.secRay {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (r : P.RR (Wv v)) : (P.infl v).RR (Wk v)

The ray map from the full subtable on the hit vertices.

theorem MultiplicativeBasisDeformations.RaySys.Mult.secRay_val {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (r : P.RR (Wv v)) : ↑↑(P.secRay v r) = (sec v ⟨P.src ↑r, ⋯⟩, sec v ⟨P.tgt ↑r, ⋯⟩, ↑r)

theorem MultiplicativeBasisDeformations.RaySys.Mult.sec_injective {V : Type} [Fintype V] [DecidableEq V] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) : Function.Injective (sec v)

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.secMor {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) : Mor (P.restrict (Wv v)) ((P.infl v).restrict (Wk v))

The full subtable on the hit vertices maps onto the chosen labels.

theorem MultiplicativeBasisDeformations.RaySys.Mult.secMor_surjective {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (t : (P.infl v).RR (Wk v)) : ∃ (r : P.RR (Wv v)), (P.secMor v).f r = some t

theorem MultiplicativeBasisDeformations.RaySys.Mult.infl_full {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (a : ↥((P.infl v).Lin k)) : a ∈ Submodule.span k {x : ↥((P.infl v).Lin k) | ∃ (p : ↥((P.infl v).Lin k)) (q : ↥((P.infl v).Lin k)), x = p * (P.infl v).eW k (Wk v) * q}

theorem MultiplicativeBasisDeformations.RaySys.Mult.infl_isRepresentationFinite {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((P.infl v).Lin k)

Repeated labels preserve representation-finiteness.

Graded covers

theorem MultiplicativeBasisDeformations.RaySys.Mult.γ_e {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (x : V) : γ (P.e x) = 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Mult.CR {V R : Type} (P : Mult V R) {κ : Type} (v : κ → V) {G : Type} [AddCommGroup G] (γ : R → G) (g : κ → G) : Type

Rays of the graded cover: labelled rays of degree g j - g i.

theorem MultiplicativeBasisDeformations.RaySys.Mult.graded_of_mulI {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) {t t' t'' : P.IR v} (h : P.mulI v t t' = some t'') (ht : γ (↑t).2.2 = g (↑t).2.1 - g (↑t).1) (ht' : γ (↑t').2.2 = g (↑t').2.1 - g (↑t').1) : γ (↑t'').2.2 = g (↑t'').2.1 - g (↑t'').1

def MultiplicativeBasisDeformations.RaySys.Mult.mulC {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (t t' : P.CR v γ g) : Option (P.CR v γ g)

The product of the graded cover.

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulC_val {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (t t' : P.CR v γ g) : Option.map Subtype.val (P.mulC v γ hγ g t t') = P.mulI v ↑t ↑t'

theorem MultiplicativeBasisDeformations.RaySys.Mult.mulC_eq_some_iff {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) {t t' t'' : P.CR v γ g} : P.mulC v γ hγ g t t' = some t'' ↔ P.mulI v ↑t ↑t' = some ↑t''

def MultiplicativeBasisDeformations.RaySys.Mult.cover {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) : Mult κ (P.CR v γ g)

The graded cover on the objects (v i, g i).

def MultiplicativeBasisDeformations.RaySys.Mult.coverMor {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) : Mor (P.cover v γ hγ g) (P.infl v)

The inclusion of the graded cover into the repeated labels.

noncomputable def MultiplicativeBasisDeformations.RaySys.Mult.coverProj {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) : ↥((P.infl v).Lin k) →ₗ[k] ↥((P.cover v γ hγ g).Lin k)

The projection onto the graded rays.

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverProj_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (t : P.IR v) : (P.coverProj k v γ hγ g) ((P.infl v).b k t) = if h : γ (↑t).2.2 = g (↑t).2.1 - g (↑t).1 then (P.cover v γ hγ g).b k ⟨t, h⟩ else 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverMor_alg_b {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (t : P.CR v γ g) : ((P.coverMor v γ hγ g).alg k) ((P.cover v γ hγ g).b k t) = (P.infl v).b k ↑t

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverProj_alg {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (x : ↥((P.cover v γ hγ g).Lin k)) : (P.coverProj k v γ hγ g) (((P.coverMor v γ hγ g).alg k) x) = x

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverProj_left {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (d : ↥((P.cover v γ hγ g).Lin k)) (x : ↥((P.infl v).Lin k)) : (P.coverProj k v γ hγ g) (((P.coverMor v γ hγ g).alg k) d * x) = d * (P.coverProj k v γ hγ g) x

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverProj_right {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (x : ↥((P.infl v).Lin k)) (d : ↥((P.cover v γ hγ g).Lin k)) : (P.coverProj k v γ hγ g) (x * ((P.coverMor v γ hγ g).alg k) d) = (P.coverProj k v γ hγ g) x * d

theorem MultiplicativeBasisDeformations.RaySys.Mult.coverMor_injective {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) : Function.Injective ⇑((P.coverMor v γ hγ g).alg k)

theorem MultiplicativeBasisDeformations.RaySys.Mult.cover_isRepresentationFinite {V R : Type} [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Mult V R) (k : Type u) [Field k] {κ : Type} [Fintype κ] [DecidableEq κ] (v : κ → V) {G : Type} [AddCommGroup G] [DecidableEq G] (γ : R → G) (hγ : ∀ (r s t : R), P.mul r s = some t → γ t = γ r + γ s) (g : κ → G) (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((P.cover v γ hγ g).Lin k)

Lemma 4.7 for ray tables (lem:homogeneous-projection): every graded cover of a representation-finite table is representation-finite.