Lemma 8.8 for incidence algebras of posets with unique paths

local-ray-geometry.tex (lem:dimension-infinity and the table after it): "For the relation-free diagrams used below the required vectors are […] These counts depend only on the underlying graphs; for a tree any orientation is allowed."

Here: a finite poset P with a set E of arrows (x < y) such that between comparable points there is exactly one E-path. Its incidence algebra is the path algebra of E, so a right module of dimension vector d is a tuple of matrices on the arrows, and isomorphism is conjugation by ∏ GL_{d v} (isoConj). If ∑ d_v² ≤ ∑_{x → y} d_x d_y and d ≠ 0, the incidence algebra is representation-infinite (not_isRepresentationFinite): finite representation type would give finitely many orbits (exists_labels_iso), contradicting OrbitDim.orbits_not_finite with F = 0.

Paths along the arrows

inductive MultiplicativeBasisDeformations.PosetRep.EPath {P : Type} (E : P → P → Prop) : P → P → Type

Paths along the arrows E.

• nil {P : Type} {E : P → P → Prop} (x : P) : EPath E x x
• cons {P : Type} {E : P → P → Prop} {x y z : P} (p : EPath E x y) (h : E y z) : EPath E x z

def MultiplicativeBasisDeformations.PosetRep.EPath.comp {P : Type} {E : P → P → Prop} {x y : P} (p : EPath E x y) {z : P} : EPath E y z → EPath E x z

Concatenation.

theorem MultiplicativeBasisDeformations.PosetRep.EPath.le {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {x y : P} : ∀ (a : EPath E x y), x ≤ y

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.Sp {P : Type} (k : Type u) (d : P → ℕ) (v : P) : Type u

The vector space at a vertex.

@[irreducible]

def MultiplicativeBasisDeformations.PosetRep.tr {k : Type u} [Field k] {P : Type} {E : P → P → Prop} (d : P → ℕ) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y : P} : EPath E x y → Sp k d x →ₗ[k] Sp k d y

Transport along a path.

