Tree configurations from arrows

A configuration (Tab.Conf) of a finite poset whose cover paths are unique is determined by rays on the cover arrows, provided every path product is nonzero: ρ a b is the product along the unique path (Conf.ofArrows). This is how the paper presents its trees ("every path survives").

@[irreducible]

def MultiplicativeBasisDeformations.RaySys.Tab.pprod {V R L : Type} [AddCommGroup L] (P : Tab V R L) {Q : Type} [PartialOrder Q] (v : Q → V) (α : (a b : Q) → a ⋖ b → R) {a b : Q} : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b → M P.toMult

The product of the arrows along a path.

theorem MultiplicativeBasisDeformations.RaySys.Tab.pprod_nil {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] [LocallyFiniteOrder Q] (v : Q → V) (α : (a b : Q) → a ⋖ b → R) (a : Q) : P.pprod v α (PosetRep.EPath.nil a) = P.rr (P.e (v a))

theorem MultiplicativeBasisDeformations.RaySys.Tab.pprod_cons {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] [LocallyFiniteOrder Q] (v : Q → V) (α : (a b : Q) → a ⋖ b → R) {a b c : Q} (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) (h : b ⋖ c) : P.pprod v α (p.cons h) = P.pprod v α p * P.rr (α b c h)

theorem MultiplicativeBasisDeformations.RaySys.Tab.pprod_cases {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) {a b : Q} (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) : P.pprod v α p = 0 ∨ ∃ (r : R), P.pprod v α p = P.rr r ∧ P.src r = v a ∧ P.tgt r = v b

The product along a path is zero or a ray from v a to v b.

theorem MultiplicativeBasisDeformations.RaySys.Tab.e_mul_pprod {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) {a b : Q} (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) : P.rr (P.e (v a)) * P.pprod v α p = P.pprod v α p

theorem MultiplicativeBasisDeformations.RaySys.Tab.pprod_comp {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) {a b : Q} (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) {c : Q} (q : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) b c) : P.pprod v α (p.comp q) = P.pprod v α p * P.pprod v α q

theorem MultiplicativeBasisDeformations.RaySys.Tab.pprod_wt {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) {g : Q → L} (hwt : ∀ (a b : Q) (h : a ⋖ b), P.wt (α a b h) = g b - g a) {a b : Q} (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) (r : R) : P.pprod v α p = P.rr r → P.wt r = g b - g a

theorem MultiplicativeBasisDeformations.RaySys.Tab.exists_ρ {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) (hpath : ∀ (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b), P.pprod v α p ≠ 0) (a b : Q) (h : a ≤ b) : ∃ (r : R), P.pprod v α (Classical.choice ⋯) = P.rr r ∧ P.src r = v a ∧ P.tgt r = v b

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.ρA {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) (hpath : ∀ (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b), P.pprod v α p ≠ 0) (a b : Q) (h : a ≤ b) : R

The ray of a comparable pair: the product along its path.

theorem MultiplicativeBasisDeformations.RaySys.Tab.ρA_spec {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) (hpath : ∀ (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b), P.pprod v α p ≠ 0) (a b : Q) (h : a ≤ b) : P.pprod v α (Classical.choice ⋯) = P.rr (P.ρA hsrc htgt hpath a b h) ∧ P.src (P.ρA hsrc htgt hpath a b h) = v a ∧ P.tgt (P.ρA hsrc htgt hpath a b h) = v b

