Small-arity classification for noncrossing partitions

TheoremNoncrossing partitions of one point are indiscrete#✓fully proved

Every noncrossing partition of the one-point set \(\{0\}\) equals the indiscrete noncrossing partition of \(\{0\}\).

theorem eq_indiscrete_one (P : NoncrossingPartition 1) : P = indiscrete 1

Uses 7 · Used by 1

Statement usesNoncrossing partition · The indiscrete noncrossing partition

Proof usesA partition has a block exactly when its ground set is nonempty · Recognizing the one-block partition · Noncrossing set partition · Set partition · Characterization of the indiscrete noncrossing partition

Used byNoncrossing partitions of a one-element set

TheoremThe discrete and indiscrete partitions of a two-element set differ#✓fully proved

The discrete noncrossing partition of \(\{0, 1\}\) is not equal to the indiscrete noncrossing partition of \(\{0, 1\}\).

theorem discrete_two_ne_indiscrete_two : discrete 2 ≠ indiscrete 2

Uses 7 · Used by 3

Statement usesNoncrossing partition · Discrete noncrossing partition · The indiscrete noncrossing partition

Proof usesNoncrossing set partition · Set partition · The discrete noncrossing partition consists of the singletons · The indiscrete partition of a nonempty set has a single block

Used byNoncrossing partitions of a two-element set · Enumerating the proper noncrossing partitions of three points · The proper noncrossing partition of two points

TheoremClassification of noncrossing partitions of a two-element set#✓fully proved

Every noncrossing partition of \(\{0, 1\}\) is either the discrete or the indiscrete noncrossing partition of \(\{0, 1\}\).

theorem eq_discrete_or_indiscrete_two (P : NoncrossingPartition 2) :
    P = discrete 2 ∨ P = indiscrete 2

Uses 10 · Used by 2

Statement usesNoncrossing partition · Discrete noncrossing partition · The indiscrete noncrossing partition

Proof usesA partition has a block exactly when its ground set is nonempty · Recognizing the partition into singletons by its number of blocks · Recognizing the one-block partition · Noncrossing set partition · Set partition · Characterization of the discrete noncrossing partition · Characterization of the indiscrete noncrossing partition

Used byNoncrossing partitions of a two-element set · The proper noncrossing partition of two points

TheoremNoncrossing partitions of the empty set#✓fully proved

There is exactly one noncrossing partition of the empty set, that is, of \(\{0, \dots, n-1\}\) for \(n = 0\).

@[simp]
theorem card_zero : Fintype.card (NoncrossingPartition 0) = 1

Uses 6 · Used by 2

Statement usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Proof usesThe indiscrete noncrossing partition · The indiscrete partition of the empty set has no blocks

Used bySmall values of the lonely singles count · Base value of the noncrossing block and singleton count

TheoremNoncrossing partitions of a one-element set#✓fully proved

There is exactly one noncrossing partition of \(\{0\}\).

@[simp]
theorem card_one : Fintype.card (NoncrossingPartition 1) = 1

Uses 6 · Used by 1

Statement usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Proof usesNoncrossing partitions of one point are indiscrete · The indiscrete noncrossing partition

Used bySmall values of the lonely singles count

TheoremNoncrossing partitions of a two-element set#✓fully proved

There are exactly two noncrossing partitions of \(\{0, 1\}\).

@[simp]
theorem card_two : Fintype.card (NoncrossingPartition 2) = 2

Uses 8

Statement usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Proof usesDiscrete noncrossing partition · The discrete and indiscrete partitions of a two-element set differ · Classification of noncrossing partitions of a two-element set · The indiscrete noncrossing partition

DefinitionThe proper noncrossing partition of two points#✓fully proved

Call a noncrossing partition of \(\{0, 1\}\) proper if it is not the indiscrete one. This is the bijection from a one-element set onto the set of proper noncrossing partitions of \(\{0, 1\}\), sending its element to the discrete noncrossing partition; in particular the discrete partition is the only proper one.

