Incidence tables and faithful supports of ray tables

• inc Q: the incidence table of a finite poset; its linearization is the incidence algebra (incEquiv), so the forbidden configurations of FinPoset apply to it.
• Faithful projective support (def:faithful-support): the rays from x in a finite set T, ordered by r ≤ s if r v = s for a ray v. Its incidence table is a quotient of the graded cover on the objects (tgt r, wt r) (the action on H(X, -)), so it is representation-finite when kP is (Lemma 4.10).

Incidence tables

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.IP (Q : Type) [PartialOrder Q] : Type

Comparable pairs.

def MultiplicativeBasisDeformations.RaySys.inc (Q : Type) [PartialOrder Q] [DecidableEq Q] : Mult Q (IP Q)

The incidence table of a finite poset.

theorem MultiplicativeBasisDeformations.RaySys.inc_mul_of {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] {p p' : IP Q} (h : (↑p).2 = (↑p').1) : (inc Q).mul p p' = some ⟨((↑p).1, (↑p').2), ⋯⟩

def MultiplicativeBasisDeformations.RaySys.delta {Q : Type} [PartialOrder Q] [DecidableEq Q] (k : Type u) [Field k] (p : IP Q) : IncidenceAlgebra k Q

The indicator incidence function of a comparable pair.

theorem MultiplicativeBasisDeformations.RaySys.delta_apply {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] (p : IP Q) (a b : Q) : (delta k p) a b = if (a, b) = ↑p then 1 else 0

noncomputable def MultiplicativeBasisDeformations.RaySys.incLin {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] : ↥((inc Q).Lin k) →ₗ[k] IncidenceAlgebra k Q

The map from the linearization of the incidence table.

theorem MultiplicativeBasisDeformations.RaySys.incLin_b {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] (p : IP Q) : (incLin k) ((inc Q).b k p) = delta k p

