|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Violeta Hernández Palacios |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.SetTheory.Cardinal.Cofinality.Basic |
| 9 | +public import Mathlib.SetTheory.Ordinal.Family |
| 10 | +public import Mathlib.SetTheory.Ordinal.Univ |
| 11 | + |
| 12 | +/-! |
| 13 | +# Enumerating a cofinal set |
| 14 | +
|
| 15 | +We define a typeclass `IsRegularCardinalOrder` for well-ordered types, whose order type equals (the |
| 16 | +initial ordinal of) their cofinality. This notion does not appear in the literature, but intends to |
| 17 | +generalize the properties of intervals `Iio c.ord`, wherever `c` is a regular cardinal. Other |
| 18 | +instances of this typeclass include `ℕ`, `Ordinal`, and `Cardinal`. |
| 19 | +
|
| 20 | +If `s` is a cofinal subset of a regular cardinal order `α`, there exists a unique order isomorphism |
| 21 | +`α ≃o s`, which we call `Order.enum`. When `α = Ordinal`, this is referred to as the enumerator |
| 22 | +function of the set. Note that if `α = ℕ`, then this definition matches `Nat.nth`. |
| 23 | +
|
| 24 | +## TODO |
| 25 | +
|
| 26 | +- Deprecate `Ordinal.enumOrd` in favor of `Order.enum`. |
| 27 | +- Prove that `Order.enum` on the naturals coincides with `Nat.nth`. |
| 28 | +-/ |
| 29 | + |
| 30 | +public section |
| 31 | + |
| 32 | +universe u |
| 33 | + |
| 34 | +open Cardinal Order Ordinal Set |
| 35 | + |
| 36 | +variable {α : Type*} |
| 37 | + |
| 38 | +/-- A typeclass which expresses that the order type of a well-order equals (the initial ordinal of) |
| 39 | +its cofinality. |
| 40 | +
|
| 41 | +If `α` is infinite, this implies that `α` is order isomorphic to `Iio c.ord` for some regular |
| 42 | +cardinal `c`. In the informal literature, one often says that `α` is a regular cardinal, by abuse |
| 43 | +of notation. -/ |
| 44 | +class IsRegularCardinalOrder (α : Type*) [LinearOrder α] [WellFoundedLT α] where |
| 45 | + type_lt_le_ord_cof : typeLT α ≤ (cof α).ord |
| 46 | + |
| 47 | +instance : IsRegularCardinalOrder ℕ := ⟨by simp⟩ |
| 48 | + |
| 49 | +instance (priority := low) [LinearOrder α] [WellFoundedLT α] [Subsingleton α] : |
| 50 | + IsRegularCardinalOrder α where |
| 51 | + type_lt_le_ord_cof := by |
| 52 | + cases isEmpty_or_nonempty α |
| 53 | + · simpa |
| 54 | + · cases nonempty_unique α |
| 55 | + have := BoundedOrder.ofUnique α |
| 56 | + simp |
| 57 | + |
| 58 | +instance : IsRegularCardinalOrder Ordinal where |
| 59 | + type_lt_le_ord_cof := by |
| 60 | + rw [type_lt_ordinal, ← ord_univ, ord_le_ord, le_cof_iff] |
| 61 | + intro s hs |
| 62 | + contrapose! hs |
| 63 | + rw [← Cardinal.lift_id (#s), ← small_iff_lift_mk_lt_univ] at hs |
| 64 | + rw [not_isCofinal_iff_bddAbove] |
| 65 | + exact Ordinal.bddAbove_of_small |
| 66 | + |
| 67 | +namespace Order |
| 68 | +variable [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] |
| 69 | + |
| 70 | +theorem ord_cof_eq_type_lt : (cof α).ord = typeLT α := by |
| 71 | + apply IsRegularCardinalOrder.type_lt_le_ord_cof.antisymm' |
| 72 | + rw [ord_le, card_type] |
| 73 | + exact cof_le_cardinalMk α |
| 74 | + |
| 75 | +@[simp] |
| 76 | +theorem cof_eq_cardinalMk : cof α = #α := by |
| 77 | + rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord] |
| 78 | + |
| 79 | +@[simp] |
| 80 | +theorem _root_.Cardinal.ord_cardinalMk : ord #α = typeLT α := by |
| 81 | + rw [← ord_cof_eq_type_lt, cof_eq_cardinalMk] |
| 82 | + |
| 83 | +theorem cof_ordinal : cof Ordinal.{u} = Cardinal.univ.{u, u + 1} := by |
| 84 | + simp |
| 85 | + |
| 86 | +theorem type_eq_of_isCofinal {s : Set α} (hs : IsCofinal s) : typeLT s = typeLT α := by |
| 87 | + apply (RelEmbedding.ofMonotone Subtype.val (by simp)).ordinal_type_le.antisymm |
| 88 | + rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk] |
| 89 | + exact cof_le hs |
| 90 | + |
| 91 | +/-- Enumerate the elements of a cofinal subset of `α` by `α` itself. This is a generalization of |
| 92 | +`Nat.nth`. -/ |
| 93 | +noncomputable def enum (s : Set α) (hs : IsCofinal s) : α ≃o s := |
| 94 | + .ofRelIsoLT (type_eq.1 (type_eq_of_isCofinal hs).symm).some |
| 95 | + |
| 96 | +theorem enum_le_of_forall_lt {a o : α} {s : Set α} {hs : IsCofinal s} (ho : o ∈ s) |
| 97 | + (H : ∀ b < a, enum s hs b < o) : enum s hs a ≤ o := by |
| 98 | + rw [← Subtype.coe_mk o ho, Subtype.coe_le_coe, ← OrderIso.le_symm_apply] |
| 99 | + apply le_of_forall_lt |
| 100 | + simpa [OrderIso.lt_symm_apply] |
| 101 | + |
| 102 | +theorem enum_succ_le_of_lt [SuccOrder α] {a o : α} {s : Set α} {hs : IsCofinal s} (ha : o ∈ s) |
| 103 | + (H : enum s hs a < o) : enum s hs (succ a) ≤ o := by |
| 104 | + refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_ |
| 105 | + simpa using le_of_lt_succ hb |
| 106 | + |
| 107 | +@[simp] |
| 108 | +theorem enum_univ (x : α) : enum univ .univ x = ⟨x, mem_univ x⟩ := by |
| 109 | + rw [← Subsingleton.allEq OrderIso.Set.univ.symm (enum univ .univ)] |
| 110 | + rfl |
| 111 | + |
| 112 | +end Order |
0 commit comments