theorem MultiplicativeBasisDeformations.PosetRep.tr_nil {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (x : P) : tr d M (EPath.nil x) = LinearMap.id

theorem MultiplicativeBasisDeformations.PosetRep.tr_cons {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y z : P} (p : EPath E x y) (h : E y z) : tr d M (p.cons h) = M y z h ∘ₗ tr d M p

theorem MultiplicativeBasisDeformations.PosetRep.tr_comp {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y : P} (p : EPath E x y) {z : P} (q : EPath E y z) : tr d M (p.comp q) = tr d M q ∘ₗ tr d M p

noncomputable def MultiplicativeBasisDeformations.PosetRep.T {k : Type u} [Field k] {P : Type} [PartialOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (x y : P) : Sp k d x →ₗ[k] Sp k d y

The transport between comparable points.

theorem MultiplicativeBasisDeformations.PosetRep.T_path {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y : P} (p : EPath E x y) : T d hex M x y = tr d M p

theorem MultiplicativeBasisDeformations.PosetRep.T_self {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (x : P) : T d hex M x x = LinearMap.id

theorem MultiplicativeBasisDeformations.PosetRep.T_trans {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y z : P} (hxy : x ≤ y) (hyz : y ≤ z) : T d hex M x z = T d hex M y z ∘ₗ T d hex M x y

theorem MultiplicativeBasisDeformations.PosetRep.T_arrow {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y : P} (h : E x y) : T d hex M x y = M x y h

theorem MultiplicativeBasisDeformations.PosetRep.T_not_le {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) {x y : P} (h : ¬x ≤ y) : T d hex M x y = 0

The module of a tuple of matrices

noncomputable def MultiplicativeBasisDeformations.PosetRep.act {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v) (v : P) : Sp k d v

The action of the incidence algebra.

theorem MultiplicativeBasisDeformations.PosetRep.act_mul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (a b : IncidenceAlgebra k P) (w : (v : P) → Sp k d v) : act d hex M (b * a) w = act d hex M a (act d hex M b w)

theorem MultiplicativeBasisDeformations.PosetRep.act_one {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (w : (v : P) → Sp k d v) : act d hex M 1 w = w

theorem MultiplicativeBasisDeformations.PosetRep.act_algebraMap {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (c : k) (w : (v : P) → Sp k d v) : act d hex M ((algebraMap k (IncidenceAlgebra k P)) c) w = c • w

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.Car {k : Type u} [Field k] {P : Type} {E : P → P → Prop} (d : P → ℕ) (_M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : Type u

The carrier.

noncomputable def MultiplicativeBasisDeformations.PosetRep.repModule {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : Module (IncidenceAlgebra k P)ᵐᵒᵖ (Car d M)

The right module structure.

noncomputable def MultiplicativeBasisDeformations.PosetRep.repObj {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : RightModuleCat (IncidenceAlgebra k P)

The module of a tuple of matrices.

def MultiplicativeBasisDeformations.PosetRep.toPi {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : ↑(repObj d hE huniq hex M) →ₗ[k] (v : P) → Sp k d v

The identification with ∏ k^{d v} is k-linear.

theorem MultiplicativeBasisDeformations.PosetRep.repObj_finite {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : Module.Finite k ↑(repObj d hE huniq hex M)

Isomorphisms are conjugations

def MultiplicativeBasisDeformations.PosetRep.sgl {k : Type u} [Field k] {P : Type} [PartialOrder P] [DecidableEq P] (x y : P) (h : x ≤ y) : IncidenceAlgebra k P

The matrix unit at x ≤ y.

theorem MultiplicativeBasisDeformations.PosetRep.act_sgl {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (p q : P) (hpq : p ≤ q) (w : (v : P) → Sp k d v) : act d hex M (sgl p q hpq) w = Pi.single q ((T d hex M p q) (w p))

def MultiplicativeBasisDeformations.PosetRep.comp {k : Type u} [Field k] {P : Type} [DecidableEq P] (d : P → ℕ) (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (v : P) (u : Sp k d v) : Sp k d v

The component maps of an isomorphism.

theorem MultiplicativeBasisDeformations.PosetRep.f_single {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M M' : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hf : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), f (act d hex M a w) = act d hex M' a (f w)) (v : P) (u : Sp k d v) : f (Pi.single v u) = Pi.single v (comp d f v u)

theorem MultiplicativeBasisDeformations.PosetRep.f_smul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M M' : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hf : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), f (act d hex M a w) = act d hex M' a (f w)) (c : k) (w : (v : P) → Sp k d v) : f (c • w) = c • f w

def MultiplicativeBasisDeformations.PosetRep.compL {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M M' : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hf : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), f (act d hex M a w) = act d hex M' a (f w)) (hfa : ∀ (w w' : (v : P) → Sp k d v), f (w + w') = f w + f w') (v : P) : Sp k d v →ₗ[k] Sp k d v

The component maps as linear maps.

theorem MultiplicativeBasisDeformations.PosetRep.comp_arrow {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M M' : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hf : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), f (act d hex M a w) = act d hex M' a (f w)) (hfa : ∀ (w w' : (v : P) → Sp k d v), f (w + w') = f w + f w') {p q : P} (h : E p q) (u : Sp k d p) : (compL d hE huniq hex f hf hfa q) ((M p q h) u) = (M' p q h) ((compL d hE huniq hex f hf hfa p) u)

The arrow relation g_q M_e = M'_e g_p.

theorem MultiplicativeBasisDeformations.PosetRep.comp_left_inv {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M M' : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (f : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hf : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), f (act d hex M a w) = act d hex M' a (f w)) (hfa : ∀ (w w' : (v : P) → Sp k d v), f (w + w') = f w + f w') (g : ((v : P) → Sp k d v) → (v : P) → Sp k d v) (hg : ∀ (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v), g (act d hex M' a w) = act d hex M a (g w)) (hga : ∀ (w w' : (v : P) → Sp k d v), g (w + w') = g w + g w') (hgf : ∀ (w : (v : P) → Sp k d v), g (f w) = w) (v : P) (u : Sp k d v) : (compL d hE huniq hex g hg hga v) ((compL d hE huniq hex f hf hfa v) u) = u

Points of the representation space

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.Arr {P : Type} (E : P → P → Prop) : Type

The arrows.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.src {P : Type} {E : P → P → Prop} (a : Arr E) : P

The source of an arrow.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.tgt {P : Type} {E : P → P → Prop} (a : Arr E) : P

The target of an arrow.

def MultiplicativeBasisDeformations.PosetRep.Mpt {k : Type u} [Field k] {P : Type} {E : P → P → Prop} (d : P → ℕ) (x : OrbitDim.Coord d src tgt → k) (p q : P) : E p q → Sp k d p →ₗ[k] Sp k d q

The maps of a point of the representation space.

theorem MultiplicativeBasisDeformations.PosetRep.conj_of_iso {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) [DecidableRel E] (x y : OrbitDim.Coord d src tgt → k) (L : ↑(repObj d hE huniq hex (Mpt d x)) ≃ₗ[(IncidenceAlgebra k P)ᵐᵒᵖ] ↑(repObj d hE huniq hex (Mpt d y))) : ∃ (g : (v : P) → GL (Fin (d v)) k), y = OrbitDim.act g x

Isomorphic modules are conjugate points.

noncomputable def MultiplicativeBasisDeformations.PosetRep.Obj {k : Type u} [Field k] {P : Type} [PartialOrder P] [DecidableEq P] [LocallyFiniteOrder P] {N : ℕ} (X : Fin N → RightModuleCat (IncidenceAlgebra k P)) (B : ℕ) (τ : (m : Fin (B + 1)) × (Fin ↑m → Fin N)) : RightModuleCat (IncidenceAlgebra k P)

The labelled biproducts.

theorem MultiplicativeBasisDeformations.PosetRep.finrank_repObj_le {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) [DecidableRel E] (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : Module.finrank k ↑(repObj d hE huniq hex M) ≤ ∑ v : P, d v

theorem MultiplicativeBasisDeformations.PosetRep.not_isRepresentationFinite {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) [DecidableRel E] [IsAlgClosed k] (hd : ∃ (v : P), 0 < d v) (hN : ∑ v : P, d v ^ 2 ≤ ∑ a : Arr E, d (tgt a) * d (src a)) : ¬IsRepresentationFinite k (IncidenceAlgebra k P)

Lemma 8.8 (lem:dimension-infinity) for incidence algebras of posets with unique paths: if d ≠ 0 and ∑ d_v² ≤ ∑_{x → y} d_x d_y, the incidence algebra is representation-infinite.