Poset configurations in a ray table (Lemmas 8.9 and C.1)

A configuration of a finite poset Q in a ray table: objects (v a, g a) of the graded covering category, and rays ρ a b for a ≤ b of weight g b - g a, composing as the poset. The retraction conditions say that a selected ray never factors as a selected arrow times a non-selected morphism (on either side); they are required only for cover relations of Q (the arrows of its Hasse diagram, lem:representation-transfer, lem:tree-quotient). Then the incidence algebra of Q is representation-finite when kP is.

structure MultiplicativeBasisDeformations.RaySys.Tab.Conf {V R L : Type} [AddCommGroup L] (P : Tab V R L) (Q : Type) [PartialOrder Q] : Type

A configuration of a finite poset in the graded covering category.

• v : Q → V
• g : Q → L
• ρ (a b : Q) : a ≤ b → R
• src_ρ (a b : Q) (h : a ≤ b) : P.src (self.ρ a b h) = self.v a
• tgt_ρ (a b : Q) (h : a ≤ b) : P.tgt (self.ρ a b h) = self.v b
• wt_ρ (a b : Q) (h : a ≤ b) : P.wt (self.ρ a b h) = self.g b - self.g a
• mul_ρ (a b c : Q) (h1 : a ≤ b) (h2 : b ≤ c) : P.mul (self.ρ a b h1) (self.ρ b c h2) = some (self.ρ a c ⋯)
• retL (a b c : Q) (hab : a ⋖ b) (hac : a ≤ c) (h : R) : P.src h = self.v b → P.tgt h = self.v c → P.wt h = self.g c - self.g b → P.mul (self.ρ a b ⋯) h = some (self.ρ a c hac) → b ≤ c
• retR (a b c : Q) (hab : a ⋖ b) (hcb : c ≤ b) (h : R) : P.src h = self.v c → P.tgt h = self.v a → P.wt h = self.g a - self.g c → P.mul h (self.ρ a b ⋯) = some (self.ρ c b hcb) → c ≤ a

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.ρ_eq_of {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) {a b : Q} (hab : a ≤ b) (h : R) (h1 : P.src h = C.v a) (h2 : P.tgt h = C.v b) (h3 : P.wt h = C.g b - C.g a) : h = C.ρ a b hab

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.ρ_self {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) (a : Q) : C.ρ a a ⋯ = P.e (C.v a)

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.retL_all {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] (a b c : Q) (hab : a ≤ b) (hac : a ≤ c) (h : R) (h1 : P.src h = C.v b) (h2 : P.tgt h = C.v c) (h3 : P.wt h = C.g c - C.g b) (hm : P.mul (C.ρ a b hab) h = some (C.ρ a c hac)) : b ≤ c

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.retR_all {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] (a b c : Q) (hab : a ≤ b) (hcb : c ≤ b) (h : R) (h1 : P.src h = C.v c) (h2 : P.tgt h = C.v a) (h3 : P.wt h = C.g a - C.g c) (hm : P.mul h (C.ρ a b hab) = some (C.ρ c b hcb)) : c ≤ a

def MultiplicativeBasisDeformations.RaySys.Tab.Conf.emb {V R L : Type} [AddCommGroup L] {P : Tab V R L} {Q : Type} [PartialOrder Q] (C : P.Conf Q) (p : IP Q) : P.CR C.v P.wt C.g

The embedded ray of a comparable pair.

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.emb_injective {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] : Function.Injective C.emb

def MultiplicativeBasisDeformations.RaySys.Tab.Conf.mor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) : Mor (inc Q) (P.cover C.v P.wt ⋯ C.g)

The selected rays embed the incidence table into the graded cover.

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.hL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] (s : IP Q) (t : P.CR C.v P.wt C.g) (t' : IP Q) (hm : (P.cover C.v P.wt ⋯ C.g).mul (C.emb s) t = some (C.emb t')) : ∃ (s' : IP Q), C.emb s' = t

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.hR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] (s : IP Q) (t : P.CR C.v P.wt C.g) (t' : IP Q) (hm : (P.cover C.v P.wt ⋯ C.g).mul t (C.emb s) = some (C.emb t')) : ∃ (s' : IP Q), C.emb s' = t

theorem MultiplicativeBasisDeformations.RaySys.Tab.Conf.isRepresentationFinite {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [DecidableLE Q] (C : P.Conf Q) [LocallyFiniteOrder Q] (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((inc Q).Lin k)

A configuration makes the incidence algebra of the poset representation-finite (Lemmas 8.9 and C.1).