Non-cofinality of type indices in mu

Signed-off-by: zeramorphic <[email protected]>

ConNF/Aux/Ordinal.lean

@@ -8,21 +8,7 @@ open Cardinal
 
 namespace Ordinal
 
-theorem card_Iio (o : Ordinal.{u}) : #(Set.Iio o) = Cardinal.lift.{u + 1} o.card := by
-  rw [Cardinal.eq.mpr ⟨o.enumIsoOut.toEquiv.trans Equiv.ulift.{u + 1, u}.symm⟩,
-    mk_uLift, mk_ordinal_out, lift_card]
-
-instance {o : Ordinal.{u}} : LtWellOrder (Set.Iio o) where
-
-theorem type_Iio (o : Ordinal.{u}) :
-    type ((· < ·) : Set.Iio o → Set.Iio o → Prop) = lift.{u + 1} o := by
-  have := Ordinal.lift_type_eq.{u + 1, u, u + 1}
-    (r := ((· < ·) : Set.Iio o → Set.Iio o → Prop)) (s := o.out.r)
-  rw [lift_id, type_out] at this
-  rw [this]
-  exact ⟨o.enumIsoOut.toRelIsoLT⟩
-
-def withBot_orderIso {α : Type u} [Preorder α] [IsWellOrder α (· < ·)] :
+def withBotOrderIso {α : Type u} [Preorder α] [IsWellOrder α (· < ·)] :
     ((· < ·) : WithBot α → WithBot α → Prop) ≃r
       Sum.Lex (EmptyRelation (α := PUnit)) ((· < ·) : α → α → Prop) where
   toFun := WithBot.recBotCoe (Sum.inl PUnit.unit) Sum.inr
@@ -39,7 +25,7 @@ theorem type_withBot {α : Type u} [Preorder α] [IsWellOrder α (· < ·)] :
     type ((· < ·) : WithBot α → WithBot α → Prop) = 1 + type ((· < ·) : α → α → Prop) := by
   change _ = type EmptyRelation + _
   rw [← type_sum_lex, type_eq]
