Linear extensions of posets

DefinitionLinear extensions of a finite poset#✓fully proved

Let \(\alpha\) be a finite poset with \(n\) elements. Its linear extensions are represented as rank functions: the set of linear extensions of \(\alpha\) is the finite set of all maps \(\sigma : \alpha \to \{0, 1, \dots, n-1\}\) that are bijective and monotone, meaning that \(x \le y\) implies \(\sigma(x) \le \sigma(y)\).

noncomputable def linearExtensions (α : Type*) [Fintype α] [PartialOrder α] :
    Finset (α → Fin (Fintype.card α)) := by
  classical
  exact Finset.univ.filter fun σ => Function.Bijective σ ∧ Monotone σ

Used by 3

Used byThe number of linear extensions is positive · Membership in the linear extensions · Existence of linear extensions

TheoremMembership in the linear extensions#✓fully proved

Let \(\alpha\) be a finite poset with \(n\) elements. A map \(\sigma : \alpha \to \{0, 1, \dots, n-1\}\) belongs to the set of linear extensions of \(\alpha\) if and only if \(\sigma\) is bijective and monotone.

theorem mem_linearExtensions (α : Type*) [Fintype α] [PartialOrder α]
    (σ : α → Fin (Fintype.card α)) :
    σ ∈ linearExtensions α ↔ Function.Bijective σ ∧ Monotone σ

Uses 1 · Used by 1

Statement usesLinear extensions of a finite poset

Used byExistence of linear extensions

DefinitionRanking a Szpilrajn linear extension#✓fully proved

Let \(\alpha\) be a finite poset with \(n\) elements, and fix a linear order on \(\alpha\) extending its partial order (one exists by Szpilrajn's extension theorem; it is chosen once and for all). This is the order isomorphism from \(\alpha\) with that linear order onto \(\{0, 1, \dots, n-1\}\) with its usual order.

noncomputable def linExtOrderIso (α : Type*) [Fintype α] [PartialOrder α] :
    LinearExtension α ≃o Fin (Fintype.card α) := by
  have : Fintype (LinearExtension α) := inferInstanceAs (Fintype α)
  have hcard : Fintype.card (LinearExtension α) = Fintype.card α :=
    Fintype.card_congr (Equiv.refl α : α ≃ LinearExtension α)
  exact (Fintype.orderIsoFinOfCardEq (LinearExtension α) rfl).symm.trans
    (Fin.castOrderIso hcard)

Used by 3

Used byThe chosen linear extension is bijective · The chosen linear extension is monotone · A chosen linear extension

DefinitionA chosen linear extension#✓fully proved

Let \(\alpha\) be a finite poset with \(n\) elements, and fix a linear order on \(\alpha\) extending its partial order (one exists by Szpilrajn's extension theorem; it is chosen once and for all). The chosen linear extension of \(\alpha\) is the rank function \(\alpha \to \{0, 1, \dots, n-1\}\) sending each element to its position in that linear order, counted from \(0\).

noncomputable def someLinearExtension (α : Type*) [Fintype α] [PartialOrder α] :
    α → Fin (Fintype.card α) := fun x =>
  linExtOrderIso α (toLinearExtension x)

Uses 1 · Used by 3

Statement usesRanking a Szpilrajn linear extension

Used byThe chosen linear extension is bijective · The chosen linear extension is monotone · Existence of linear extensions

TheoremThe chosen linear extension is bijective#✓fully proved

For every finite poset \(\alpha\) with \(n\) elements, the chosen linear extension of \(\alpha\), viewed as a rank function \(\alpha \to \{0, 1, \dots, n-1\}\), is a bijection.

theorem bijective_someLinearExtension (α : Type*) [Fintype α] [PartialOrder α] :
    Function.Bijective (someLinearExtension α)

Uses 2 · Used by 1

Statement usesA chosen linear extension

Proof usesRanking a Szpilrajn linear extension

Used byExistence of linear extensions

TheoremThe chosen linear extension is monotone#✓fully proved

For every finite poset \(\alpha\) with \(n\) elements, the chosen linear extension of \(\alpha\), viewed as a rank function \(\sigma : \alpha \to \{0, 1, \dots, n-1\}\), is monotone: \(x \le y\) implies \(\sigma(x) \le \sigma(y)\).

theorem monotone_someLinearExtension (α : Type*) [Fintype α] [PartialOrder α] :
    Monotone (someLinearExtension α)

Uses 2 · Used by 1

Statement usesA chosen linear extension

Proof usesRanking a Szpilrajn linear extension

Used byExistence of linear extensions

TheoremExistence of linear extensions#✓fully proved

Every finite poset has a linear extension.

theorem nonempty_linearExtensions (α : Type*) [Fintype α] [PartialOrder α] :
    (linearExtensions α).Nonempty

Uses 5 · Used by 1

Statement usesLinear extensions of a finite poset

Proof usesThe chosen linear extension is bijective · Membership in the linear extensions · The chosen linear extension is monotone · A chosen linear extension

Used byThe number of linear extensions is positive

TheoremThe number of linear extensions is positive#✓fully proved

For every finite poset \(\alpha\), the number of linear extensions of \(\alpha\) is positive.

So this count is a valid denominator for probabilities over linear extensions.

theorem card_linearExtensions_pos (α : Type*) [Fintype α] [PartialOrder α] :
    0 < (linearExtensions α).card

Uses 2

Statement usesLinear extensions of a finite poset

Proof usesExistence of linear extensions

DefinitionMaximal elements of a finite set#✓fully proved

For a finite subset \(A\) of a partially ordered set \(P\), the maximal elements of \(A\) form the subset of those \(x \in A\) such that every \(y \in A\) with \(x \le y\) equals \(x\).

noncomputable def maximalElements {P : Type*} [PartialOrder P]
    (A : Finset P) : Finset P := by
  classical
  exact A.filter fun x ↦ ∀ y ∈ A, x ≤ y → y = x

Used by 1

Used byMembership in the maximal elements

TheoremMembership in the maximal elements#✓fully proved

Let \(A\) be a finite subset of a partially ordered set \(P\) and let \(x \in P\). Then \(x\) belongs to the set of maximal elements of \(A\) if and only if \(x \in A\) and every \(y \in A\) with \(x \le y\) equals \(x\).

theorem mem_maximalElements {P : Type*} [PartialOrder P] (A : Finset P)
    (x : P) : x ∈ maximalElements A ↔ x ∈ A ∧ ∀ y ∈ A, x ≤ y → y = x

Uses 1

Statement usesMaximal elements of a finite set

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.