Finish chapter 2

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

ConNF.lean

@@ -7,9 +7,11 @@ import ConNF.Aux.WellOrder
 import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm
 import ConNF.Setup.BasePositions
+import ConNF.Setup.CoherentData
 import ConNF.Setup.Deny
 import ConNF.Setup.Enumeration
 import ConNF.Setup.Fuzz
+import ConNF.Setup.Level
 import ConNF.Setup.Litter
 import ConNF.Setup.ModelData
 import ConNF.Setup.NearLitter

ConNF/Setup/CoherentData.lean

@@ -0,0 +1,83 @@
+import ConNF.Setup.Fuzz
+import ConNF.Setup.Level
+import ConNF.Setup.ModelData
+
+/-!
+# Coherent data
+
+In this file, we define the type of coherent data below a particular proper type index.
+
+## Main declarations
+
+* `ConNF.InflexiblePath`: A pair of paths starting at `β` that describe a particular way to use
+    a `fuzz` map.
+* `ConNF.CoherentData`: Coherent data below a given level `α`.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+
+namespace ConNF
+
+/-!
+TODO: We're going to try allowing model data at level `⊥` to vary. That is, we use
+`(β : TypeIndex) → [LeLevel β] → ModelData β` instead of `(β : Λ) → [LeLevel β] → ModelData β`.
+-/
+
+variable [Params.{u}] [Level]
+
+/-- A convenience typeclass to hold data below the current level. -/
+class LtData where
+  [data : (β : TypeIndex) → [LeLevel β] → ModelData β]
+  [positions : (β : TypeIndex) → [LtLevel β] → Position (Tangle β)]
+
+instance [LtData] : (β : TypeIndex) → [LeLevel β] → ModelData β :=
+  LtData.data
+
+instance [LtData] : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) :=
+  LtData.positions
+
+class PreCoherentData extends LtData where
+  allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ
+  singleton {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : TSet γ → TSet β
+
+instance [PreCoherentData] {β γ : TypeIndex} [LeLevel β] [LeLevel γ] :
+    Derivative (AllPerm β) (AllPerm γ) β γ where
+  deriv ρ A := A.recSderiv
+    (motive := λ (δ : TypeIndex) (A : β ↝ δ) ↦
+      letI : LeLevel δ := ⟨A.le.trans LeLevel.elim⟩; AllPerm δ)
+    ρ (λ δ ε A h ρ ↦
+      letI : LeLevel δ := ⟨A.le.trans LeLevel.elim⟩
+      letI : LeLevel ε := ⟨h.le.trans LeLevel.elim⟩
+      PreCoherentData.allPermSderiv h ρ)
+
+class CoherentData extends PreCoherentData where
+  allPermSderiv_forget {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) (ρ : AllPerm β) :
+    (ρ ↘ h)ᵁ = ρᵁ ↘ h
+  pos_atom_lt_pos {β : TypeIndex} [LtLevel β] (t : Tangle β) (A : β ↝ ⊥) (a : Atom) :
+    a ∈ (t.support ⇘. A)ᴬ → pos a < pos t
+  pos_nearLitter_lt_pos {β : TypeIndex} [LtLevel β] (t : Tangle β) (A : β ↝ ⊥) (N : NearLitter) :
+    N ∈ (t.support ⇘. A)ᴺ → pos N < pos t
+  smul_fuzz {γ δ : TypeIndex} {ε : Λ} [LeLevel γ] [LtLevel δ] [LtLevel ε]
+    (hδ : δ < γ) (hε : ε < γ) (hδε : δ ≠ ε) (ρ : AllPerm γ) (t : Tangle δ) :
+    ρᵁ ↘ hε ↘. • fuzz hδε t = fuzz hδε (ρ ↘ hδ • t)
+  exists_of_smulFuzz {γ : TypeIndex} [LeLevel γ]
+    (ρs : {δ : TypeIndex} → [LtLevel δ] → δ < γ → AllPerm δ)
+    (h : ∀ {δ : TypeIndex} {ε : Λ} [LeLevel γ] [LtLevel δ] [LtLevel ε]
+      (hδ : δ < γ) (hε : ε < γ) (hδε : δ ≠ ε) (t : Tangle δ),
+      (ρs hε)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hδ • t)) :
+    ∃ ρ : AllPerm γ, ∀ δ : TypeIndex, [LtLevel δ] → ∀ hδ : δ < γ, ρ ↘ hδ = ρs hδ
+  typedMem_tSetForget {β : Λ} {γ : TypeIndex} [LeLevel β] [LeLevel γ]
+    (hγ : γ < β) (x : TSet β) (y : StrSet γ) :
+    y ∈[hγ] xᵁ → ∃ z : TSet γ, y = zᵁ
+  typedMem_singleton_iff {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (hγ : γ < β) (x y : TSet γ) :
+    y ∈[hγ] singleton hγ x ↔ y = x
+
+export CoherentData (allPermSderiv_forget pos_atom_lt_pos pos_nearLitter_lt_pos smul_fuzz
+  exists_of_smulFuzz typedMem_tSetForget typedMem_singleton_iff)
+
+attribute [simp] allPermSderiv_forget typedMem_singleton_iff
+
+end ConNF

ConNF/Setup/Fuzz.lean

@@ -35,4 +35,14 @@ class TypedNearLitters {α : Λ} [ModelData α] [Position (Tangle α)] where
   typed_injective : Function.Injective typed
   pos_le_pos_of_typed (N : NearLitter) (t : Tangle α) : t.set = typed N → pos N ≤ pos t
 
+@[ext]
+structure InflexiblePath (β : TypeIndex) where
+  γ : TypeIndex
+  δ : TypeIndex
+  ε : Λ
+  hδ : δ < γ
+  hε : ε < γ
+  hδε : δ ≠ ε
+  A : β ↝ γ
+
 end ConNF

ConNF/Setup/Level.lean

@@ -0,0 +1,43 @@
+import ConNF.Setup.TypeIndex
+
+/-!
+# Levels
+
+In this file, we provide a typeclass `Level` that stores the current type level of the construction.
+
+## Main declarations
+
+* `ConNF.Level`: The current level.
+* `ConNF.LtLevel`: A type index less than the current level.
+* `ConNF.LeLevel`: A type index less than or equal to the current level.
+-/
+
+universe u
+
+open Cardinal
+
+namespace ConNF
+
+variable [Params.{u}]
+
+class Level where
+  /-- The current level of the construction. -/
+  α : Λ
+
+export Level (α)
+
+variable [Level]
+
+class LtLevel (β : TypeIndex) : Prop where
+  elim : β < α
+
+class LeLevel (β : TypeIndex) : Prop where
+  elim : β ≤ α
+
+instance {β : TypeIndex} [LtLevel β] : LeLevel β where
+  elim := LtLevel.elim.le
+
+instance : LeLevel α where
+  elim := le_rfl
+
+end ConNF

ConNF/Setup/ModelData.lean

@@ -44,17 +44,81 @@ structure Support.Supports {X : Type _} {α : TypeIndex} [PreModelData α] [MulA
   nearLitters_eq_empty_of_bot : α = ⊥ → Sᴺ = .empty
 
 class ModelData (α : TypeIndex) extends PreModelData α where
+  tSetForget_injective : Function.Injective tSetForget
+  allPermForget_injective : Function.Injective allPermForget
   allPermForget_one : (1 : AllPerm)ᵁ = 1
   allPermForget_mul (ρ₁ ρ₂ : AllPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ
   smul_forget (ρ : AllPerm) (x : TSet) : (ρ • x)ᵁ = ρᵁ • xᵁ
   exists_support (x : TSet) : ∃ S : Support α, S.Supports x
 
+export ModelData (tSetForget_injective allPermForget_injective allPermForget_one allPermForget_mul
+  smul_forget exists_support)
+
+attribute [simp] allPermForget_one allPermForget_mul smul_forget
+
+@[simp]
+theorem allPermForget_inv {α : TypeIndex} [ModelData α] (ρ : AllPerm α) : ρ⁻¹ᵁ = ρᵁ⁻¹ := by
+  rw [eq_inv_iff_mul_eq_one, ← allPermForget_mul, inv_mul_cancel, allPermForget_one]
+
+theorem Support.Supports.smul_eq_smul {X : Type _} {α : TypeIndex}
+    [ModelData α] [MulAction (AllPerm α) X]
+    {S : Support α} {x : X} (h : S.Supports x) {ρ₁ ρ₂ : AllPerm α} (hρ : ρ₁ᵁ • S = ρ₂ᵁ • S) :
+    ρ₁ • x = ρ₂ • x := by
+  have := h.supports (ρ₂⁻¹ * ρ₁) ?_
+  · rwa [mul_smul, inv_smul_eq_iff] at this
+  · rwa [allPermForget_mul, mul_smul, allPermForget_inv, inv_smul_eq_iff]
+
+theorem Support.Supports.smul {X : Type _} {α : TypeIndex}
+    [ModelData α] [MulAction (AllPerm α) X]
+    {S : Support α} {x : X} (h : S.Supports x) (ρ : AllPerm α) :
+    (ρᵁ • S).Supports (ρ • x) := by
+  constructor
+  · intro σ hσ
+    rw [smul_smul, ← allPermForget_mul] at hσ
+    have := h.smul_eq_smul hσ
+    rwa [mul_smul] at this
+  · intro h'
+    rw [smul_nearLitters, h.nearLitters_eq_empty_of_bot h']
+    rfl
+
+instance {β α : TypeIndex} [ModelData β] [ModelData α] : TypedMem (TSet β) (TSet α) β α where
+  typedMem h y x := yᵁ ∈[h] xᵁ
+
 @[ext]
 structure Tangle (α : TypeIndex) [ModelData α] where
   set : TSet α
   support : Support α
   support_supports : support.Supports set
 
+instance {α : TypeIndex} [ModelData α] : SMul (AllPerm α) (Tangle α) where
+  smul ρ t := ⟨ρ • t.set, ρᵁ • t.support, t.support_supports.smul ρ⟩
+
+@[simp]
+theorem Tangle.smul_set {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (t : Tangle α) :
+    (ρ • t).set = ρ • t.set :=
+  rfl
+
+@[simp]
+theorem Tangle.smul_support {α : TypeIndex} [ModelData α] (ρ : AllPerm α) (t : Tangle α) :
+    (ρ • t).support = ρᵁ • t.support :=
+  rfl
+
+theorem Tangle.smul_eq_smul {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α}
+    (h : ρ₁ᵁ • t.support = ρ₂ᵁ • t.support) :
+    ρ₁ • t = ρ₂ • t :=
+  Tangle.ext (t.support_supports.smul_eq_smul h) h
+
+instance {α : TypeIndex} [ModelData α] : MulAction (AllPerm α) (Tangle α) where
+  one_smul t := by
+    ext : 1
+    · rw [Tangle.smul_set, one_smul]
+    · rw [Tangle.smul_support, allPermForget_one, one_smul]
+  mul_smul ρ₁ ρ₂ t := by
+    ext : 1
+    · rw [Tangle.smul_set, Tangle.smul_set, Tangle.smul_set, mul_smul]
+    · rw [Tangle.smul_support, Tangle.smul_support, Tangle.smul_support,
+        allPermForget_mul, mul_smul]
+
 /-!
 ## Criteria for supports
 -/
@@ -98,6 +162,8 @@ def botPreModelData : PreModelData ⊥ where
   allPermForget ρ _ := ρ
 
 def botModelData : ModelData ⊥ where
+  tSetForget_injective := StrSet.botEquiv.symm.injective
+  allPermForget_injective _ _ h := congr_fun h Path.nil
   allPermForget_one := rfl
   allPermForget_mul _ _ := rfl
   smul_forget ρ x := by

ConNF/Setup/StrSet.lean

@@ -46,7 +46,7 @@ def coeEquiv {α : Λ} :
 
 /-- Extensionality for structural sets at proper type indices. If two structural sets have the same
 extensions at every lower type index, then they are the same. -/
-theorem coe_ext_iff {α : Λ} {x y : StrSet α} :
+theorem coe_ext_iff' {α : Λ} {x y : StrSet α} :
     x = y ↔ ∀ β hβ z, z ∈ coeEquiv x β hβ ↔ z ∈ coeEquiv y β hβ := by
   constructor
   · rintro rfl
@@ -94,4 +94,25 @@ theorem strPerm_smul_coe {α : Λ} (π : StrPerm α) (x : StrSet α) :
 
 end StrSet
 
+/-!
+## Notation for typed membership
+-/
+
+class TypedMem (X Y : Type _) (β α : outParam TypeIndex) where
+  typedMem : β < α → X → Y → Prop
+
+notation:50 x:50 " ∈[" h:50 "] " y:50 => TypedMem.typedMem h x y
+
+instance {β α : TypeIndex} : TypedMem (StrSet β) (StrSet α) β α where
+  typedMem h x y :=
+    match α with
+    | ⊥ => (not_lt_bot h).elim
+    | (α : Λ) => x ∈ StrSet.coeEquiv y β h
+
+/-- Extensionality for structural sets at proper type indices. If two structural sets have the same
+extensions at every lower type index, then they are the same. -/
+theorem StrSet.coe_ext_iff {α : Λ} {x y : StrSet α} :
+    x = y ↔ ∀ β : TypeIndex, ∀ hβ : β < α, ∀ z : StrSet β, z ∈[hβ] x ↔ z ∈[hβ] y :=
+  StrSet.coe_ext_iff'
+
 end ConNF

blueprint/src/chapters/environment.tex

@@ -394,6 +394,8 @@ \section{Hypotheses of the recursion}
 \begin{definition}[inflexible path]
   \label{def:InflexiblePath}
   \uses{prop:fuzz}
+  \lean{ConNF.InflexiblePath}
+  \leanok
   Let \( \alpha \) be a proper type index.
   Suppose that we have model data for all type indices \( \beta \leq \alpha \) and position functions for \( \Tang_\beta \) for all \( \beta < \alpha \).
   For any type index \( \beta \leq \alpha \), a \emph{inflexible \( \beta \)-path} is a tuple \( I = (\gamma, \delta, \varepsilon, A) \) where \( \delta, \varepsilon < \gamma \) are distinct, the index \( \varepsilon \) is proper, and \( A : \beta \tpath \gamma \).
@@ -403,6 +405,8 @@ \section{Hypotheses of the recursion}
 \begin{definition}[typed near-litter]
   \label{def:TypedNearLitter}
   \uses{def:ModelData,def:Tangle,prop:BasePositions}
+  \lean{ConNF.TypedNearLitters}
+  \leanok
   Let \( \alpha \) be a proper type index with model data, and suppose that \( \Tang_\alpha \) has a position function.
   We say that \( \alpha \) has \emph{typed near-litters} if there is an embedding \( \typed_\alpha : \NearLitter \to \TSet_\alpha \) such that
   \begin{itemize}
@@ -414,6 +418,8 @@ \section{Hypotheses of the recursion}
 \begin{definition}[coherent data]
   \label{def:CoherentData}
   \uses{def:TypedNearLitter,def:InflexiblePath}
+  \lean{ConNF.CoherentData}
+  \leanok
   Let \( \alpha \) be a proper type index.
   Suppose that we have model data for all type indices \( \beta \leq \alpha \), position functions for \( \Tang_\beta \) for all \( \beta < \alpha \), and typed near-litters for all \( \beta < \alpha \).
   We say that the model data is \emph{coherent} below level \( \alpha \) if the following hold.