diff --git a/ConNF/Base/Small.lean b/ConNF/Base/Small.lean index b07e82dc40..6fb93906ec 100644 --- a/ConNF/Base/Small.lean +++ b/ConNF/Base/Small.lean @@ -3,15 +3,10 @@ import ConNF.Background.Set import ConNF.Base.Params /-! -# Smallness +# Small sets In this file, we define the notion of a small set, and prove many of the basic properties of small sets. - -## Main declarations - -* `ConNF.Small`: A set is *small* if its cardinality is less than `#κ`. -* `ConNF.Near`: Two sets are *near* if their symmetric difference is small. -/ universe u v @@ -23,7 +18,7 @@ namespace ConNF variable [Params.{u}] {ι α β : Type _} {s t u : Set α} -/-- A set is *small* if its cardinality is less than `#κ`. -/ +/-- We say that a set is *small* if its cardinality is less than `#κ`. -/ def Small (s : Set α) : Prop := #s < #κ @@ -34,13 +29,16 @@ theorem Small.lt : Small s → #s < #κ := ## Criteria for smallness -/ +/-- Subsingletons are small. -/ theorem small_of_subsingleton (h : s.Subsingleton) : Small s := h.cardinalMk_le_one.trans_lt <| one_lt_aleph0.trans_le aleph0_lt_κ.le +/-- The empty set is small. -/ @[simp] theorem small_empty : Small (∅ : Set α) := small_of_subsingleton subsingleton_empty +/-- Singletons are small. -/ @[simp] theorem small_singleton (x : α) : Small {x} := small_of_subsingleton subsingleton_singleton @@ -49,25 +47,32 @@ theorem small_singleton (x : α) : Small {x} := theorem Small.mono (h : s ⊆ t) : Small t → Small s := (mk_le_mk_of_subset h).trans_lt +/-- If two sets are equal and one is small, then the other is small. -/ theorem Small.congr (h : s = t) : Small t → Small s := Small.mono (subset_of_eq h) -/-- Unions of small subsets are small. -/ +/-- Binary unions of small sets are small. -/ theorem small_union (hs : Small s) (ht : Small t) : Small (s ∪ t) := (mk_union_le _ _).trans_lt <| add_lt_of_lt Params.κ_isRegular.aleph0_le hs ht -/-- Unions of small subsets are small. -/ +/-- The *symmetric difference* of two small sets is small; recall that the symmetric difference +`s ∆ t` of two sets `s` and `t` is the union of their differences: `s ∆ t = s \ t ∪ t \ s`. -/ theorem small_symmDiff (hs : Small s) (ht : Small t) : Small (s ∆ t) := (small_union hs ht).mono symmDiff_subset_union +/-- An indexed union of sets is small if the index type is small and each set mentioned is small. -/ theorem small_iUnion (hι : #ι < #κ) {f : ι → Set α} (hf : ∀ i, Small (f i)) : Small (⋃ i, f i) := (mk_iUnion_le _).trans_lt <| mul_lt_of_lt Params.κ_isRegular.aleph0_le hι <| iSup_lt_of_isRegular Params.κ_isRegular hι hf +/-- It is occasionally useful to take an indexed union over the proofs of a proposition, for example +when taking a union over the elements of some set. In these cases, if the resulting set is small +for every proof, the union is also small. -/ theorem small_iUnion_Prop {p : Prop} {f : p → Set α} (hf : ∀ i, Small (f i)) : Small (⋃ i, f i) := by by_cases p <;> simp_all +/-- A small set-indexed union of sets is small. -/ theorem small_biUnion {s : Set ι} (hs : Small s) {f : ∀ i ∈ s, Set α} (hf : ∀ (i : ι) (hi : i ∈ s), Small (f i hi)) : Small (⋃ (i : ι) (hi : i ∈ s), f i hi) := (small_iUnion hs (λ i ↦ hf i i.prop)).congr (Set.biUnion_eq_iUnion _ _) @@ -80,13 +85,16 @@ 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 +/-- If a set is not small, its cardinality is larger than `#κ`. -/ theorem κ_le_of_not_small (h : ¬Small s) : #κ ≤ #s := by rwa [Small, not_lt] at h +/-- Initial segments of `κ` (excluding the endpoint) are small. -/ theorem iio_small (i : κ) : Small {j | j < i} := by have := Ordinal.type_Iio_lt i rwa [κ_type, lt_ord, Ordinal.card_type] at this +/-- Initial segments of `κ` (including the endpoint) are small. -/ theorem iic_small (i : κ) : Small {j | j ≤ i} := by have := Ordinal.type_Iic_lt i rwa [κ_type, lt_ord, Ordinal.card_type] at this @@ -95,13 +103,14 @@ theorem iic_small (i : κ) : Small {j | j ≤ i} := by ## Cardinality bounds on collections of small sets -/ -/-- The amount of small subsets of `α` is bounded below by the cardinality of `α`. -/ +/-- The amount of small subsets of any type `α` 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⟩) intro x y h exact singleton_injective <| congr_arg Subtype.val h -/-- There are at most `μ` small sets of a type at most as large as `μ`. -/ +/-- Because `μ` is a strong limit, +there are at most `μ` small subsets of a type at most as large as `μ`. -/ theorem card_small_le (h : #α ≤ #μ) : #{s : Set α | Small s} ≤ #μ := by rw [le_def] at h obtain ⟨⟨f, hf⟩⟩ := h @@ -111,7 +120,7 @@ theorem card_small_le (h : #α ≤ #μ) : #{s : Set α | Small s} ≤ #μ := by · intro s t h exact Subtype.val_injective <| hf.image_injective <| congr_arg Subtype.val h -/-- There are exactly `μ` small sets of a type of size `μ`. -/ +/-- There are exactly `μ` small subsets of any type `α` of size `μ`. -/ theorem card_small_eq (h : #α = #μ) : #{s : Set α | Small s} = #μ := by apply le_antisymm · exact card_small_le h.le @@ -119,8 +128,39 @@ theorem card_small_eq (h : #α = #μ) : #{s : Set α | Small s} = #μ := by /-! ## Small relations + +One of the crucial differences between this formalisation and previous iterations of the paper is +our extensive use of relational reasoning as opposed to function-based reasoning. This has some +technical advantages that should hopefully become clear over the course of this work. + +We will begin our study of relations by proving some smallness results for them, but we will first +establish some terminology that will be used throughout this document. + +The *domain* of a relation `r` is the set `{a | ∃ b, r a b}`. +The *codomain* of `r` is the set `{b | ∃ a, r a b}`. + +A relation `r` is called + +* *injective*, if `r a b` and `r a' b` imply `a = a'`; +* *surjective*, if for every `b`, there is some `a` such that `r a b`; +* *coinjective*, if `r a b'` and `r a b'` imply `b = b'`; +* *cosurjective*, if for every `a`, there is some `b` such that `r a b`; +* *one-to-one*, if `r` is both injective and coinjective; +* *functional*, if `r` is both coinjective and cosurjective + (so is a set-theoretic function); +* *cofunctional*, if `r` is both injective and surjective + (so is the converse of a set-theoretic function); +* *bijective*, if `r` is both functional and cofunctional; +* *permutative*, if `r` is one-to-one and its domain and codomain are equal. + +The *image* of a set `s` under a relation `r` is the set `{b | ∃ a ∈ s, r a b}`. +The *graph* of a relation `r` is the set `{(a, b) | r a b}`. +We can now state our results. -/ +/-- The image of any small set under a coinjective relation is small. +This is a generalisation of the fact that the image of a small set under a function (or functional +relation) is small. -/ theorem image_small_of_coinjective {r : Rel α β} (h : r.Coinjective) {s : Set α} (hs : Small s) : Small (r.image s) := by have := small_biUnion hs (f := λ x _ ↦ {y | r x y}) ?_ @@ -133,10 +173,13 @@ theorem image_small_of_coinjective {r : Rel α β} (h : r.Coinjective) {s : Set intro y hy z hz exact h.coinjective hy hz +/-- If the domain of a coinjective relation is small, then its codomain is also small. +This is a special case of the previous result. -/ theorem small_codom_of_small_dom {r : Rel α β} (h : r.Coinjective) (h' : Small r.dom) : Small r.codom := Rel.image_dom ▸ image_small_of_coinjective h h' +/-- If the domain and codomain of a relation are small, then its graph is also small. -/ 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}) ?_ @@ -154,29 +197,40 @@ theorem small_graph' {r : Rel α β} (h₁ : Small r.dom) (h₂ : Small r.codom) /-! ## Nearness + +Once we fix a notion of smallness, we can define an equivalence relation on sets of any type by +declaring that two sets are *near* each other if their symmetric difference is small. This notion +is used when defining *near-litters*, an important part of the ambient structure at the base type +level. -/ /-- Two sets are called *near* if their symmetric difference is small. -/ def Near (s t : Set α) : Prop := Small (s ∆ t) +/-! We establish the symbol `~` to denote nearness. -/ @[inherit_doc] infix:50 " ~ " => Near +/-- Nearness is reflexive. -/ @[refl] theorem near_refl (s : Set α) : s ~ s := by rw [Near, symmDiff_self] exact small_empty +/-- Like `near_refl`, but leaving all arguments implicit. -/ theorem near_rfl : s ~ s := near_refl s +/-- Equal sets are near. -/ theorem near_of_eq (h : s = t) : s ~ t := h ▸ near_refl s +/-- Nearness is symmetric. -/ @[symm] theorem near_symm (h : s ~ t) : t ~ s := by rwa [Near, symmDiff_comm] at h +/-- Nearness is transitive. -/ @[trans] theorem near_trans (h₁ : s ~ t) (h₂ : t ~ u) : s ~ u := (small_union h₁ h₂).mono (symmDiff_trans_subset s t u) @@ -184,9 +238,11 @@ theorem near_trans (h₁ : s ~ t) (h₂ : t ~ u) : s ~ u := instance {α : Type u} : Trans (Near : Set α → Set α → Prop) Near Near where trans := near_trans +/-- If `s` is small, then `s ∆ t` is near `t` for any `t`. -/ theorem near_symmDiff_self_of_small (h : Small s) : s ∆ t ~ t := by rwa [Near, symmDiff_symmDiff_cancel_right] +/-- If `s` is small, then `t ∪ s` is near `t` for any `t`. -/ theorem near_union_of_small (h : Small s) : t ∪ s ~ t := by simp only [Near, Set.symmDiff_def, union_diff_left] apply small_union @@ -194,9 +250,11 @@ theorem near_union_of_small (h : Small s) : t ∪ s ~ t := by · rw [show t \ (t ∪ s) = ∅ by aesop] exact small_empty +/-- Nearness is preserved under function application. -/ theorem near_image (h : s ~ t) (f : α → β) : f '' s ~ f '' t := (h.image f).mono subset_image_symmDiff +/-- Symmetric differences can be cancelled when comparing sets for nearness. -/ theorem near_symmDiff_iff (u : Set α) : u ∆ s ~ u ∆ t ↔ s ~ t := by rw [Near, Near, symmDiff_comm u s, symmDiff_assoc, symmDiff_symmDiff_cancel_left] @@ -215,6 +273,8 @@ theorem card_eq_of_near (h₁ : s ~ t) (h₂ : ¬Small t) : #s = #t := by have h₃ : ¬Small s := h₂ ∘ this.trans_lt exact le_antisymm (card_le_of_near (near_symm h₁) h₃) this +/-- If `s` and `t` are large and near each other, then their intersection has the same cardinality +as both `s` and `t`. -/ theorem card_inter_of_near (h₁ : s ~ t) (h₂ : ¬Small s) : #(s ∩ t : Set α) = #s := by apply le_antisymm · apply mk_le_of_injective (f := λ x ↦ ⟨x, x.prop.1⟩) @@ -225,16 +285,21 @@ theorem card_inter_of_near (h₁ : s ~ t) (h₂ : ¬Small s) : #(s ∩ t : Set · exact aleph0_lt_κ.le.trans (κ_le_of_not_small h₂) · exact h₁.trans_le (κ_le_of_not_small h₂) +/-- Any two large sets that are near each other must have nonempty intersection. -/ theorem inter_nonempty_of_near (h₁ : s ~ t) (h₂ : ¬Small s) : (s ∩ t).Nonempty := by rw [← mk_ne_zero_iff_nonempty, card_inter_of_near h₁ h₂] exact ne_of_gt <| aleph0_pos.trans <| aleph0_lt_κ.trans_le <| κ_le_of_not_small h₂ +/-- If `α` is any type with cardinality bounded by `μ`, then the amount of sets near a given set `s` +is also bounded by `μ`. -/ theorem card_near_le (s : Set α) (h : #α ≤ #μ) : #{t | t ~ s} ≤ #μ := by refine le_trans ?_ (card_small_le h) apply mk_le_of_injective (f := λ t ↦ ⟨t ∆ s, t.prop⟩) intro t₁ t₂ ht exact Subtype.val_injective <| symmDiff_left_injective s <| congr_arg Subtype.val ht +/-- If `α` is any type with cardinality exactly `μ`, then the amount of sets near a given set `s` +is precisely `μ`. -/ theorem card_near_eq (s : Set α) (h : #α = #μ) : #{t | t ~ s} = #μ := by refine trans ?_ (card_small_eq h) rw [Cardinal.eq]