-  exact ⟨withBot_orderIso⟩
+  exact ⟨withBotOrderIso⟩
 
 theorem noMaxOrder_of_isLimit {α : Type u} [Preorder α] [IsWellOrder α (· < ·)]
     (h : (type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
@@ -66,6 +52,69 @@ theorem isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWell
     (type ((· < ·) : α → α → Prop)).IsLimit ↔ NoMaxOrder α :=
   ⟨noMaxOrder_of_isLimit, isLimit_of_noMaxOrder⟩
 
+theorem type_Iio_lt {α : Type u} [LtWellOrder α] (x : α) :
+    type (Subrel ((· < ·) : α → α → Prop) (Set.Iio x)) < type ((· < ·) : α → α → Prop) :=
+  typein_lt_type _ x
+
+def iicOrderIso {α : Type u} [LtWellOrder α] (x : α) :
+    (Subrel ((· < ·) : α → α → Prop) (Set.Iic x)) ≃r
+      Sum.Lex (Subrel ((· < ·) : α → α → Prop) (Set.Iio x)) (EmptyRelation (α := PUnit)) where
+  toFun y := if h : y = x then Sum.inr PUnit.unit else Sum.inl ⟨y, y.prop.lt_of_ne h⟩
+  invFun := Sum.elim (λ y ↦ ⟨y, y.prop.le⟩) (λ _ ↦ ⟨x, le_rfl⟩)
+  left_inv y := by aesop
+  right_inv y := by
+    dsimp only
+    split_ifs with h
+    · cases y with
+      | inl y => rw [Sum.elim_inl] at h; cases ne_of_lt y.prop h
+      | inr y => rfl
+    · cases y with
+      | inl y => rfl
+      | inr y => simp only [Sum.elim_inr, not_true_eq_false] at h
+  map_rel_iff' {y z} := by
+    simp only [Equiv.coe_fn_mk, subrel_val, Subtype.coe_lt_coe]
+    split_ifs with h h' h'
+    · rw [Sum.lex_inr_inr, empty_relation_apply, false_iff, not_lt,
+        Subtype.coe_injective (h.trans h'.symm)]
+    · simp only [Sum.lex_inr_inl, false_iff, not_lt, ← Subtype.coe_le_coe, h]
+      exact z.prop
+    · simp only [Sum.Lex.sep, true_iff]
+      rw [← Subtype.coe_lt_coe]
+      exact lt_of_le_of_ne (y.prop.trans_eq h'.symm) (h'.trans_ne (Ne.symm h)).symm
+    · simp only [Sum.lex_inl_inl, subrel_val, Subtype.coe_lt_coe]
+
+theorem type_Iic_eq {α : Type u} [LtWellOrder α] (x : α) :
+    type (Subrel ((· < ·) : α → α → Prop) (Set.Iic x)) =
+    type (Subrel ((· < ·) : α → α → Prop) (Set.Iio x)) + 1 := by
+  change _ = _ + type EmptyRelation
+  rw [← type_sum_lex, type_eq]
+  exact ⟨iicOrderIso x⟩
+
+theorem type_Iic_lt {α : Type u} [LtWellOrder α] [NoMaxOrder α] (x : α) :
+    type (Subrel ((· < ·) : α → α → Prop) (Set.Iic x)) < type ((· < ·) : α → α → Prop) := by
+  rw [type_Iic_eq]
+  haveI : Nonempty α := ⟨x⟩
+  have h := isLimit_of_noMaxOrder (inferInstanceAs (NoMaxOrder α))
+  exact h.right _ (type_Iio_lt x)
+
+/-!
+## The additive structure on the set of ordinals below a cardinal
+-/
+
+theorem card_Iio (o : Ordinal.{u}) : #(Set.Iio o) = Cardinal.lift.{u + 1} o.card := by
+  rw [Cardinal.eq.mpr ⟨o.enumIsoOut.toEquiv.trans Equiv.ulift.{u + 1, u}.symm⟩,
+    mk_uLift, mk_ordinal_out, lift_card]
+
+instance {o : Ordinal.{u}} : LtWellOrder (Set.Iio o) where
+
+theorem type_Iio (o : Ordinal.{u}) :
+    type ((· < ·) : Set.Iio o → Set.Iio o → Prop) = lift.{u + 1} o := by
+  have := Ordinal.lift_type_eq.{u + 1, u, u + 1}
+    (r := ((· < ·) : Set.Iio o → Set.Iio o → Prop)) (s := o.out.r)
+  rw [lift_id, type_out] at this
+  rw [this]
+  exact ⟨o.enumIsoOut.toRelIsoLT⟩
+
 variable {c : Cardinal.{u}} (h : ℵ₀ ≤ c)
 
 theorem add_lt_ord (h : ℵ₀ ≤ c) {x y : Ordinal.{u}}
@@ -110,4 +159,26 @@ def iioAddMonoid : AddMonoid (Set.Iio c.ord) where
   __ := iioAdd h
   __ := iioZero h
 
+theorem nat_lt_ord (h : ℵ₀ ≤ c) (n : ℕ) : n < c.ord := by
+  apply (nat_lt_omega n).trans_le
+  apply ord_mono at h
+  rwa [ord_aleph0] at h
+
+def iioOfNat (n : ℕ) : OfNat (Set.Iio c.ord) n where
+  ofNat := ⟨n, nat_lt_ord h n⟩
+
+theorem iioOfNat_coe (n : ℕ) :
+    letI := iioOfNat h
+    ((OfNat.ofNat n : Set.Iio c.ord) : Ordinal) = n :=
+  rfl
+
+theorem iio_noMaxOrder (h : ℵ₀ ≤ c) : NoMaxOrder (Set.Iio c.ord) := by
+  letI := iioAdd h
+  letI := iioOfNat h
+  constructor
+  intro x
+  use x + 1
+  rw [← Subtype.coe_lt_coe, iioAdd_def, lt_add_iff_pos_right, iioOfNat_coe, Nat.cast_one]
+  exact zero_lt_one
+
 end Ordinal

ConNF/Aux/Transfer.lean

@@ -123,6 +123,20 @@ theorem ltWellOrder_type [LtWellOrder β] :
   rw [Ordinal.lift_type_eq.{u, v, max u v}]
   exact ⟨e.ltIso⟩
 
+protected theorem noMaxOrder [LT β] [NoMaxOrder β] :
+    letI := e.lt
+    NoMaxOrder α := by
+  letI := e.lt
+  constructor
+  intro x
+  obtain ⟨y, hy⟩ := exists_gt (e x)
+  use e.symm y
+  rw [lt_def, apply_symm_apply]
+  exact hy
+
+protected def ofNat (n : ℕ) [OfNat β n] : OfNat α n where
+  ofNat := e.symm (OfNat.ofNat n)
+
 theorem apply_add [Add β] (x y : α) :
     letI := e.add
     e (x + y) = e x + e y := by

ConNF/Setup/Params.lean

@@ -33,7 +33,7 @@ class Params where
   μ_isStrongLimit : (#μ).IsStrongLimit
   κ_lt_μ : #κ < #μ
   κ_le_cof_μ : #κ ≤ (#μ).ord.cof
-  Λ_le_cof_μ : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord.cof.ord
+  Λ_type_le_cof_μ : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord.cof.ord
 
 def minimalParams : Params where
   Λ := ℕ
@@ -57,7 +57,7 @@ def minimalParams : Params where
     rw [mk_out, mk_out]
     have := beth_normal.cof_le (aleph 1).ord
     rwa [isRegular_aleph_one.cof_eq] at this
-  Λ_le_cof_μ := by
+  Λ_type_le_cof_μ := by
     rw [type_nat_lt, mk_out]
     have := beth_normal.cof_le (aleph 1).ord
     rw [isRegular_aleph_one.cof_eq, ← ord_le_ord] at this
@@ -92,11 +92,11 @@ def inaccessibleParams.{v} : Params where
   κ_le_cof_μ := by
     rw [mk_uLift, mk_out, mk_out, univ_inaccessible.2.1.cof_eq]
     exact (lift_lt_univ _).le
-  Λ_le_cof_μ := by
+  Λ_type_le_cof_μ := by
     change type (Cardinal.univ.{v, v + 1}).ord.out.r ≤ _
     rw [type_out, mk_out, univ_inaccessible.2.1.cof_eq]
 
-export Params (Λ κ μ aleph0_lt_κ κ_isRegular μ_isStrongLimit κ_lt_μ κ_le_cof_μ Λ_le_cof_μ)
+export Params (Λ κ μ aleph0_lt_κ κ_isRegular μ_isStrongLimit κ_lt_μ κ_le_cof_μ Λ_type_le_cof_μ)
 
 variable [Params.{u}]
 
@@ -107,8 +107,8 @@ instance : NoMaxOrder Λ := Params.Λ_noMaxOrder
 theorem aleph0_lt_μ : ℵ₀ < #μ :=
   aleph0_lt_κ.trans κ_lt_μ
 
-theorem type_Λ_le_μ_ord : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord :=
-  Λ_le_cof_μ.trans <| ord_cof_le (#μ).ord
+theorem Λ_type_le_μ_ord : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord :=
+  Λ_type_le_cof_μ.trans <| ord_cof_le (#μ).ord
 
 @[irreducible]
 def κEquiv : κ ≃ Set.Iio (#κ).ord := by
@@ -123,7 +123,17 @@ def μEquiv : μ ≃ Set.Iio (#μ).ord := by
   rw [← Cardinal.eq, mk_uLift, card_Iio, card_ord]
 
 instance : LtWellOrder κ := Equiv.ltWellOrder κEquiv
+instance (n : ℕ) : OfNat κ n :=
+  letI := iioOfNat aleph0_lt_κ.le n
+  Equiv.ofNat κEquiv n
+instance : NoMaxOrder κ :=
+  letI := iio_noMaxOrder aleph0_lt_κ.le
+  Equiv.noMaxOrder κEquiv
+
 instance : LtWellOrder μ := Equiv.ltWellOrder μEquiv
+instance : NoMaxOrder μ :=
+  letI := iio_noMaxOrder aleph0_lt_μ.le
+  Equiv.noMaxOrder μEquiv
 
 instance : Infinite Λ := NoMaxOrder.infinite
 instance : Infinite κ := by rw [infinite_iff]; exact aleph0_lt_κ.le
@@ -151,6 +161,11 @@ instance : Sub κ :=
   letI := iioSub (#κ).ord
   Equiv.sub κEquiv
 
+theorem κ_ofNat_def (n : ℕ) :
+    letI := iioOfNat aleph0_lt_κ.le n
+    OfNat.ofNat n = κEquiv.symm (OfNat.ofNat n) :=
+  rfl
+
 theorem κ_add_def (x y : κ) :
     letI := iioAddMonoid aleph0_lt_κ.le
     x + y = κEquiv.symm (κEquiv x + κEquiv y) :=
@@ -161,6 +176,11 @@ theorem κ_sub_def (x y : κ) :
     x - y = κEquiv.symm (κEquiv x - κEquiv y) :=
   rfl
 
+theorem κEquiv_ofNat (n : ℕ) :
+    (κEquiv (OfNat.ofNat n) : Ordinal) = n := by
+  rw [κ_ofNat_def, Equiv.apply_symm_apply]
+  rfl
+
 theorem κEquiv_add (x y : κ) :
     (κEquiv (x + y) : Ordinal) = (κEquiv x : Ordinal) + κEquiv y := by
   rw [κ_add_def, Equiv.apply_symm_apply]

ConNF/Setup/TypeIndex.lean

@@ -37,4 +37,20 @@ protected theorem TypeIndex.card :
   have := congr_arg Ordinal.card TypeIndex.type
   rwa [card_type, card_type] at this
 
+theorem Λ_card_Iio_lt (α : Λ) : #{β | β < α} < (#μ).ord.cof := by
+  have := (type_Iio_lt α).trans_le Λ_type_le_cof_μ
+  rwa [lt_ord] at this
+
+theorem Λ_card_Iic_lt (α : Λ) : #{β | β ≤ α} < (#μ).ord.cof := by
+  have := (type_Iic_lt α).trans_le Λ_type_le_cof_μ
+  rwa [lt_ord] at this
+
+theorem TypeIndex.card_Iio_lt (α : TypeIndex) : #{β | β < α} < (#μ).ord.cof := by
+  have := ((type_Iio_lt α).trans_eq TypeIndex.type).trans_le Λ_type_le_cof_μ
+  rwa [lt_ord] at this
+
+theorem TypeIndex.card_Iic_lt (α : TypeIndex) : #{β | β ≤ α} < (#μ).ord.cof := by
+  have := ((type_Iic_lt α).trans_eq TypeIndex.type).trans_le Λ_type_le_cof_μ
+  rwa [lt_ord] at this
+
 end ConNF