Concrete finite posets and forbidden configurations

For the configurations excluded by Lemma 8.8 in Part III (four-point crowns, four-leaf stars, the Euclidean trees of the table after lem:dimension-infinity): a poset on Fin n given by a Boolean table (Pos), whose axioms, cover relation, uniqueness of lower covers and dimension count are checked by decide. forbidden transfers the conclusion along an order isomorphism, for the poset and its dual.

structure MultiplicativeBasisDeformations.PosetRep.Pos (n : ℕ) (le : Fin n → Fin n → Bool) : Type

A poset on Fin n given by a table.

• v : Fin n

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableEqPos {n✝ : ℕ} {le✝ : Fin n✝ → Fin n✝ → Bool} : DecidableEq (Pos n✝ le✝)

def MultiplicativeBasisDeformations.PosetRep.instDecidableEqPos.decEq {n✝ : ℕ} {le✝ : Fin n✝ → Fin n✝ → Bool} (x✝ x✝¹ : Pos n✝ le✝) : Decidable (x✝ = x✝¹)

def MultiplicativeBasisDeformations.PosetRep.posEquiv {n : ℕ} {le : Fin n → Fin n → Bool} : Pos n le ≃ Fin n

The underlying vertices.

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instFintypePos {n : ℕ} {le : Fin n → Fin n → Bool} : Fintype (Pos n le)

def MultiplicativeBasisDeformations.PosetRep.ltB {n : ℕ} (le : Fin n → Fin n → Bool) (i j : Fin n) : Bool

The strict comparison of the table.

def MultiplicativeBasisDeformations.PosetRep.covB {n : ℕ} (le : Fin n → Fin n → Bool) (i j : Fin n) : Bool

The cover relation of the table.

def MultiplicativeBasisDeformations.PosetRep.Ax {n : ℕ} (le : Fin n → Fin n → Bool) : Prop

The axioms of a partial order, checked on the table.

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instPartialOrderPos {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : PartialOrder (Pos n le)

theorem MultiplicativeBasisDeformations.PosetRep.pos_le_iff {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (a b : Pos n le) : a ≤ b ↔ le a.v b.v = true

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableRelPosLe {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : DecidableRel fun (x1 x2 : Pos n le) => x1 ≤ x2

theorem MultiplicativeBasisDeformations.PosetRep.pos_lt_iff {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (a b : Pos n le) : a < b ↔ ltB le a.v b.v = true

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableRelPosLt {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : DecidableRel fun (x1 x2 : Pos n le) => x1 < x2

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instLocallyFiniteOrderPos {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : LocallyFiniteOrder (Pos n le)

theorem MultiplicativeBasisDeformations.PosetRep.pos_covBy_iff {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (a b : Pos n le) : a ⋖ b ↔ covB le a.v b.v = true

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableRelPosCovBy {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : DecidableRel fun (x1 x2 : Pos n le) => x1 ⋖ x2

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableRelOrderDualPosCovBy {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : DecidableRel fun (x1 x2 : (Pos n le)ᵒᵈ) => x1 ⋖ x2

def MultiplicativeBasisDeformations.PosetRep.UniqOK {n : ℕ} (le : Fin n → Fin n → Bool) : Prop

Unique lower covers above a point, on the table.

theorem MultiplicativeBasisDeformations.PosetRep.pos_uniq {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (hu : UniqOK le) (x y : Pos n le) : Subsingleton (EPath (fun (x1 x2 : Pos n le) => x1 ⋖ x2) x y)

def MultiplicativeBasisDeformations.PosetRep.CountOK {n : ℕ} (le : Fin n → Fin n → Bool) (d : Fin n → ℕ) : Prop

The dimension count on the table.

theorem MultiplicativeBasisDeformations.PosetRep.pos_sq_eq {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (d : Fin n → ℕ) : ∑ v : Pos n le, d v.v ^ 2 = ∑ i : Fin n, d i ^ 2

theorem MultiplicativeBasisDeformations.PosetRep.pos_arr_eq {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (d : Fin n → ℕ) : ∑ a : Arr fun (x1 x2 : Pos n le) => x1 ⋖ x2, d (tgt a).v * d (src a).v = ∑ i : Fin n, ∑ j : Fin n, if covB le i j = true then d i * d j else 0

theorem MultiplicativeBasisDeformations.PosetRep.pos_count {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (d : Fin n → ℕ) (hc : CountOK le d) : ∑ v : Pos n le, d v.v ^ 2 ≤ ∑ a : Arr fun (x1 x2 : Pos n le) => x1 ⋖ x2, d (tgt a).v * d (src a).v

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

Forbidden configurations: a poset isomorphic to a table poset with unique lower covers whose dimension count holds has representation-infinite incidence algebra.

Transposed tables

instance MultiplicativeBasisDeformations.PosetRep.instFactAxFlipFinBool {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : Fact (Ax (flip le))

def MultiplicativeBasisDeformations.PosetRep.flipIso {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] : Pos n (flip le) ≃o (Pos n le)ᵒᵈ

The transposed table is the dual poset.

theorem MultiplicativeBasisDeformations.PosetRep.forbidden_dual {n : ℕ} {le : Fin n → Fin n → Bool} [hA : Fact (Ax le)] (k : Type u) [Field k] [IsAlgClosed k] {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [LocallyFiniteOrder Q] (e : Pos n le ≃o Q) (d : Fin n → ℕ) (hu : UniqOK (flip le)) (hc : CountOK (flip le) d) : ¬IsRepresentationFinite k (IncidenceAlgebra k Qᵒᵈ)

Forbidden configurations, dual form.