Enumerations and their cardinality bounds

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

ConNF.lean

@@ -1,15 +1,16 @@
 import ConNF.Aux.Cardinal
 import ConNF.Aux.Ordinal
+import ConNF.Aux.Rel
 import ConNF.Aux.Set
 import ConNF.Aux.Transfer
 import ConNF.Aux.WellOrder
 import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm
+import ConNF.Setup.Enumeration
 import ConNF.Setup.Litter
 import ConNF.Setup.NearLitter
 import ConNF.Setup.Params
 import ConNF.Setup.Path
-import ConNF.Setup.Relation
 import ConNF.Setup.Small
 import ConNF.Setup.StrPerm
 import ConNF.Setup.StrSet

ConNF/Aux/Cardinal.lean

@@ -7,6 +7,7 @@ namespace Function
 
 open Cardinal
 
+/-- An alternate spelling of `Function.graph`, useful in proving inequalities of cardinals. -/
 def graph' {α β : Type _} (f : α → β) : Set (α × β) :=
   {(x, y) | y = f x}
 
@@ -28,6 +29,11 @@ end Function
 
 namespace Cardinal
 
+theorem mul_le_of_le {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a * b ≤ c := by
+  apply (mul_le_max a b).trans
+  rw [max_le_iff, max_le_iff]
+  exact ⟨⟨h1, h2⟩, hc⟩
+
 theorem lift_isRegular (c : Cardinal.{u}) (h : IsRegular c) : IsRegular (lift.{v} c) := by
   constructor
   · rw [← lift_aleph0.{v, u}, lift_le]

ConNF/Aux/Rel.lean

@@ -0,0 +1,58 @@
+import Mathlib.Data.Rel
+
+namespace Rel
+
+variable {α β : Type _}
+
+-- Note the backward composition style of Rel.comp!
+@[inherit_doc]
+scoped infixr:80 " • " => Rel.comp
+
+structure Injective (r : Rel α β) : Prop where
+  injective : ∀ ⦃x₁ x₂ y⦄, r x₁ y → r x₂ y → x₁ = x₂
+
+structure Coinjective (r : Rel α β) : Prop where
+  coinjective : ∀ ⦃x y₁ y₂⦄, r x y₁ → r x y₂ → y₁ = y₂
+
+structure Surjective (r : Rel α β) : Prop where
+  surjective : ∀ y, ∃ x, r x y
+
+structure Cosurjective (r : Rel α β) : Prop where
+  cosurjective : ∀ x, ∃ y, r x y
+
+structure Functional (r : Rel α β) extends r.Coinjective, r.Cosurjective : Prop
+
+structure Cofunctional (r : Rel α β) extends r.Injective, r.Surjective : Prop
+
+structure OneOne (r : Rel α β) extends r.Injective, r.Coinjective : Prop
+
+structure Bijective (r : Rel α β) extends r.Functional, r.Cofunctional : Prop
+
+structure DomEqCodom (r : Rel α α) : Prop where
+  dom_eq_codom : r.dom = r.codom
+
+structure Permutative (r : Rel α α) extends r.OneOne, r.DomEqCodom : Prop
+
+/-- An alternative spelling of `Rel.graph` that is useful for proving inequalities of cardinals. -/
+def graph' (r : Rel α β) : Set (α × β) :=
+  r.uncurry
+
+theorem le_of_graph'_subset {r s : Rel α β} (h : r.graph' ⊆ s.graph') :
+    r ≤ s :=
+  λ x y h' ↦ Set.mem_of_subset_of_mem (a := (x, y)) h h'
+
+theorem graph'_subset_of_le {r s : Rel α β} (h : r ≤ s) :
+    r.graph' ⊆ s.graph' :=
+  λ z ↦ h z.1 z.2
+
+theorem graph'_subset_iff {r s : Rel α β} :
+    r.graph' ⊆ s.graph' ↔ r ≤ s :=
+  ⟨le_of_graph'_subset, graph'_subset_of_le⟩
+
+theorem graph'_injective :
+    Function.Injective (Rel.graph' : Rel α β → Set (α × β)) :=
+  λ _ _ h ↦ le_antisymm (le_of_graph'_subset h.le) (le_of_graph'_subset h.symm.le)
+
+-- Compare Mathlib.Data.Rel and Mathlib.Logic.Relator.
+
+end Rel

ConNF/Setup/Enumeration.lean

@@ -0,0 +1,120 @@
+import ConNF.Aux.Rel
+import ConNF.Setup.Small
+
+/-!
+# Enumerations
+
+In this file, we define enumerations of a type.
+
+## Main declarations
+
+* `ConNF.Enumeration`: The type family of enumerations.
+-/
+
+universe u
+
+open Cardinal
+
+namespace ConNF
+
+variable [Params.{u}] {X : Type u}
+
+@[ext]
+structure Enumeration (X : Type u) where
+  bound : κ
+  rel : Rel κ X
+  lt_bound : ∀ i ∈ rel.dom, i < bound
+  rel_coinjective : rel.Coinjective
+
+namespace Enumeration
+
+variable {E F G : Enumeration X}
+
+instance : CoeTC (Enumeration X) (Set X) where
+  coe E := E.rel.codom
+
+instance : Membership X (Enumeration X) where
+  mem x E := x ∈ E.rel.codom
+
+theorem mem_iff (x : X) (E : Enumeration X) :
+    x ∈ E ↔ x ∈ E.rel.codom :=
+  Iff.rfl
+
+theorem dom_small (E : Enumeration X) :
+    Small E.rel.dom :=
+  (iio_small E.bound).mono E.lt_bound
+
+theorem coe_small (E : Enumeration X) :
+    Small (E : Set X) :=
+  small_codom_of_small_dom E.rel_coinjective E.dom_small
+
+theorem graph'_small (E : Enumeration X) :
+    Small E.rel.graph' :=
+  small_graph' E.dom_small E.coe_small
+
+noncomputable def singleton (x : X) : Enumeration X where
+  bound := 1
+  rel i y := i = 0 ∧ y = x
+  lt_bound i h := by
+    have : i = 0 := by simpa only [Rel.dom, exists_eq_right, Set.setOf_eq_eq_singleton,
+      Set.mem_singleton_iff] using h
+    rw [this, κEquiv_lt, ← Subtype.coe_lt_coe, κEquiv_ofNat, κEquiv_ofNat, Nat.cast_zero,
+      Nat.cast_one]
+    exact zero_lt_one
+  rel_coinjective := by
+    constructor
+    cc
+
+@[simp]
+theorem mem_singleton_iff (x y : X) :
+    y ∈ singleton x ↔ y = x := by
+  constructor
+  · rintro ⟨_, _, h⟩
+    exact h
+  · intro h
+    exact ⟨0, rfl, h⟩
+
+theorem singleton_injective : Function.Injective (singleton : X → Enumeration X) := by
+  intro x y h
+  have := mem_singleton_iff y x
+  rw [← h, mem_singleton_iff] at this
+  exact this.mp rfl
+
+/-!
+## Cardinality bounds on enumerations
+-/
+
+theorem card_enumeration_ge (X : Type u) : #X ≤ #(Enumeration X) :=
+  mk_le_of_injective singleton_injective
+
+def enumerationEmbedding (X : Type u) : Enumeration X ↪ κ × {s : Set (κ × X) | Small s} where
+  toFun E := (E.bound, ⟨E.rel.graph', E.graph'_small⟩)
+  inj' := by
+    intro E F h
+    rw [Prod.mk.injEq, Subtype.mk.injEq] at h
+    exact Enumeration.ext h.1 (Rel.graph'_injective h.2)
+
+theorem card_enumeration_le (h : #X ≤ #μ) : #(Enumeration X) ≤ #μ := by
+  apply (mk_le_of_injective (enumerationEmbedding X).injective).trans
+  rw [mk_prod, lift_id, lift_id]
+  apply mul_le_of_le aleph0_lt_μ.le κ_le_μ
+  apply card_small_le
+  rw [mk_prod, lift_id, lift_id]
+  exact mul_le_of_le aleph0_lt_μ.le κ_le_μ h
+
+theorem card_enumeration_lt (h : #X < #μ) : #(Enumeration X) < #μ := by
+  apply (mk_le_of_injective (enumerationEmbedding X).injective).trans_lt
+  rw [mk_prod, lift_id, lift_id]
+  apply mul_lt_of_lt aleph0_lt_μ.le κ_lt_μ
+  apply (mk_subtype_le _).trans_lt
+  rw [mk_set]
+  apply μ_isStrongLimit.2
+  rw [mk_prod, lift_id, lift_id]
+  exact mul_lt_of_lt aleph0_lt_μ.le κ_lt_μ h
+
+theorem card_enumeration_eq (h : #X = #μ) : #(Enumeration X) = #μ :=
+  le_antisymm (card_enumeration_le h.le) (h.symm.le.trans (card_enumeration_ge X))
+
+end Enumeration
+
+end ConNF

ConNF/Setup/Params.lean

@@ -207,4 +207,12 @@ theorem κEquiv_sub (x y : κ) :
   rw [κ_sub_def, Equiv.apply_symm_apply]
   rfl
 
+theorem κEquiv_lt (x y : κ) :
+    x < y ↔ κEquiv x < κEquiv y :=
+  Iff.rfl
+
+theorem κEquiv_le (x y : κ) :
+    x ≤ y ↔ κEquiv x ≤ κEquiv y :=
+  Iff.rfl
+
 end ConNF

ConNF/Setup/Small.lean

@@ -1,3 +1,4 @@
+import ConNF.Aux.Rel
 import ConNF.Aux.Set
 import ConNF.Setup.Params
 
@@ -13,8 +14,7 @@ sets.
 * `ConNF.Near`: Two sets are *near* if their symmetric difference is small.
 -/
 
-noncomputable section
-universe u
+universe u v
 
 open Cardinal Set
 open scoped symmDiff
@@ -80,6 +80,21 @@ theorem Small.image (f : α → β) : Small s → Small (f '' s) :=
 theorem Small.preimage (f : β → α) (h : f.Injective) : Small s → Small (f ⁻¹' s) :=
   (mk_preimage_of_injective f s h).trans_lt
 
+theorem κ_le_of_not_small (h : ¬Small s) : #κ ≤ #s := by
+  rwa [Small, not_lt] at h
+
+theorem iio_small (i : κ) : Small {j | j < i} := by
+  have := Ordinal.type_Iio_lt i
+  rwa [κ_type, lt_ord, Ordinal.card_type] at this
+
+theorem iic_small (i : κ) : Small {j | j ≤ i} := by
+  have := Ordinal.type_Iic_lt i
+  rwa [κ_type, lt_ord, Ordinal.card_type] at this
+
+/-!
+## Cardinality bounds on collections of small sets
+-/
+
 /-- The amount of small subsets of `α` is bounded below by the cardinality of `α`. -/
 theorem card_le_card_small (α : Type _) : #α ≤ #{s : Set α | Small s} := by
   apply mk_le_of_injective (f := λ x ↦ ⟨{x}, small_singleton x⟩)
@@ -102,8 +117,40 @@ theorem card_small_eq (h : #α = #μ) : #{s : Set α | Small s} = #μ := by
   · exact card_small_le h.le
   · exact h.symm.trans_le <| card_le_card_small α
 
-theorem κ_le_of_not_small (h : ¬Small s) : #κ ≤ #s := by
-  rwa [Small, not_lt] at h
+/-!
+## Small relations
+-/
+
+theorem small_codom_of_small_dom {r : Rel α β} (h : r.Coinjective) (h' : Small r.dom) :
+    Small r.codom := by
+  have := small_biUnion h' (f := λ x _ ↦ {y | r x y}) ?_
+  · apply this.mono
+    rintro y ⟨x, hxy⟩
+    simp only [mem_iUnion]
+    exact ⟨x, ⟨y, hxy⟩, hxy⟩
+  · intro x hx
+    apply small_of_subsingleton
+    intro y hy z hz
+    exact h.coinjective hy hz
+
+theorem small_graph' {r : Rel α β} (h₁ : Small r.dom) (h₂ : Small r.codom) :
+    Small r.graph' := by
+  have := small_biUnion h₁ (f := λ x _ ↦ {z : α × β | z.1 = x ∧ r x z.2}) ?_
+  · apply this.mono
+    rintro z hz
+    simp only [mem_iUnion]
+    exact ⟨z.1, ⟨z.2, hz⟩, rfl, hz⟩
+  · intro x hx
+    apply (h₂.image (λ y ↦ (x, y))).mono
+    rintro ⟨x', y⟩ hy
+    rw [mem_setOf_eq] at hy
+    cases hy.1
+    rw [mem_image]
+    exact ⟨y, ⟨x', hy.2⟩, rfl⟩
+
+/-!
+## Nearness
+-/
 
 /-- Two sets are called *near* if their symmetric difference is small. -/
 def Near (s t : Set α) : Prop :=

blueprint/src/chapters/environment.tex

@@ -211,6 +211,7 @@ \section{The structural hierarchy}
 \begin{definition}[enumeration]
   \label{def:Enumeration}
   \uses{def:Small}
+  \lean{ConNF.Enumeration}
   Let \( \tau \) be a type.
   An \emph{enumeration} of \( \tau \) is a pair \( E = (i, f) \) where \( i : \kappa \) and \( f \) is a partial function \( \kappa \to \tau \), such that all domain elements of \( f \) are strictly less than \( i \).\footnote{This should be encoded as a coinjective relation \( \kappa \to \tau \to \Prop \); see \cref{def:relation_props}.}
   If \( x : \tau \), we write \( x \in E \) for \( x \in \ran f \).