Forbidden configurations in faithful supports #
def:faithful-support with Lemma 8.8: if finitely many rays from x (or into x) have a
factorization order isomorphic to a table poset that passes the decide checks of
FinPoset (unique lower covers and the dimension count), finite representation type is
contradicted. The axioms of the table poset follow from those of the factorization order.
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ax_of_rf
{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}
(r : Fin n → R)
(hr : Function.Injective r)
(hle : ∀ (i j : Fin n), le i j = true ↔ P.RF (r i) (r j))
:
PosetRep.Ax le
The axioms of a table read off a factorization order.
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ax_of_lf
{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}
(r : Fin n → R)
(hr : Function.Injective r)
(hle : ∀ (i j : Fin n), le i j = true ↔ P.LF (r i) (r j))
:
PosetRep.Ax le
theorem
MultiplicativeBasisDeformations.RaySys.Tab.projSup_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
{n : ℕ}
{le : Fin n → Fin n → Bool}
(x : V)
(r : Fin n → R)
(hr : Function.Injective r)
(hsrc : ∀ (i : Fin n), P.src (r i) = x)
(hle : ∀ (i j : Fin n), le i j = true ↔ P.RF (r i) (r j))
(d : Fin n → ℕ)
(hu : PosetRep.UniqOK le)
(hc : PosetRep.CountOK le d)
:
False
A forbidden configuration in a faithful projective support.
theorem
MultiplicativeBasisDeformations.RaySys.Tab.injSup_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
{n : ℕ}
{le : Fin n → Fin n → Bool}
(x : V)
(r : Fin n → R)
(hr : Function.Injective r)
(htgt : ∀ (i : Fin n), P.tgt (r i) = x)
(hle : ∀ (i j : Fin n), le i j = true ↔ P.LF (r i) (r j))
(d : Fin n → ℕ)
(hu : PosetRep.UniqOK le)
(hc : PosetRep.CountOK le d)
:
False
A forbidden configuration in a faithful injective support (order: r ≤ s if
r = v s).
The four-point crown: lower points 0, 1, upper points 2, 3, all four comparisons.
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.tCrown_count :
PosetRep.CountOK tCrown ![1, 1, 1, 1]
theorem
MultiplicativeBasisDeformations.RaySys.Tab.crown_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
(x : V)
(l1 l2 u1 u2 : R)
(hsrc : P.src l1 = x ∧ P.src l2 = x ∧ P.src u1 = x ∧ P.src u2 = x)
(h11 : P.RF l1 u1)
(h12 : P.RF l1 u2)
(h21 : P.RF l2 u1)
(h22 : P.RF l2 u2)
(n1 : ¬P.RF l1 l2)
(n2 : ¬P.RF l2 l1)
(n3 : ¬P.RF u1 u2)
(n4 : ¬P.RF u2 u1)
(n5 : ¬P.RF u1 l1)
(n6 : ¬P.RF u1 l2)
(n7 : ¬P.RF u2 l1)
(n8 : ¬P.RF u2 l2)
:
False
A four-point crown in a faithful projective support is excluded.
The four-leaf star 0 → 1 → 2, 3, 4.
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.tStar4_count :
PosetRep.CountOK tStar4 ![1, 2, 1, 1, 1]
theorem
MultiplicativeBasisDeformations.RaySys.Tab.star4_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
(x : V)
(p0 p1 l1 l2 l3 : R)
(hsrc : P.src p0 = x ∧ P.src p1 = x ∧ P.src l1 = x ∧ P.src l2 = x ∧ P.src l3 = x)
(h01 : P.RF p0 p1)
(h1 : P.RF p1 l1)
(h2 : P.RF p1 l2)
(h3 : P.RF p1 l3)
(n10 : ¬P.RF p1 p0)
(n1 : ∀ l ∈ [l1, l2, l3], ¬P.RF l p0 ∧ ¬P.RF l p1)
(n12 : ¬P.RF l1 l2)
(n13 : ¬P.RF l1 l3)
(n21 : ¬P.RF l2 l1)
(n23 : ¬P.RF l2 l3)
(n31 : ¬P.RF l3 l1)
(n32 : ¬P.RF l3 l2)
:
False
A four-leaf star p₀ → p₁ → l₁, l₂, l₃ in a faithful projective support is excluded.
The six-point tree 0 → 1, 2, 3 and 1 → 4, 5 (two adjacent trivalent points).
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.tSix_count :
PosetRep.CountOK tSix ![2, 2, 1, 1, 1, 1]
theorem
MultiplicativeBasisDeformations.RaySys.Tab.six_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
(x : V)
(r : Fin 6 → R)
(hsrc : ∀ (i : Fin 6), P.src (r i) = x)
(hpos : ∀ (i j : Fin 6), tSix i j = true → P.RF (r i) (r j))
(hneg : ∀ (i j : Fin 6), tSix i j = false → ¬P.RF (r i) (r j))
:
False
The six-point tree in a faithful projective support is excluded.
theorem
MultiplicativeBasisDeformations.RaySys.Tab.table_supp_false
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(P : Tab V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
(hfin : IsRepresentationFinite k ↥(P.Lin k))
{n : ℕ}
(le : Fin n → Fin n → Bool)
(x : V)
(r : Fin n → R)
(d : Fin n → ℕ)
(hu : PosetRep.UniqOK le)
(hc : PosetRep.CountOK le d)
(hanti : ∀ (i j : Fin n), le i j = true → le j i = true → i = j)
(hsrc : ∀ (i : Fin n), P.src (r i) = x)
(hpos : ∀ (i j : Fin n), le i j = true → P.RF (r i) (r j))
(hneg : ∀ (i j : Fin n), le i j = false → ¬P.RF (r i) (r j))
:
False
A table configuration in a faithful projective support, given by positive and negative comparisons.
The chain Q₀ → Q₁ → Q₂ → Q₃ with leaves Q₁ → Y₁, Q₂ → Y₂ (indices 4, 5).
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.tL6_count :
PosetRep.CountOK tL6 ![1, 2, 2, 1, 1, 1]