Litters and atoms

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

ConNF.lean

@@ -2,6 +2,8 @@ import ConNF.Aux.Cardinal
 import ConNF.Aux.Ordinal
 import ConNF.Aux.Transfer
 import ConNF.Aux.WellOrder
+import ConNF.Setup.Atom
+import ConNF.Setup.Litter
 import ConNF.Setup.Params
 import ConNF.Setup.Path
 import ConNF.Setup.Small

ConNF/Setup/Atom.lean

@@ -0,0 +1,90 @@
+import ConNF.Setup.Litter
+
+/-!
+# Atoms
+
+In this file, we define atoms: the elements of the base type of our model. They are not atoms in the
+ZFU sense (for example), they are simply the elements of the model which are in type `⊥`.
+
+This base type does not appear in the final construction, it is just used as the foundation on which
+the subsequent layers can be built.
+
+## Main declarations
+
+* `ConNF.Atom`: The type of atoms.
+-/
+
+universe u
+
+open Cardinal Set
+
+namespace ConNF
+
+variable [Params.{u}]
+
+/--
+The base type of the construction, denoted by `τ₋₁` in various papers. Instead of declaring it as an
+arbitrary type of cardinality `μ` and partitioning it into suitable sets of litters afterwards, we
+define it as `Litter × κ`, which has the correct cardinality and comes with a natural partition.
+
+These are not 'atoms' in the ZFU, TTTU or NFU sense; they are simply the elements of the model which
+are in type `τ₋₁`.
+-/
+structure Atom : Type u where
+  litter : Litter
+  index : κ
+
+instance : ToLitter Atom where
+  toLitter := Atom.litter
+
+/-- The set of atoms corresponding to litter `L`. -/
+def litterSet (L : Litter) : Set Atom :=
+  {a | a° = L}
+
+@[inherit_doc] postfix:75 "ᴬ" => litterSet
+
+@[simp]
+theorem mem_litterSet_iff (a : Atom) (L : Litter) :
+    a ∈ Lᴬ ↔ a° = L :=
+  Iff.rfl
+
+@[ext]
+theorem Atom.ext {a₁ a₂ : Atom} (h : a₁° = a₂°) (h' : a₁.index = a₂.index) : a₁ = a₂ := by
+  obtain ⟨L₁, i₁⟩ := a₁
+  obtain ⟨L₂, i₂⟩ := a₂
+  subst h
+  subst h'
+  rfl
+
+/-- Strips away the name of the type of atoms, converting it into a combination of types
+well-known to mathlib. -/
+def atomEquiv : Atom ≃ Litter × κ
+    where
+  toFun a := (a°, a.index)
+  invFun a := ⟨a.1, a.2⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The cardinality of `Atom` is the cardinality of `μ`.
+We will prove that all types constructed in our model have cardinality equal to `μ`. -/
+@[simp]
+theorem card_atom : #Atom = #μ := by
+  rw [atomEquiv.cardinal_eq, mk_prod, lift_id, lift_id, card_litter]
+  exact mul_eq_left aleph0_lt_μ.le κ_le_μ (mk_ne_zero κ)
+
+/-- Each litter set is equivalent as a type to `κ`. -/
+def litterSetEquiv (L : Litter) : Lᴬ ≃ κ where
+  toFun a := a.val.index
+  invFun i := ⟨⟨L, i⟩, rfl⟩
+  left_inv x := Subtype.ext <| Atom.ext x.prop.symm rfl
+  right_inv _ := rfl
+
+/-- Each litter set has cardinality `κ`. -/
+@[simp]
+theorem mk_litterSet (L : Litter) : #(Lᴬ) = #κ :=
+  Cardinal.eq.mpr ⟨litterSetEquiv L⟩
+
+instance (L : Litter) : Nonempty (Lᴬ) :=
+  ⟨⟨L, Classical.arbitrary κ⟩, rfl⟩
+
+end ConNF

ConNF/Setup/Litter.lean

@@ -0,0 +1,64 @@
+import ConNF.Setup.TypeIndex
+
+/-!
+# Litters
+
+In this file, we define litters, which are the parts of an indexed partition of the base type of our
+model. Each litter is indexed by an element of `μ`, as well as some parameters `β` and `γ` used for
+defining the `fuzz` map later.
+
+## Main declarations
+
+* `ConNF.Litter`: The type of litters.
+-/
+
+universe u
+
+open Cardinal WithBot
+
+namespace ConNF
+
+variable [Params.{u}]
+
+/-- The type indexing the partition of `ConNF.Atom`. Each atom belongs to a unique litter.
+The field `ν : μ` is an index that enforces that there are `μ` litters.
+The fields `β` and `γ` are used in the definition of the `fuzz` map, which is an injection
+into the type of litters. -/
+structure Litter where
+  ν : μ
+  β : TypeIndex
+  γ : Λ
+  β_ne_γ : β ≠ γ
+
+instance : Nonempty Litter :=
+  ⟨⟨Classical.arbitrary μ, ⊥, Classical.arbitrary Λ, bot_ne_coe⟩⟩
+
+/-- Strips away the name of the type of litters, converting it into a combination of types
+well-known to mathlib. -/
+def litterEquiv : Litter ≃ { a : μ × TypeIndex × Λ // a.2.1 ≠ a.2.2 }
+    where
+  toFun L := ⟨⟨L.ν, L.β, L.γ⟩, L.β_ne_γ⟩
+  invFun L := ⟨L.val.1, L.val.2.1, L.val.2.2, L.prop⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- There are precisely `μ` litters. -/
+@[simp]
+theorem card_litter : #Litter = #μ := by
+  apply le_antisymm
+  · apply litterEquiv.cardinal_eq.trans_le
+    apply (mk_subtype_le _).trans_eq
+    simp only [mk_prod, Cardinal.lift_id, TypeIndex.card, mul_mk_eq_max, max_self,
+      max_eq_left_iff, Λ_le_μ]
+  · apply mk_le_of_injective (f := λ ν ↦ ⟨ν, ⊥, Classical.arbitrary Λ, bot_ne_coe⟩)
+    intro ν₁ ν₂ h
+    cases h
+    rfl
+
+class ToLitter (X : Type _) where
+  /-- Returns a litter associated to this object. -/
+  toLitter : X → Litter
+
+@[inherit_doc] postfix:75 "°" => ToLitter.toLitter
+
+end ConNF

ConNF/Setup/Params.lean

@@ -110,6 +110,17 @@ theorem aleph0_lt_μ : ℵ₀ < #μ :=
 theorem Λ_type_le_μ_ord : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord :=
   Λ_type_le_cof_μ.trans <| ord_cof_le (#μ).ord
 
+theorem Λ_le_cof_μ : #Λ ≤ (#μ).ord.cof := by
+  have := card_le_of_le_ord Λ_type_le_cof_μ
+  rwa [card_type] at this
+
+theorem Λ_le_μ : #Λ ≤ #μ := by
+  have := card_le_of_le_ord Λ_type_le_μ_ord
+  rwa [card_type] at this
+
+theorem κ_le_μ : #κ ≤ #μ :=
+  κ_lt_μ.le
+
 @[irreducible]
 def κEquiv : κ ≃ Set.Iio (#κ).ord := by
   apply Equiv.ulift.{u + 1, u}.symm.trans

ConNF/Setup/Path.lean

@@ -88,6 +88,7 @@ theorem coderiv_single {X Y : Type _} [Coderivative X Y β γ] (x : X) (h : γ <
 instance : SingleDerivative (α ↝ β) (α ↝ γ) β γ where
   sderiv := .cons
 
+/-- The downwards recursion principle for paths. -/
 @[elab_as_elim, induction_eliminator, cases_eliminator]
 def Path.recSderiv {motive : ∀ β, α ↝ β → Sort _}
     (nil : motive α .nil)
@@ -116,6 +117,8 @@ theorem Path.le (A : α ↝ β) : β ≤ α := by
   | nil => exact le_rfl
   | sderiv β γ _A h h' => exact h.le.trans h'
 
+/-- The downwards recursion principle for paths, specialised to the case where the motive at `β`
+only depends on the fact that `β ≤ α`. -/
 def Path.recSderivLe {motive : ∀ β ≤ α, Sort _}
     (nil : motive α le_rfl)
     (sderiv : ∀ β γ, ∀ (A : α ↝ β) (h : γ < β), motive β A.le → motive γ (h.le.trans A.le)) :
@@ -137,6 +140,8 @@ theorem Path.recSderivLe_sderiv {motive : ∀ β ≤ α, Sort _}
     recSderivLe (motive := motive) nil sderiv (A ↘ h) = sderiv β γ A h (recSderiv nil sderiv A) :=
   rfl
 
+/-- The downwards recursion principle for paths, specialised to the case where the motive is not
+dependent on the relation of `β` to `α`. -/
 @[elab_as_elim]
 def Path.recSderivGlobal {motive : TypeIndex → Sort _}
     (nil : motive α)
@@ -195,7 +200,10 @@ theorem Path.coderiv_deriv (A : β ↝ γ) (h₁ : β < α) (h₂ : δ < γ) :
 ## Upwards recursion along paths
 -/
 
-/-- The same as `Path`, but the components of this path point "upwards" instead of "downwards". -/
+/--
+The same as `Path`, but the components of this path point "upwards" instead of "downwards".
+This type is only used for proving `revScoderiv`, and should be considered an implementation detail.
+-/
 inductive RevPath (α : TypeIndex) : TypeIndex → Type u
   | nil : RevPath α α
   | cons {β γ : TypeIndex} : RevPath α β → β < γ → RevPath α γ
@@ -274,6 +282,8 @@ theorem Path.recScoderiv'_cons {motive : ∀ β, β ↝ γ → Sort _}
       scoderiv α β A.rev h (recScoderiv' nil scoderiv A) :=
   rfl
 
+/-- The upwards recursion principle for paths. The `scoderiv` computation rule
+`recScoderiv_scoderiv` is not a definitional equality. -/
 @[elab_as_elim]
 def Path.recScoderiv {motive : ∀ β, β ↝ γ → Sort _}
     (nil : motive γ .nil)

blueprint/src/chapters/environment.tex

@@ -65,12 +65,16 @@ \section{Model parameters}
 \begin{definition}[litter]
   \label{def:Litter}
   \uses{def:Params}
+  \lean{ConNF.Litter}
+  \leanok
   A \emph{litter} is a triple \( L = (\nu, \beta, \gamma) : \mu \times \lambda^\bot \times \lambda \) where \( \beta \neq \gamma \).
   The type of all litters is denoted \( \Litter \), and \( \#\Litter = \#\mu \).
 \end{definition}
 \begin{definition}[atom]
   \label{def:Atom}
   \uses{def:Litter}
+  \lean{ConNF.Atom}
+  \leanok
   An \emph{atom} is a pair \( a = (L, i) : \Litter \times \kappa \).\footnote{This should be formalised as a structure, not as a definition. We should not use the projections of atoms unless absolutely necessary.}
   The type of all atoms is denoted \( \Atom \), and \( \#\Atom = \#\mu \).
   We write \( (-)^\circ : \Atom \to \Litter \) for the operation \( (L, i) \mapsto L \).\footnote{This must be a notation typeclass.}