Finite posets of width at most two

We prove the width-two case of Dilworth's theorem in the exact form needed by the magnitude argument: a finite poset without a three-element antichain is the union of two chains.

noncomputable def MagnitudeConjecture.PosetSpace.minimalIn {T : Type u} [PartialOrder T] [Fintype T] (A : Finset T) : Finset T

The minimal elements of a finite subset of a poset.

theorem MagnitudeConjecture.PosetSpace.card_minimalIn_le_two {T : Type u} [PartialOrder T] [Fintype T] (hno : ∀ (a b c : T), ¬IsThreeAntichain a b c) (A : Finset T) : (minimalIn A).card ≤ 2

If the ambient poset has no three-element antichain, a finite subset has at most two minimal elements.

def MagnitudeConjecture.PosetSpace.successorRel {T : Type u} [PartialOrder T] (x : T) : T ⊕ Fin 2 → Prop

A left vertex may be matched either to a strictly larger poset element or to one of two terminal symbols.

theorem MagnitudeConjecture.PosetSpace.exists_injective_successor {T : Type u} [PartialOrder T] [Fintype T] (hno : ∀ (a b c : T), ¬IsThreeAntichain a b c) : ∃ (f : T → T ⊕ Fin 2), Function.Injective f ∧ ∀ (x : T), successorRel x (f x)

Hall's theorem supplies an injective successor assignment with two terminals.

noncomputable def MagnitudeConjecture.PosetSpace.strictUpperFinset {T : Type u} [PartialOrder T] [Fintype T] (x : T) : Finset T

Strict upper set of an element, used as a termination measure.

theorem MagnitudeConjecture.PosetSpace.card_strictUpperFinset_lt_of_lt {T : Type u} [PartialOrder T] [Fintype T] {x y : T} (hxy : x < y) : (strictUpperFinset y).card < (strictUpperFinset x).card

Moving strictly upward strictly decreases the cardinality of the strict upper set.

structure MagnitudeConjecture.PosetSpace.TwoSuccessor (T : Type u) [PartialOrder T] : Type u

An injective successor assignment whose only non-poset outputs are two terminal symbols.

• next : T → T ⊕ Fin 2
• next_injective : Function.Injective self.next
• related (x : T) : successorRel x (self.next x)

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.lt_of_next_eq_inl {S : Type u} [PartialOrder S] (F : TwoSuccessor S) {x y : S} (h : F.next x = Sum.inl y) : x < y

@[irreducible]

def MagnitudeConjecture.PosetSpace.TwoSuccessor.trace {S : Type u} [PartialOrder S] [Fintype S] (F : TwoSuccessor S) (x : S) : Fin 2 × ℕ

Terminal label and number of successor steps remaining.

@[simp]

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.trace_of_next_eq_inr {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) {x : T} {d : Fin 2} (h : F.next x = Sum.inr d) : F.trace x = (d, 0)

@[simp]

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.trace_of_next_eq_inl {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) {x y : T} (h : F.next x = Sum.inl y) : F.trace x = ((F.trace y).1, (F.trace y).2 + 1)

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.eq_of_trace_eq {S : Type u} [PartialOrder S] [Fintype S] (F : TwoSuccessor S) {x y : S} (htrace : F.trace x = F.trace y) : x = y

The terminal label together with the remaining path length uniquely determines a vertex.

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.trace_injective {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) : Function.Injective F.trace

The full two-terminal trace is injective.

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.le_of_trace_fst_eq_of_snd_le {S : Type u} [PartialOrder S] [Fintype S] (F : TwoSuccessor S) {x y : S} (hfst : (F.trace x).1 = (F.trace y).1) (hsnd : (F.trace y).2 ≤ (F.trace x).2) : x ≤ y

Along one terminal fiber, greater remaining path length means a smaller poset element.

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.comparable_of_trace_fst_eq {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) {x y : T} (hfst : (F.trace x).1 = (F.trace y).1) : x ≤ y ∨ y ≤ x

Vertices with the same terminal label are comparable.

def MagnitudeConjecture.PosetSpace.TwoSuccessor.terminalFiber {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) (d : Fin 2) : Set T

Fiber of the successor trace over one of the two terminal labels.

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.isChain_terminalFiber {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) (d : Fin 2) : IsChain (fun (x1 x2 : T) => x1 ≤ x2) (F.terminalFiber d)

Each terminal fiber is a chain.

theorem MagnitudeConjecture.PosetSpace.TwoSuccessor.terminalFiber_zero_union_one {T : Type u} [PartialOrder T] [Fintype T] (F : TwoSuccessor T) : F.terminalFiber 0 ∪ F.terminalFiber 1 = Set.univ

The two terminal fibers cover the whole poset.

theorem MagnitudeConjecture.PosetSpace.exists_twoSuccessor {T : Type u} [PartialOrder T] [Fintype T] (hno : ∀ (a b c : T), ¬IsThreeAntichain a b c) : Nonempty (TwoSuccessor T)

The Hall assignment as a bundled successor structure.

theorem MagnitudeConjecture.PosetSpace.exists_two_chain_cover_of_no_threeAntichain {T : Type u} [PartialOrder T] [Fintype T] (hno : ∀ (a b c : T), ¬IsThreeAntichain a b c) : ∃ (A : Set T) (B : Set T), A ∪ B = Set.univ ∧ IsChain (fun (x1 x2 : T) => x1 ≤ x2) A ∧ IsChain (fun (x1 x2 : T) => x1 ≤ x2) B

Width-two Dilworth: a finite poset without a three-element antichain is covered by two chains.

theorem MagnitudeConjecture.PosetSpace.finrank_eq_one_of_isSchur_of_no_threeAntichain {T : Type u} [PartialOrder T] [Fintype T] {k : Type u} [Field k] (X : Obj k T) (hschur : IsSchur k T X) (hno : ∀ (a b c : T), ¬IsThreeAntichain a b c) : Module.finrank k X.carrier = 1

If the indexing poset has width at most two, every Schur poset space is one-dimensional.

theorem MagnitudeConjecture.PosetSpace.exists_threeAntichain_of_isSchur_of_two_le_finrank {T : Type u} [PartialOrder T] [Fintype T] {k : Type u} [Field k] (X : Obj k T) (hschur : IsSchur k T X) (hrank : 2 ≤ Module.finrank k X.carrier) : ∃ (a : T) (b : T) (c : T), IsThreeAntichain a b c

Consequently, every Schur poset space of dimension at least two forces a three-element antichain in the indexing poset.