Lemma 8.8 for tree posets

local-ray-geometry.tex: "These counts depend only on the underlying graphs; for a tree any orientation is allowed." For a finite poset whose cover graph is acyclic, paths along covering relations are unique (subsingleton_ePath) and exist between comparable points (nonempty_ePath), so the incidence algebra is the path algebra of the oriented tree and Lemma 8.8 applies (tree_not_isRepresentationFinite); the dual poset has the same cover graph (tree_not_isRepresentationFinite_dual).

def MultiplicativeBasisDeformations.PosetRep.coverGraph (P : Type) [PartialOrder P] : SimpleGraph P

The cover graph.

theorem MultiplicativeBasisDeformations.PosetRep.adj_of_covBy {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {y z : P} (h : y ⋖ z) : (coverGraph P).Adj y z

@[irreducible]

def MultiplicativeBasisDeformations.PosetRep.toWalk {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {x y : P} : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y → (coverGraph P).Walk x y

A path along covers as a walk of the cover graph.

theorem MultiplicativeBasisDeformations.PosetRep.toWalk_nil {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (x : P) : toWalk (EPath.nil x) = SimpleGraph.Walk.nil

theorem MultiplicativeBasisDeformations.PosetRep.toWalk_cons {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {x y z : P} (p : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y) (h : y ⋖ z) : toWalk (p.cons h) = (toWalk p).concat ⋯

theorem MultiplicativeBasisDeformations.PosetRep.toWalk_support_lt {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {x y : P} (p : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y) (v : P) : v ∈ (toWalk p).support → v ≤ y

theorem MultiplicativeBasisDeformations.PosetRep.toWalk_isPath {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {x y : P} (p : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y) : (toWalk p).IsPath

theorem MultiplicativeBasisDeformations.PosetRep.toWalk_injective {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {x y : P} (p q : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y) : toWalk p = toWalk q → p = q

theorem MultiplicativeBasisDeformations.PosetRep.subsingleton_ePath {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (hT : (coverGraph P).IsAcyclic) (x y : P) : Subsingleton (EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y)

Paths along covers are unique when the cover graph is acyclic.

theorem MultiplicativeBasisDeformations.PosetRep.subsingleton_ePath_of_lowerCover {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (h : ∀ (x y m m' : P), x ≤ m → m ⋖ y → x ≤ m' → m' ⋖ y → m = m') {x y : P} (p q : EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y) : p = q

Paths along covers are unique when lower covers above a point are unique: if every y has at most one lower cover m with x ≤ m (true for trees and crowns).

theorem MultiplicativeBasisDeformations.PosetRep.nonempty_ePath {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (x y : P) (h : x ≤ y) : Nonempty (EPath (fun (x1 x2 : P) => x1 ⋖ x2) x y)

Comparable points are joined by covers.

theorem MultiplicativeBasisDeformations.PosetRep.isAcyclic_of_rank {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (r : V → ℕ) (hr : Function.Injective r) (h : ∀ (v a b : V), G.Adj v a → G.Adj v b → r a < r v → r b < r v → a = b) : G.IsAcyclic

A rank criterion for acyclicity: if every vertex has at most one neighbour of smaller rank, the graph is acyclic (the vertex of largest rank on a cycle would have two).

def MultiplicativeBasisDeformations.PosetRep.incMap {P : Type} [PartialOrder P] {k : Type u} [Field k] {Q : Type} [PartialOrder Q] (e : P ≃o Q) (f : IncidenceAlgebra k P) : IncidenceAlgebra k Q

Transport of incidence functions along an order isomorphism.

def MultiplicativeBasisDeformations.PosetRep.incidenceEquiv {P : Type} [PartialOrder P] [DecidableEq P] [LocallyFiniteOrder P] {k : Type u} [Field k] {Q : Type} [PartialOrder Q] [Fintype Q] [DecidableEq Q] [LocallyFiniteOrder Q] (e : P ≃o Q) : IncidenceAlgebra k P ≃ₐ[k] IncidenceAlgebra k Q

Incidence algebras of isomorphic posets are isomorphic.

theorem MultiplicativeBasisDeformations.PosetRep.covBy_lt {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (x y : P) (h : x ⋖ y) : x < y

theorem MultiplicativeBasisDeformations.PosetRep.tree_not_isRepresentationFinite {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (k : Type u) [Field k] [IsAlgClosed k] [DecidableRel fun (x1 x2 : P) => x1 ⋖ x2] (hT : (coverGraph P).IsAcyclic) (d : P → ℕ) (hd : ∃ (v : P), 0 < d v) (hN : ∑ v : P, d v ^ 2 ≤ ∑ a : Arr fun (x1 x2 : P) => x1 ⋖ x2, d (tgt a) * d (src a)) : ¬IsRepresentationFinite k (IncidenceAlgebra k P)

Lemma 8.8 for a poset whose cover graph is acyclic.

Duals

theorem MultiplicativeBasisDeformations.PosetRep.coverGraph_dual_adj {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] [DecidableRel fun (x1 x2 : P) => x1 ⋖ x2] (x y : Pᵒᵈ) : (coverGraph Pᵒᵈ).Adj x y ↔ (coverGraph P).Adj (OrderDual.ofDual x) (OrderDual.ofDual y)

theorem MultiplicativeBasisDeformations.PosetRep.isAcyclic_dual {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] [DecidableRel fun (x1 x2 : P) => x1 ⋖ x2] (hT : (coverGraph P).IsAcyclic) : (coverGraph Pᵒᵈ).IsAcyclic

def MultiplicativeBasisDeformations.PosetRep.arrDual {P : Type} [PartialOrder P] : (Arr fun (x1 x2 : Pᵒᵈ) => x1 ⋖ x2) ≃ Arr fun (x1 x2 : P) => x1 ⋖ x2

The arrows of the dual poset.

theorem MultiplicativeBasisDeformations.PosetRep.sum_arr_dual {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] [DecidableRel fun (x1 x2 : P) => x1 ⋖ x2] [DecidableRel fun (x1 x2 : Pᵒᵈ) => x1 ⋖ x2] (d : P → ℕ) : ∑ a : Arr fun (x1 x2 : Pᵒᵈ) => x1 ⋖ x2, d (OrderDual.ofDual (tgt a)) * d (OrderDual.ofDual (src a)) = ∑ a : Arr fun (x1 x2 : P) => x1 ⋖ x2, d (tgt a) * d (src a)

theorem MultiplicativeBasisDeformations.PosetRep.tree_not_isRepresentationFinite_dual {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (k : Type u) [Field k] [IsAlgClosed k] [DecidableRel fun (x1 x2 : P) => x1 ⋖ x2] [DecidableRel fun (x1 x2 : Pᵒᵈ) => x1 ⋖ x2] (hT : (coverGraph P).IsAcyclic) (d : P → ℕ) (hd : ∃ (v : P), 0 < d v) (hN : ∑ v : P, d v ^ 2 ≤ ∑ a : Arr fun (x1 x2 : P) => x1 ⋖ x2, d (tgt a) * d (src a)) : ¬IsRepresentationFinite k (IncidenceAlgebra k Pᵒᵈ)