theorem MultiplicativeBasisDeformations.RaySys.delta_mul {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] (p p' : IP Q) : delta k p * delta k p' = ((inc Q).mul p p').elim 0 (delta k)

def MultiplicativeBasisDeformations.RaySys.evalAt {Q : Type} [PartialOrder Q] (k : Type u) [Field k] (a b : Q) : IncidenceAlgebra k Q →+ k

Evaluation of incidence functions.

theorem MultiplicativeBasisDeformations.RaySys.sum_apply' {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] {ι : Type} (s : Finset ι) (f : ι → IncidenceAlgebra k Q) (a b : Q) : (∑ i ∈ s, f i) a b = ∑ i ∈ s, (f i) a b

theorem MultiplicativeBasisDeformations.RaySys.incLin_mul {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] (x y : ↥((inc Q).Lin k)) : (incLin k) (x * y) = (incLin k) x * (incLin k) y

theorem MultiplicativeBasisDeformations.RaySys.incLin_one {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] : (incLin k) 1 = 1

theorem MultiplicativeBasisDeformations.RaySys.incLin_injective {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] : Function.Injective ⇑(incLin k)

theorem MultiplicativeBasisDeformations.RaySys.incLin_surjective {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] : Function.Surjective ⇑(incLin k)

noncomputable def MultiplicativeBasisDeformations.RaySys.incEquiv {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] : ↥((inc Q).Lin k) ≃ₐ[k] IncidenceAlgebra k Q

The linearization of the incidence table is the incidence algebra.

theorem MultiplicativeBasisDeformations.RaySys.inc_forbidden {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (k : Type u) [Field k] [LocallyFiniteOrder Q] [IsAlgClosed k] {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (e : PosetRep.Pos n le ≃o Q) (d : Fin n → ℕ) (hu : PosetRep.UniqOK le) (hc : PosetRep.CountOK le d) : ¬IsRepresentationFinite k ↥((inc Q).Lin k)

Forbidden configurations for incidence tables (Lemma 8.8 with the table after it).

Faithful supports

def MultiplicativeBasisDeformations.RaySys.Tab.RF {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r s : R) : Prop

Right factorization: s = r v for a ray v.

def MultiplicativeBasisDeformations.RaySys.Tab.LF {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r s : R) : Prop

Left factorization: r = v s for a ray v.

theorem MultiplicativeBasisDeformations.RaySys.Tab.rf_refl {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (r : R) : P.RF r r

theorem MultiplicativeBasisDeformations.RaySys.Tab.lf_refl {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (r : R) : P.LF r r

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_assoc_some {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r v v' s t : R} (h1 : P.mul r v = some s) (h2 : P.mul s v' = some t) : ∃ (w : R), P.mul v v' = some w ∧ P.mul r w = some t

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_assoc_some' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {v' v s r t : R} (h1 : P.mul v s = some r) (h2 : P.mul v' r = some t) : ∃ (w : R), P.mul v' v = some w ∧ P.mul w s = some t

theorem MultiplicativeBasisDeformations.RaySys.Tab.rf_trans {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r s t : R} (h1 : P.RF r s) (h2 : P.RF s t) : P.RF r t

theorem MultiplicativeBasisDeformations.RaySys.Tab.lf_trans {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r s t : R} (h1 : P.LF r s) (h2 : P.LF s t) : P.LF r t

theorem MultiplicativeBasisDeformations.RaySys.Tab.eq_of_mul_wt_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r v s : R} (h : P.mul r v = some s) (hv : P.wt v = 0) : s = r

theorem MultiplicativeBasisDeformations.RaySys.Tab.eq_of_mul_wt_zero' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {v r s : R} (h : P.mul v r = some s) (hv : P.wt v = 0) : s = r

theorem MultiplicativeBasisDeformations.RaySys.Tab.wt_zero_of_sum {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {v v' : R} (h : P.wt v + P.wt v' = 0) : P.wt v = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.rf_antisymm {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r s : R} (h1 : P.RF r s) (h2 : P.RF s r) : r = s

theorem MultiplicativeBasisDeformations.RaySys.Tab.lf_antisymm {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r s : R} (h1 : P.LF r s) (h2 : P.LF s r) : r = s

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_assoc_some_inv {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {r w u h h' : R} (hw : P.mul h h' = some w) (hu : P.mul r w = some u) : ∃ (s' : R), P.mul r h = some s' ∧ P.mul s' h' = some u

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_assoc_some_inv' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {w s u h h' : R} (hw : P.mul h h' = some w) (hu : P.mul w s = some u) : ∃ (s' : R), P.mul h' s = some s' ∧ P.mul h s' = some u

def MultiplicativeBasisDeformations.RaySys.Tab.ProjSup {V R L : Type} [AddCommGroup L] (_P : Tab V R L) (T : Finset R) : Type

The faithful projective support on T (def:faithful-support): r ≤ s if s = r v.

def MultiplicativeBasisDeformations.RaySys.Tab.ProjSup.ray {V R L : Type} [AddCommGroup L] {P : Tab V R L} {T : Finset R} (a : P.ProjSup T) : R

The ray of a point of the support.

theorem MultiplicativeBasisDeformations.RaySys.Tab.ProjSup.ray_mem {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} (a : P.ProjSup T) : a.ray ∈ T

theorem MultiplicativeBasisDeformations.RaySys.Tab.ProjSup.ext {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} {a b : P.ProjSup T} (h : a.ray = b.ray) : a = b

def MultiplicativeBasisDeformations.RaySys.Tab.ProjSup.mk {V R L : Type} [AddCommGroup L] {P : Tab V R L} {T : Finset R} (r : R) (h : r ∈ T) : P.ProjSup T

The point of the support at a ray.

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.ProjSup.ray_mk {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} (r : R) (h : r ∈ T) : (mk r h).ray = r

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instPartialOrderProjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : PartialOrder (P.ProjSup T)

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instFintypeProjSup {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : Fintype (P.ProjSup T)

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableEqProjSup {V R L : Type} [AddCommGroup L] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableEq (P.ProjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableLEProjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableLE (P.ProjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableLTProjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableLT (P.ProjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instLocallyFiniteOrderProjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : LocallyFiniteOrder (P.ProjSup T)

theorem MultiplicativeBasisDeformations.RaySys.Tab.projSup_le_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b : P.ProjSup T) : a ≤ b ↔ ∃ (v : R), P.mul a.ray v = some b.ray

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.psv {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : P.ProjSup T → V

The labels of the projective support: (tgt r, wt r).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.psg {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : P.ProjSup T → L

The weights of the projective support.

def MultiplicativeBasisDeformations.RaySys.Tab.supPair {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b : P.ProjSup T) (v : R) (hm : P.mul a.ray v = some b.ray) : IP (P.ProjSup T)

A comparable pair of the support from a factorization.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.PCR {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : Type

The rays of the graded cover of the support.

def MultiplicativeBasisDeformations.RaySys.Tab.psf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.PCR T) : Option (IP (P.ProjSup T))

The action on H(X, -).

theorem MultiplicativeBasisDeformations.RaySys.Tab.psf_pos {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.PCR T) (hm : P.mul (↑↑t).1.ray (↑↑t).2.2 = some (↑↑t).2.1.ray) : P.psf T t = some (P.supPair T (↑↑t).1 (↑↑t).2.1 (↑↑t).2.2 hm)

theorem MultiplicativeBasisDeformations.RaySys.Tab.psf_neg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.PCR T) (hm : ¬P.mul (↑↑t).1.ray (↑↑t).2.2 = some (↑↑t).2.1.ray) : P.psf T t = none

theorem MultiplicativeBasisDeformations.RaySys.Tab.inc_supPair_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b c : P.ProjSup T) (v v' : R) (h1 : P.mul a.ray v = some b.ray) (h2 : P.mul b.ray v' = some c.ray) : (inc (P.ProjSup T)).mul (P.supPair T a b v h1) (P.supPair T b c v' h2) = some ⟨(a, c), ⋯⟩

def MultiplicativeBasisDeformations.RaySys.Tab.projSupMor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) {x : V} (hT : ∀ r ∈ T, P.src r = x) : Mor (P.cover (P.psv T) P.wt ⋯ (P.psg T)) (inc (P.ProjSup T))

The action on H(X, -) as a table morphism onto the incidence table.

theorem MultiplicativeBasisDeformations.RaySys.Tab.projSup_isRepresentationFinite {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) {x : V} (hT : ∀ r ∈ T, P.src r = x) (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((inc (P.ProjSup T)).Lin k)

Lemma 4.10 for a projective support: its incidence algebra is representation-finite when kP is.

def MultiplicativeBasisDeformations.RaySys.Tab.InjSup {V R L : Type} [AddCommGroup L] (_P : Tab V R L) (T : Finset R) : Type

The faithful injective support on T (def:faithful-support), in the opposite of the paper's order: r ≤ s if r = v s for a ray v.

def MultiplicativeBasisDeformations.RaySys.Tab.InjSup.ray {V R L : Type} [AddCommGroup L] {P : Tab V R L} {T : Finset R} (a : P.InjSup T) : R

The ray of a point of the injective support.

theorem MultiplicativeBasisDeformations.RaySys.Tab.InjSup.ray_mem {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} (a : P.InjSup T) : a.ray ∈ T

theorem MultiplicativeBasisDeformations.RaySys.Tab.InjSup.ext {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} {a b : P.InjSup T} (h : a.ray = b.ray) : a = b

def MultiplicativeBasisDeformations.RaySys.Tab.InjSup.mk {V R L : Type} [AddCommGroup L] {P : Tab V R L} {T : Finset R} (r : R) (h : r ∈ T) : P.InjSup T

The point of the injective support at a ray.

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Tab.InjSup.ray_mk {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {T : Finset R} (r : R) (h : r ∈ T) : (mk r h).ray = r

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instPartialOrderInjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : PartialOrder (P.InjSup T)

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instFintypeInjSup {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : Fintype (P.InjSup T)

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableEqInjSup {V R L : Type} [AddCommGroup L] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableEq (P.InjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableLEInjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableLE (P.InjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instDecidableLTInjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : DecidableLT (P.InjSup T)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.RaySys.Tab.instLocallyFiniteOrderInjSup {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) : LocallyFiniteOrder (P.InjSup T)

theorem MultiplicativeBasisDeformations.RaySys.Tab.injSup_le_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b : P.InjSup T) : a ≤ b ↔ ∃ (v : R), P.mul v b.ray = some a.ray

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.isv {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : P.InjSup T → V

The labels of the injective support: (src r, -wt r).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.isg {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : P.InjSup T → L

The weights of the injective support.

def MultiplicativeBasisDeformations.RaySys.Tab.isupPair {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b : P.InjSup T) (v : R) (hm : P.mul v b.ray = some a.ray) : IP (P.InjSup T)

A comparable pair of the injective support from a factorization.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.ICR {V R L : Type} [AddCommGroup L] (P : Tab V R L) (T : Finset R) : Type

The rays of the graded cover of the injective support.

def MultiplicativeBasisDeformations.RaySys.Tab.isf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.ICR T) : Option (IP (P.InjSup T))

The action on H(-, X).

theorem MultiplicativeBasisDeformations.RaySys.Tab.isf_pos {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.ICR T) (hm : P.mul (↑↑t).2.2 (↑↑t).2.1.ray = some (↑↑t).1.ray) : P.isf T t = some (P.isupPair T (↑↑t).1 (↑↑t).2.1 (↑↑t).2.2 hm)

theorem MultiplicativeBasisDeformations.RaySys.Tab.isf_neg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (t : P.ICR T) (hm : ¬P.mul (↑↑t).2.2 (↑↑t).2.1.ray = some (↑↑t).1.ray) : P.isf T t = none

theorem MultiplicativeBasisDeformations.RaySys.Tab.inc_isupPair_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) (a b c : P.InjSup T) (v v' : R) (h1 : P.mul v b.ray = some a.ray) (h2 : P.mul v' c.ray = some b.ray) : (inc (P.InjSup T)).mul (P.isupPair T a b v h1) (P.isupPair T b c v' h2) = some ⟨(a, c), ⋯⟩

def MultiplicativeBasisDeformations.RaySys.Tab.injSupMor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) {x : V} (hT : ∀ r ∈ T, P.tgt r = x) : Mor (P.cover (P.isv T) P.wt ⋯ (P.isg T)) (inc (P.InjSup T))

The action on H(-, X) as a table morphism onto the incidence table.

theorem MultiplicativeBasisDeformations.RaySys.Tab.injSup_isRepresentationFinite {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (T : Finset R) {x : V} (hT : ∀ r ∈ T, P.tgt r = x) (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((inc (P.InjSup T)).Lin k)

Lemma 4.10 for an injective support.