def properTwoEquiv : Unit ≃ { P : NoncrossingPartition 2 // P ≠ indiscrete 2 } where
  toFun _ := ⟨discrete 2, discrete_two_ne_indiscrete_two⟩
  invFun _ := ()
  left_inv _ := rfl
  right_inv := by
    intro ⟨P, hP⟩
    have h_eq : P = discrete 2 := by
      rcases eq_discrete_or_indiscrete_two P with hD | hI
      · exact hD
      · exact absurd hI hP
    exact Subtype.ext h_eq.symm

Uses 5

Statement usesNoncrossing partition · Discrete noncrossing partition · The discrete and indiscrete partitions of a two-element set differ · Classification of noncrossing partitions of a two-element set · The indiscrete noncrossing partition

DefinitionTwo-block partition of three points#✓fully proved

For \(a \in \{0, 1, 2\}\), this is the noncrossing partition of \(\{0, 1, 2\}\) whose blocks are \(\{a\}\) and \(\{0, 1, 2\} \setminus \{a\}\).

def twoBlockPartition (a : Fin 3) : NoncrossingPartition 3 :=
  ⟨Finpartition.atomise Finset.univ ({ {a} } : Finset (Finset (Fin 3))),
    isNoncrossing_of_le_three (by decide) _⟩

Uses 4 · Used by 4

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · Partitions of at most three points are noncrossing

Used byClassification of noncrossing partitions of a three-element set · Enumerating the proper noncrossing partitions of three points · Enumerating the two-block noncrossing partitions of three points · The two-block partitions of three points are not indiscrete

TheoremNoncrossing partitions of three points have one, two or three blocks#✓fully proved

Every noncrossing partition of \(\{0, 1, 2\}\) has one, two, or three blocks.

theorem three_card_one_two_three (P : NoncrossingPartition 3) :
    P.val.parts.card = 1 ∨ P.val.parts.card = 2 ∨ P.val.parts.card = 3

Uses 4 · Used by 1

Statement usesNoncrossing partition · Noncrossing set partition · Set partition

Proof usesA partition has a block exactly when its ground set is nonempty

Used byClassification of noncrossing partitions of a three-element set

TheoremA noncrossing partition of three points with one block is indiscrete#✓fully proved

If a noncrossing partition \(P\) of \(\{0, 1, 2\}\) has exactly one block, then \(P\) is the indiscrete noncrossing partition of \(\{0, 1, 2\}\).

theorem eq_indiscrete_of_card_one_three (P : NoncrossingPartition 3)
    (h_card : P.val.parts.card = 1) : P = indiscrete 3

Uses 6 · Used by 1

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · The indiscrete noncrossing partition

Proof usesRecognizing the one-block partition · Characterization of the indiscrete noncrossing partition

Used byClassification of noncrossing partitions of a three-element set

TheoremA noncrossing partition of three points with three blocks is discrete#✓fully proved

If a noncrossing partition \(P\) of \(\{0, 1, 2\}\) has exactly three blocks, then \(P\) is the discrete noncrossing partition of \(\{0, 1, 2\}\).

theorem eq_discrete_of_card_three_three (P : NoncrossingPartition 3)
    (h_card : P.val.parts.card = 3) : P = discrete 3

Uses 6 · Used by 1

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · Discrete noncrossing partition

Proof usesRecognizing the partition into singletons by its number of blocks · Characterization of the discrete noncrossing partition

Used byClassification of noncrossing partitions of a three-element set

TheoremClassification of noncrossing partitions of a three-element set#✓fully proved

Every noncrossing partition \(P\) of \(\{0, 1, 2\}\) is the discrete noncrossing partition of \(\{0, 1, 2\}\), the indiscrete noncrossing partition of \(\{0, 1, 2\}\), or, for some \(a \in \{0, 1, 2\}\), the two-block noncrossing partition whose blocks are \(\{a\}\) and \(\{0, 1, 2\} \setminus \{a\}\).

theorem eq_discrete_or_indiscrete_or_twoBlock_three (P : NoncrossingPartition 3) :
    P = discrete 3 ∨ P = indiscrete 3 ∨ ∃ a : Fin 3, P = twoBlockPartition a

Uses 9 · Used by 1

Statement usesNoncrossing partition · Discrete noncrossing partition · The indiscrete noncrossing partition · Two-block partition of three points

Proof usesNoncrossing set partition · Set partition · A noncrossing partition of three points with three blocks is discrete · A noncrossing partition of three points with one block is indiscrete · Noncrossing partitions of three points have one, two or three blocks

Used byEnumerating the proper noncrossing partitions of three points

TheoremThe discrete and indiscrete partitions of a three-element set differ#✓fully proved

The discrete noncrossing partition of \(\{0, 1, 2\}\) is not equal to the indiscrete noncrossing partition of \(\{0, 1, 2\}\).

theorem discrete_three_ne_indiscrete_three :
    discrete 3 ≠ indiscrete 3

Uses 7 · Used by 1

Statement usesNoncrossing partition · Discrete noncrossing partition · The indiscrete noncrossing partition

Proof usesNoncrossing set partition · Set partition · The discrete noncrossing partition consists of the singletons · The indiscrete partition of a nonempty set has a single block

Used byEnumerating the proper noncrossing partitions of three points

TheoremThe two-block partitions of three points are not indiscrete#✓fully proved

For every \(a \in \{0, 1, 2\}\), the noncrossing partition of \(\{0, 1, 2\}\) with blocks \(\{a\}\) and \(\{0, 1, 2\} \setminus \{a\}\) is different from the indiscrete noncrossing partition of \(\{0, 1, 2\}\).

theorem twoBlockPartition_ne_indiscrete_three (a : Fin 3) :
    twoBlockPartition a ≠ indiscrete 3

Uses 6

Statement usesNoncrossing partition · The indiscrete noncrossing partition · Two-block partition of three points

Proof usesNoncrossing set partition · Set partition · The indiscrete partition of a nonempty set has a single block

DefinitionEnumerating the two-block noncrossing partitions of three points#✓fully proved

The map sending \(a \in \{0, 1, 2\}\) to the partition of \(\{0, 1, 2\}\) with blocks \(\{a\}\) and \(\{0, 1, 2\} \setminus \{a\}\) is a bijection from \(\{0, 1, 2\}\) onto the set of noncrossing partitions of \(\{0, 1, 2\}\) with exactly two blocks.

noncomputable def twoBlockEquiv :
    Fin 3 ≃ { P : NoncrossingPartition 3 // P.val.parts.card = 2 } :=
  Equiv.ofBijective
    (fun a => ⟨twoBlockPartition a, twoBlockPartition_parts_card a⟩)
    ⟨by
      intro a b h_eq
      have h_val : twoBlockPartition a = twoBlockPartition b := by
        have := congrArg Subtype.val h_eq
        exact this
      exact twoBlockPartition_injective h_val,
     by
      intro ⟨P, hP⟩
      obtain ⟨a, ha⟩ := twoBlockPartition_surjective_on_two_blocks P hP
      exact ⟨a, Subtype.ext ha.symm⟩⟩

Uses 4 · Used by 1

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · Two-block partition of three points

Used byEnumerating the proper noncrossing partitions of three points

DefinitionEnumerating the proper noncrossing partitions of three points#✓fully proved

Call a noncrossing partition of \(\{0, 1, 2\}\) proper if it is not the indiscrete one. Adjoin an extra element \(\ast\) to \(\{0, 1, 2\}\); this is the bijection from \(\{\ast, 0, 1, 2\}\) onto the set of proper noncrossing partitions of \(\{0, 1, 2\}\) that sends \(\ast\) to the discrete noncrossing partition and each \(a \in \{0, 1, 2\}\) to the noncrossing partition with blocks \(\{a\}\) and \(\{0, 1, 2\} \setminus \{a\}\).

NoncrossingPartition.properThreeEquiv · 60 lines

noncomputable def properThreeEquiv :
    Option (Fin 3) ≃ { P : NoncrossingPartition 3 // P ≠ indiscrete 3 } := by
  classical
  let optEquiv : Option (Fin 3) ≃ Unit ⊕ Fin 3 :=
    { toFun
      | none => Sum.inl ()
      | some a => Sum.inr a
      invFun
      | Sum.inl _ => none
      | Sum.inr a => some a
      left_inv := by
        intro o
        cases o <;> rfl
      right_inv := by
        intro s
        cases s with
        | inl u => cases u; rfl
        | inr _ => rfl }
  let discEquiv : Unit ≃ { P : NoncrossingPartition 3 // P = discrete 3 } :=
    { toFun _ := ⟨discrete 3, rfl⟩
      invFun _ := ()
      left_inv _ := rfl
      right_inv := fun ⟨P, hP⟩ => Subtype.ext hP.symm }
  have h_disj : Disjoint (fun P : NoncrossingPartition 3 => P = discrete 3)
                         (fun P => P.val.parts.card = 2) := by
    rw [Pi.disjoint_iff]
    intro P
    rw [Prop.disjoint_iff]
    rintro ⟨h1, h2⟩
    have h_disc : (discrete 3).val.parts.card = 3 := by
      rw [discrete_parts, Finset.card_map]
      simp
    have : P.val.parts.card = 3 := h1 ▸ h_disc
    omega
  have h_iff : ∀ P : NoncrossingPartition 3,
      (P = discrete 3 ∨ P.val.parts.card = 2) ↔ P ≠ indiscrete 3 := by
    intro P
    constructor
    · rintro (rfl | hcard) h_eq
      · exact discrete_three_ne_indiscrete_three h_eq
      · have h_ind_card : (indiscrete 3).val.parts.card = 1 := by
          rw [indiscrete_parts_pos (by decide)]
          simp
        have : P.val.parts.card = 1 := h_eq ▸ h_ind_card
        omega
    · intro h_ne
      have h_class := eq_discrete_or_indiscrete_or_twoBlock_three P
      rcases h_class with h_disc | h_ind | ⟨a, ha⟩
      · exact Or.inl h_disc
      · exact absurd h_ind h_ne
      · exact Or.inr (ha ▸ twoBlockPartition_parts_card a)
  let sumEquiv := discEquiv.sumCongr twoBlockEquiv
  let orSymm :=
    (subtypeOrEquiv (fun P : NoncrossingPartition 3 => P = discrete 3)
      (fun P => P.val.parts.card = 2) h_disj).symm
  let classEquiv :
      { P : NoncrossingPartition 3 // P = discrete 3 ∨ P.val.parts.card = 2 } ≃
        { P : NoncrossingPartition 3 // P ≠ indiscrete 3 } :=
    Equiv.subtypeEquivProp (funext fun P => propext (h_iff P))
  exact optEquiv.trans (sumEquiv.trans (orSymm.trans classEquiv))

Uses 12 · Used by 1

Statement usesNoncrossing partition · Noncrossing set partition · Set partition · Discrete noncrossing partition · The discrete noncrossing partition consists of the singletons · The discrete and indiscrete partitions of a three-element set differ · The discrete and indiscrete partitions of a two-element set differ · Classification of noncrossing partitions of a three-element set · The indiscrete noncrossing partition · The indiscrete partition of a nonempty set has a single block · Enumerating the two-block noncrossing partitions of three points · Two-block partition of three points

Used byNoncrossing partitions of a three-element set

TheoremNoncrossing partitions of a three-element set#✓fully proved

There are exactly five noncrossing partitions of \(\{0, 1, 2\}\).

@[simp]
theorem card_three : Fintype.card (NoncrossingPartition 3) = 5

Uses 6

Statement usesNoncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition

Proof usesThe indiscrete noncrossing partition · Enumerating the proper noncrossing partitions of three points

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.