Mathlib.Data.Fintype.Sort

Module docstring

{"# Sorting a finite type

This file provides two equivalences for linearly ordered fintypes: * monoEquivOfFin: Order isomorphism between α and Fin (card α). * finSumEquivOfFinset: Equivalence between α and Fin m ⊕ Fin n where m and n are respectively the cardinalities of some Finset α and its complement. "}

monoEquivOfFin definition

(α : Type*) [Fintype α] [LinearOrder α] {k : ℕ} (h : Fintype.card α = k) : Fin k ≃o α

Full source

/-- Given a linearly ordered fintype `α` of cardinal `k`, the order isomorphism
`monoEquivOfFin α h` is the increasing bijection between `Fin k` and `α`. Here, `h` is a proof
that the cardinality of `α` is `k`. We use this instead of an isomorphism `Fin (card α) ≃o α` to
avoid casting issues in further uses of this function. -/
def monoEquivOfFin (α : Type*) [Fintype α] [LinearOrder α] {k : ℕ} (h : Fintype.card α = k) :
    FinFin k ≃o α :=
  (univ.orderIsoOfFin h).trans <| (OrderIso.setCongr _ _ coe_univ).trans OrderIso.Set.univ

Order isomorphism between a finite linearly ordered type and its enumeration as Fin k

Informal description

Given a finite type $\alpha$ with a linear order and cardinality $k$, the order isomorphism $\text{monoEquivOfFin}$ is the increasing bijection between $\text{Fin}\,k$ (the canonical type with $k$ elements) and $\alpha$. Here, $h$ is a proof that the cardinality of $\alpha$ is $k$. This is constructed by: 1. Creating an order isomorphism between the universal finite set of $\alpha$ and $\text{Fin}\,k$ using $\text{orderIsoOfFin}$ (which enumerates elements in order) 2. Transporting this through the equality between the universal finite set and the universal set of $\alpha$ 3. Composing with the natural order isomorphism between the universal set and $\alpha$ itself

finSumEquivOfFinset definition

(hm : #s = m) (hn : #sᶜ = n) : Fin m ⊕ Fin n ≃ α

Full source

/-- If `α` is a linearly ordered fintype, `s : Finset α` has cardinality `m` and its complement has
cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of `Fin m` to
elements of `s` and elements of `Fin n` to elements of `sᶜ` while preserving order on each
"half" of `Fin m ⊕ Fin n` (using `Set.orderIsoOfFin`). -/
def finSumEquivOfFinset (hm : #s = m) (hn : #sᶜ = n) : FinFin m ⊕ Fin nFin m ⊕ Fin n ≃ α :=
  calc
    Fin m ⊕ Fin n ≃ (s : Set α) ⊕ (sᶜ : Set α) :=
      Equiv.sumCongr (s.orderIsoOfFin hm).toEquiv <|
        (sᶜ.orderIsoOfFin hn).toEquiv.trans <| Equiv.setCongr s.coe_compl
    _ ≃ α := Equiv.Set.sumCompl _

Order-preserving equivalence between a finite type and the sum of its subset and complement

Informal description

Given a finite type $\alpha$ with a linear order and a subset $s \subseteq \alpha$ with cardinality $m$ (witnessed by $hm$) and complement $s^c$ with cardinality $n$ (witnessed by $hn$), the equivalence $\text{finSumEquivOfFinset}$ is a bijection between the disjoint union $\text{Fin}\,m \oplus \text{Fin}\,n$ and $\alpha$. This equivalence maps elements of $\text{Fin}\,m$ (left summand) to elements of $s$ and elements of $\text{Fin}\,n$ (right summand) to elements of $s^c$, preserving the order on each component via the order isomorphisms $\text{orderIsoOfFin}$ for $s$ and $s^c$.

finSumEquivOfFinset_inl theorem

(hm : #s = m) (hn : #sᶜ = n) (i : Fin m) : finSumEquivOfFinset hm hn (Sum.inl i) = s.orderEmbOfFin hm i

Full source

@[simp]
theorem finSumEquivOfFinset_inl (hm : #s = m) (hn : #sᶜ = n) (i : Fin m) :
    finSumEquivOfFinset hm hn (Sum.inl i) = s.orderEmbOfFin hm i :=
  rfl

Left Inclusion Maps to Ordered Subset Element via finSumEquivOfFinset

Informal description

Given a finite linearly ordered type $\alpha$ with a subset $s \subseteq \alpha$ of cardinality $m$ (witnessed by $hm$) and complement $s^c$ of cardinality $n$ (witnessed by $hn$), the left inclusion $\text{Sum.inl}\,i$ of an element $i \in \text{Fin}\,m$ under the equivalence $\text{finSumEquivOfFinset}$ maps to the $i$-th element of $s$ under the order embedding $\text{orderEmbOfFin}$.

finSumEquivOfFinset_inr theorem

(hm : #s = m) (hn : #sᶜ = n) (i : Fin n) : finSumEquivOfFinset hm hn (Sum.inr i) = sᶜ.orderEmbOfFin hn i

Full source

@[simp]
theorem finSumEquivOfFinset_inr (hm : #s = m) (hn : #sᶜ = n) (i : Fin n) :
    finSumEquivOfFinset hm hn (Sum.inr i) = sᶜ.orderEmbOfFin hn i :=
  rfl

Right Component of Order-Preserving Equivalence Maps to Complement

Informal description

Given a finite type $\alpha$ with a linear order and a subset $s \subseteq \alpha$ with cardinality $m$ (witnessed by $hm$) and complement $s^c$ with cardinality $n$ (witnessed by $hn$), the right component of the equivalence $\text{finSumEquivOfFinset}$ maps an element $i \in \text{Fin}\,n$ to the $i$-th element of $s^c$ under the order isomorphism $\text{orderEmbOfFin}$ for $s^c$. In other words, for any $i \in \text{Fin}\,n$, we have: \[ \text{finSumEquivOfFinset}\,hm\,hn\,(\text{Sum.inr}\,i) = \text{orderEmbOfFin}\,s^c\,hn\,i \]