theorem MultiplicativeBasisDeformations.RaySys.Tab.ρA_path {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) (hpath : ∀ (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b), P.pprod v α p ≠ 0) (huniq : ∀ (a b : Q), Subsingleton (PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b)) (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b) : P.pprod v α p = P.rr (P.ρA hsrc htgt hpath a b ⋯)

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.Conf.ofArrows {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] [LocallyFiniteOrder Q] {v : Q → V} {α : (a b : Q) → a ⋖ b → R} (hsrc : ∀ (a b : Q) (h : a ⋖ b), P.src (α a b h) = v a) (htgt : ∀ (a b : Q) (h : a ⋖ b), P.tgt (α a b h) = v b) {g : Q → L} (hwt : ∀ (a b : Q) (h : a ⋖ b), P.wt (α a b h) = g b - g a) (hpath : ∀ (a b : Q) (p : PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b), P.pprod v α p ≠ 0) (huniq : ∀ (a b : Q), Subsingleton (PosetRep.EPath (fun (x1 x2 : Q) => x1 ⋖ x2) a b)) (retL : ∀ (a b c : Q) (hab : a ⋖ b) (hac : a ≤ c) (h : R), P.src h = v b → P.tgt h = v c → P.wt h = g c - g b → P.mul (P.ρA hsrc htgt hpath a b ⋯) h = some (P.ρA hsrc htgt hpath a c hac) → b ≤ c) (retR : ∀ (a b c : Q) (hab : a ⋖ b) (hcb : c ≤ b) (h : R), P.src h = v c → P.tgt h = v a → P.wt h = g a - g c → P.mul h (P.ρA hsrc htgt hpath a b ⋯) = some (P.ρA hsrc htgt hpath c b hcb) → c ≤ a) : P.Conf Q

The configuration of a tree given by its arrows.

Configurations of table posets

def MultiplicativeBasisDeformations.RaySys.Tab.Conf.ofTable {V R L : Type} [AddCommGroup L] (P : Tab V R L) {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (v : Fin n → V) (g : Fin n → L) (ρt : Fin n → Fin n → R) (hsrc : ∀ (i j : Fin n), le i j = true → P.src (ρt i j) = v i) (htgt : ∀ (i j : Fin n), le i j = true → P.tgt (ρt i j) = v j) (hwt : ∀ (i j : Fin n), le i j = true → P.wt (ρt i j) = g j - g i) (hmul : ∀ (i j l : Fin n), le i j = true → le j l = true → P.mul (ρt i j) (ρt j l) = some (ρt i l)) (hretL : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le i l = true → P.src h = v j → P.tgt h = v l → P.wt h = g l - g j → P.mul (ρt i j) h = some (ρt i l) → le j l = true) (hretR : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le l j = true → P.src h = v l → P.tgt h = v i → P.wt h = g i - g l → P.mul h (ρt i j) = some (ρt l j) → le l i = true) : P.Conf (PosetRep.Pos n le)

The configuration of a table poset given by a table of rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.table_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (v : Fin n → V) (g : Fin n → L) (ρt : Fin n → Fin n → R) (hsrc : ∀ (i j : Fin n), le i j = true → P.src (ρt i j) = v i) (htgt : ∀ (i j : Fin n), le i j = true → P.tgt (ρt i j) = v j) (hwt : ∀ (i j : Fin n), le i j = true → P.wt (ρt i j) = g j - g i) (hmul : ∀ (i j l : Fin n), le i j = true → le j l = true → P.mul (ρt i j) (ρt j l) = some (ρt i l)) (hretL : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le i l = true → P.src h = v j → P.tgt h = v l → P.wt h = g l - g j → P.mul (ρt i j) h = some (ρt i l) → le j l = true) (hretR : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le l j = true → P.src h = v l → P.tgt h = v i → P.wt h = g i - g l → P.mul h (ρt i j) = some (ρt l j) → le l i = true) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (d : Fin n → ℕ) (hu : PosetRep.UniqOK le) (hc : PosetRep.CountOK le d) : False

A forbidden tree configuration contradicts finite representation type.

theorem MultiplicativeBasisDeformations.RaySys.Tab.hmul_of_strict {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {n : ℕ} {le : Fin n → Fin n → Bool} (v : Fin n → V) (ρt : Fin n → Fin n → R) (hsrc : ∀ (i j : Fin n), le i j = true → P.src (ρt i j) = v i) (htgt : ∀ (i j : Fin n), le i j = true → P.tgt (ρt i j) = v j) (hρe : ∀ (i : Fin n), ρt i i = P.e (v i)) (hmul' : ∀ (i j l : Fin n), le i j = true → le j l = true → i ≠ j → j ≠ l → P.mul (ρt i j) (ρt j l) = some (ρt i l)) (i j l : Fin n) : le i j = true → le j l = true → P.mul (ρt i j) (ρt j l) = some (ρt i l)