From 30412c76fd110a487e5e89b62414237b38a37227 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 11 Sep 2024 14:38:49 +0100 Subject: [PATCH] Coherence Signed-off-by: zeramorphic --- ConNF.lean | 1 + ConNF/Aux/Rel.lean | 33 ++++- ConNF/FOA/BaseApprox.lean | 84 ++++++++++- ConNF/FOA/StrApprox.lean | 231 +++++++++++++++++++++++++++++++ ConNF/Setup/CoherentData.lean | 2 - ConNF/Setup/Enumeration.lean | 29 ++++ ConNF/Setup/Fuzz.lean | 29 ++-- ConNF/Setup/Path.lean | 11 ++ ConNF/Setup/PathEnumeration.lean | 23 ++- ConNF/Setup/StrPerm.lean | 2 +- ConNF/Setup/Support.lean | 40 ++++++ ConNF/Setup/Tree.lean | 8 ++ blueprint/src/chapters/foa.tex | 9 ++ 13 files changed, 478 insertions(+), 24 deletions(-) create mode 100644 ConNF/FOA/StrApprox.lean diff --git a/ConNF.lean b/ConNF.lean index fa6eac2cf8..b6531555ee 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -5,6 +5,7 @@ import ConNF.Aux.Set import ConNF.Aux.Transfer import ConNF.Aux.WellOrder import ConNF.FOA.BaseApprox +import ConNF.FOA.StructApprox import ConNF.Setup.Atom import ConNF.Setup.BasePerm import ConNF.Setup.BasePositions diff --git a/ConNF/Aux/Rel.lean b/ConNF/Aux/Rel.lean index e8466b8882..801b172515 100644 --- a/ConNF/Aux/Rel.lean +++ b/ConNF/Aux/Rel.lean @@ -5,11 +5,7 @@ open scoped symmDiff namespace Rel -variable {α β : Type _} - --- Note the backward composition style of Rel.comp! -@[inherit_doc] -scoped infixr:80 " • " => Rel.comp +variable {α β γ : Type _} @[mk_iff] structure Injective (r : Rel α β) : Prop where @@ -109,6 +105,12 @@ theorem inv_preimage {r : Rel α β} {s : Set α} : r.inv.preimage s = r.image s := rfl +theorem comp_inv {r : Rel α β} {s : Rel β γ} : + (r.comp s).inv = s.inv.comp r.inv := by + ext c a + simp only [inv, flip, comp] + tauto + theorem Injective.image_injective {r : Rel α β} (h : r.Injective) {s t : Set α} (hs : s ⊆ r.dom) (ht : t ⊆ r.dom) (hst : r.image s = r.image t) : s = t := by rw [Set.ext_iff] at hst ⊢ @@ -162,6 +164,18 @@ theorem Permutative.inv {r : Rel α α} (h : r.Permutative) : r.inv.Permutative theorem Permutative.inv_dom {r : Rel α α} (h : r.Permutative) : r.inv.dom = r.dom := h.codom_eq_dom +theorem Injective.comp {r : Rel α β} {s : Rel β γ} (hr : r.Injective) (hs : s.Injective) : + (r.comp s).Injective := by + constructor + rintro a₁ a₂ c ⟨b₁, hr₁, hs₁⟩ ⟨b₂, hr₂, hs₂⟩ + cases hs.injective hs₁ hs₂ + exact hr.injective hr₁ hr₂ + +theorem Coinjective.comp {r : Rel α β} {s : Rel β γ} (hr : r.Coinjective) (hs : s.Coinjective) : + (r.comp s).Coinjective := by + rw [← inv_injective_iff, comp_inv] + exact Injective.comp (inv_injective_iff.mpr hs) (inv_injective_iff.mpr hr) + /-- An alternative spelling of `Rel.graph` that is useful for proving inequalities of cardinals. -/ def graph' (r : Rel α β) : Set (α × β) := r.uncurry @@ -226,6 +240,15 @@ theorem Injective.image_symmDiff {r : Rel α β} (h : r.Injective) (s t : Set α r.image (s ∆ t) = r.image s ∆ r.image t := by rw [Set.symmDiff_def, Set.symmDiff_def, image_union, h.image_diff, h.image_diff] +theorem image_eq_of_le_of_le {r s : Rel α β} (h : r ≤ s) {t : Set α} (ht : ∀ x ∈ t, s x ≤ r x) : + r.image t = s.image t := by + ext y + constructor + · rintro ⟨x, hx, hy⟩ + exact ⟨x, hx, h x y hy⟩ + · rintro ⟨x, hx, hy⟩ + exact ⟨x, hx, ht x hx y hy⟩ + @[simp] theorem sup_inv {r s : Rel α β} : (r ⊔ s).inv = r.inv ⊔ s.inv := diff --git a/ConNF/FOA/BaseApprox.lean b/ConNF/FOA/BaseApprox.lean index 4e628eed7b..afbae9420b 100644 --- a/ConNF/FOA/BaseApprox.lean +++ b/ConNF/FOA/BaseApprox.lean @@ -1,4 +1,4 @@ -import ConNF.Setup.NearLitter +import ConNF.Setup.Support /-! # Base approximations @@ -338,6 +338,75 @@ theorem atoms_le_of_le {ψ χ : BaseApprox} (h : ψ ≤ χ) : ψᴬ ≤ χᴬ := sup_le_sup h.1.le (typical_le_of_le h) +theorem nearLitters_le_of_le {ψ χ : BaseApprox} (h : ψ ≤ χ) : + ψᴺ ≤ χᴺ := by + rintro N₁ N₂ ⟨h₁, h₂, h₃⟩ + refine ⟨litters_le_of_le h N₁ᴸ N₂ᴸ h₁, ?_, ?_⟩ + · exact h₂.trans <| dom_mono <| atoms_le_of_le h + · rw [← h₃] + symm + apply image_eq_of_le_of_le (atoms_le_of_le h) + intro a₁ ha₁ a₂ ha₂ + obtain ⟨a₃, ha₃⟩ := h₂ ha₁ + cases χ.atoms_permutative.coinjective ha₂ (atoms_le_of_le h a₁ a₃ ha₃) + exact ha₃ + +instance : SMul BaseApprox BaseSupport where + smul ψ S := ⟨Sᴬ.comp ψᴬ ψ.atoms_permutative.toCoinjective, + Sᴺ.comp ψᴺ ψ.nearLitters_permutative.toCoinjective⟩ + +theorem smul_atoms (ψ : BaseApprox) (S : BaseSupport) : + (ψ • S)ᴬ = Sᴬ.comp ψᴬ ψ.atoms_permutative.toCoinjective := + rfl + +theorem smul_nearLitters (ψ : BaseApprox) (S : BaseSupport) : + (ψ • S)ᴺ = Sᴺ.comp ψᴺ ψ.nearLitters_permutative.toCoinjective := + rfl + +theorem smul_support_eq_smul_iff (ψ : BaseApprox) (S : BaseSupport) (π : BasePerm) : + ψ • S = π • S ↔ (∀ a ∈ Sᴬ, ψᴬ a (π • a)) ∧ (∀ N ∈ Sᴺ, ψᴺ N (π • N)) := by + constructor + · intro h + constructor + · rintro a ⟨i, ha⟩ + have : (π • S)ᴬ.rel i (π • a) := by + rwa [BaseSupport.smul_atoms, Enumeration.smul_rel, inv_smul_smul] + rw [← h] at this + obtain ⟨b, hb, hψ⟩ := this + cases Sᴬ.rel_coinjective.coinjective ha hb + exact hψ + · rintro a ⟨i, ha⟩ + have : (π • S)ᴺ.rel i (π • a) := by + rwa [BaseSupport.smul_nearLitters, Enumeration.smul_rel, inv_smul_smul] + rw [← h] at this + obtain ⟨b, hb, hψ⟩ := this + cases Sᴺ.rel_coinjective.coinjective ha hb + exact hψ + · intro h + ext : 2; rfl; swap; rfl + · ext i a : 3 + rw [smul_atoms, BaseSupport.smul_atoms, Enumeration.smul_rel] + constructor + · rintro ⟨b, hb, hψ⟩ + cases ψ.atoms_permutative.coinjective hψ (h.1 b ⟨i, hb⟩) + rwa [inv_smul_smul] + · intro ha + refine ⟨π⁻¹ • a, ha, ?_⟩ + have := h.1 (π⁻¹ • a) ⟨i, ha⟩ + rwa [smul_inv_smul] at this + · ext i a : 3 + rw [smul_nearLitters, BaseSupport.smul_nearLitters, Enumeration.smul_rel] + constructor + · rintro ⟨b, hb, hψ⟩ + cases ψ.nearLitters_permutative.coinjective hψ (h.2 b ⟨i, hb⟩) + rwa [inv_smul_smul] + · intro ha + refine ⟨π⁻¹ • a, ha, ?_⟩ + have := h.2 (π⁻¹ • a) ⟨i, ha⟩ + rwa [smul_inv_smul] at this + +section addOrbit + def addOrbitLitters (f : ℤ → Litter) : Rel Litter Litter := λ L₁ L₂ ↦ ∃ n : ℤ, L₁ = f n ∧ L₂ = f (n + 1) @@ -386,6 +455,19 @@ def addOrbit (ψ : BaseApprox) (f : ℤ → Litter) (disjoint_litters_dom_addOrbitLitters_dom ψ f hfψ) exceptions_small := ψ.exceptions_small +variable {ψ : BaseApprox} {f : ℤ → Litter} {hf : ∀ m n k, f m = f n → f (m + k) = f (n + k)} + {hfψ : ∀ n, f n ∉ ψᴸ.dom} + +theorem addOrbit_litters : + (ψ.addOrbit f hf hfψ)ᴸ = ψᴸ ⊔ addOrbitLitters f := + rfl + +theorem le_addOrbit : + ψ ≤ ψ.addOrbit f hf hfψ := + ⟨rfl, le_sup_left⟩ + +end addOrbit + end BaseApprox end ConNF diff --git a/ConNF/FOA/StrApprox.lean b/ConNF/FOA/StrApprox.lean new file mode 100644 index 0000000000..dd3e62acc0 --- /dev/null +++ b/ConNF/FOA/StrApprox.lean @@ -0,0 +1,231 @@ +import ConNF.Setup.CoherentData +import ConNF.FOA.BaseApprox + +/-! +# Structural approximations + +In this file, we define structural approximations, which are trees of base approximations. + +## Main declarations + +* `ConNF.StrApprox`: The type of structural approximations. +* `ConNF.InflexiblePath`: A pair of paths starting at `β` that describe a particular way to use + a `fuzz` map. +* `ConNF.Inflexible`: A litter is said to be inflexible along a path if it can be obtained by + applying a `fuzz` map along this path. +-/ + +noncomputable section +universe u + +open Cardinal Ordinal + +namespace ConNF + +variable [Params.{u}] {β : TypeIndex} + +abbrev StrApprox : TypeIndex → Type u := + Tree BaseApprox + +namespace StrApprox + +section addOrbit + +open scoped Classical in +def addOrbit (ψ : StrApprox β) (A : β ↝ ⊥) (f : ℤ → Litter) + (hf : ∀ m n k, f m = f n → f (m + k) = f (n + k)) (hfψ : ∀ n, f n ∉ (ψ A)ᴸ.dom) : StrApprox β := + λ B ↦ if h : A = B then (ψ B).addOrbit f hf (h ▸ hfψ) else ψ B + +variable {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → Litter} + {hf : ∀ m n k, f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ n, f n ∉ (ψ A)ᴸ.dom} + +theorem addOrbit_apply : + ψ.addOrbit A f hf hfψ A = (ψ A).addOrbit f hf hfψ := by + rw [addOrbit, dif_pos] + rfl + +theorem addOrbit_apply_ne (B : β ↝ ⊥) (hB : A ≠ B) : + ψ.addOrbit A f hf hfψ B = ψ B := by + rw [addOrbit, dif_neg hB] + +theorem le_addOrbit : + ψ ≤ ψ.addOrbit A f hf hfψ := by + intro B + by_cases hB : A = B + · cases hB + rw [addOrbit_apply] + exact BaseApprox.le_addOrbit + · rw [addOrbit_apply_ne B hB] + +end addOrbit + +instance : SMul (StrApprox β) (Support β) where + smul ψ S := ⟨Sᴬ.comp (Enumeration.relWithPath λ A ↦ (ψ A)ᴬ) + (Enumeration.relWithPath_coinjective λ A ↦ (ψ A).atoms_permutative.toCoinjective), + Sᴺ.comp (Enumeration.relWithPath λ A ↦ (ψ A)ᴺ) + (Enumeration.relWithPath_coinjective λ A ↦ (ψ A).nearLitters_permutative.toCoinjective)⟩ + +@[simp] +theorem smul_support_derivBot (ψ : StrApprox β) (S : Support β) (A : β ↝ ⊥) : + (ψ • S) ⇘. A = ψ A • (S ⇘. A) := by + ext : 2; rfl; swap; rfl + all_goals + · ext i a + constructor + · rintro ⟨⟨B, b⟩, h₁, h₂⟩ + cases h₂.1 + exact ⟨b, h₁, h₂.2⟩ + · rintro ⟨b, h₁, h₂⟩ + exact ⟨⟨A, b⟩, h₁, rfl, h₂⟩ + +theorem smul_support_eq_smul_iff (ψ : StrApprox β) (S : Support β) (π : StrPerm β) : + ψ • S = π • S ↔ ∀ A, + (∀ a ∈ (S ⇘. A)ᴬ, (ψ A)ᴬ a (π A • a)) ∧ (∀ N ∈ (S ⇘. A)ᴺ, (ψ A)ᴺ N (π A • N)) := by + simp only [Support.ext_iff, smul_support_derivBot, Support.smul_derivBot, + BaseApprox.smul_support_eq_smul_iff] + +end StrApprox + +@[ext] +structure InflexiblePath (β : TypeIndex) where + γ : TypeIndex + δ : TypeIndex + ε : Λ + hδ : δ < γ + hε : ε < γ + hδε : δ ≠ ε + A : β ↝ γ + +variable [Level.{u}] [CoherentData] + +instance [LeLevel β] (P : InflexiblePath β) : LeLevel P.γ := + ⟨P.A.le.trans LeLevel.elim⟩ + +instance [LeLevel β] (P : InflexiblePath β) : LtLevel P.δ := + ⟨P.hδ.trans_le LeLevel.elim⟩ + +instance [LeLevel β] (P : InflexiblePath β) : LtLevel P.ε := + ⟨P.hε.trans_le LeLevel.elim⟩ + +def Inflexible [LeLevel β] (A : β ↝ ⊥) (L : Litter) : Prop := + ∃ P : InflexiblePath β, ∃ t, A = P.A ↘ P.hε ↘. ∧ L = fuzz P.hδε t + +theorem inflexible_iff [LeLevel β] (A : β ↝ ⊥) (L : Litter) : + Inflexible A L ↔ ∃ P : InflexiblePath β, ∃ t, A = P.A ↘ P.hε ↘. ∧ L = fuzz P.hδε t := + Iff.rfl + +theorem not_inflexible_iff [LeLevel β] (A : β ↝ ⊥) (L : Litter) : + ¬Inflexible A L ↔ ∀ P : InflexiblePath β, ∀ t, A = P.A ↘ P.hε ↘. → L ≠ fuzz P.hδε t := by + rw [inflexible_iff] + push_neg + rfl + +theorem inflexible_cases [LeLevel β] (A : β ↝ ⊥) (L : Litter) : + (∃ P : InflexiblePath β, ∃ t, A = P.A ↘ P.hε ↘. ∧ L = fuzz P.hδε t) ∨ ¬Inflexible A L := + Classical.em _ + +theorem inflexiblePath_subsingleton [LeLevel β] {A : β ↝ ⊥} {L : Litter} + {P₁ P₂ : InflexiblePath β} {t₁ : Tangle P₁.δ} {t₂ : Tangle P₂.δ} + (hP₁ : A = P₁.A ↘ P₁.hε ↘.) (hP₂ : A = P₂.A ↘ P₂.hε ↘.) + (ht₁ : L = fuzz P₁.hδε t₁) (ht₂ : L = fuzz P₂.hδε t₂) : + P₁ = P₂ := by + subst hP₁ + subst ht₁ + have := fuzz_β_eq ht₂ -- δ₁ = δ₂ + obtain ⟨γ₁, δ₁, ε₁, _, _, _, A₁⟩ := P₁ + obtain ⟨γ₂, δ₂, ε₂, _, _, _, A₂⟩ := P₂ + cases this + cases Path.sderivBot_index_injective hP₂ -- ε₁ = ε₂ + cases Path.sderiv_index_injective (Path.sderivBot_path_injective hP₂) -- γ₁ = γ₂ + cases Path.sderiv_path_injective (Path.sderivBot_path_injective hP₂) -- A₁ = A₂ + rfl + +namespace StrApprox + +/-- `ψ` is defined coherently at `(A, L₁, L₂)` (or could be defined coherently at this triple). -/ +structure CoherentAt [LeLevel β] + (ψ : StrApprox β) (A : β ↝ ⊥) (L₁ L₂ : Litter) : Prop where + inflexible (P : InflexiblePath β) (t : Tangle P.δ) + (hA : A = P.A ↘ P.hε ↘.) (ht : L₁ = fuzz P.hδε t) : + ∃ ρ : AllPerm P.δ, ψ ⇘ P.A ↘ P.hδ • t.support = ρᵁ • t.support ∧ L₂ = fuzz P.hδε (ρ • t) + flexible (h : ¬Inflexible A L₁) : ¬Inflexible A L₂ + +theorem coherentAt_inflexible [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {L₁ L₂ : Litter} + {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.) (ht : L₁ = fuzz P.hδε t) : + ψ.CoherentAt A L₁ L₂ ↔ ∃ ρ : AllPerm P.δ, + ψ ⇘ P.A ↘ P.hδ • t.support = ρᵁ • t.support ∧ L₂ = fuzz P.hδε (ρ • t) := by + constructor + · intro h + exact h.inflexible P t hA ht + · intro h + constructor + · intro P' t' hA' ht' + cases inflexiblePath_subsingleton hA hA' ht ht' + cases fuzz_injective (ht.symm.trans ht') + exact h + · intro h' + cases h' ⟨P, t, hA, ht⟩ + +theorem smul_eq_of_coherentAt_inflexible [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {L₁ L₂ : Litter} + {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.) (ht : L₁ = fuzz P.hδε t) + (h : ψ.CoherentAt A L₁ L₂) : + ∀ ρ : AllPerm P.δ, ψ ⇘ P.A ↘ P.hδ • t.support = ρᵁ • t.support → L₂ = fuzz P.hδε (ρ • t) := by + intro ρ₁ hρ₁ + rw [coherentAt_inflexible hA ht] at h + obtain ⟨ρ₂, hρ₂, rfl⟩ := h + congr 1 + apply t.smul_eq_smul + rw [← hρ₁, ← hρ₂] + +theorem coherentAt_flexible [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {L₁ L₂ : Litter} + (hL : ¬Inflexible A L₁) : + ψ.CoherentAt A L₁ L₂ ↔ ¬Inflexible A L₂ := by + constructor + · intro h + exact h.flexible hL + · intro h + constructor + · intro P t hA ht + cases hL ⟨P, t, hA, ht⟩ + · intro + exact h + +theorem CoherentAt.mono [LeLevel β] {ψ χ : StrApprox β} {A : β ↝ ⊥} {L₁ L₂ : Litter} + (h : ψ.CoherentAt A L₁ L₂) (hψχ : ψ ≤ χ) : χ.CoherentAt A L₁ L₂ := by + obtain (⟨P, t, hA, hL⟩ | hL) := inflexible_cases A L₁ + · rw [coherentAt_inflexible hA hL] at h ⊢ + obtain ⟨ρ, hρ₁, hρ₂⟩ := h + refine ⟨ρ, ?_, hρ₂⟩ + rw [smul_support_eq_smul_iff] at hρ₁ ⊢ + simp only [Tree.sderiv_apply, Tree.deriv_apply] at hρ₁ ⊢ + intro B + constructor + · intro a ha + apply BaseApprox.atoms_le_of_le (hψχ (P.A ⇘ (B ↗ P.hδ))) + exact (hρ₁ B).1 a ha + · intro a ha + apply BaseApprox.nearLitters_le_of_le (hψχ (P.A ⇘ (B ↗ P.hδ))) + exact (hρ₁ B).2 a ha + · rwa [coherentAt_flexible hL] at h ⊢ + +def Coherent [LeLevel β] (ψ : StrApprox β) : Prop := + ∀ A L₁ L₂, (ψ A)ᴸ L₁ L₂ → ψ.CoherentAt A L₁ L₂ + +theorem addOrbit_coherent [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → Litter} + {hf : ∀ m n k, f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ n, f n ∉ (ψ A)ᴸ.dom} + (hψ : ψ.Coherent) (hfc : ∀ n, ψ.CoherentAt A (f n) (f (n + 1))) : + (ψ.addOrbit A f hf hfψ).Coherent := by + intro B L₁ L₂ + by_cases hB : A = B + · subst hB + rw [addOrbit_apply, BaseApprox.addOrbit_litters] + rintro (hL | ⟨n, rfl, rfl⟩) + · exact (hψ A L₁ L₂ hL).mono le_addOrbit + · exact (hfc n).mono le_addOrbit + · rw [addOrbit_apply_ne B hB] + intro hL + exact (hψ B L₁ L₂ hL).mono le_addOrbit + +end StrApprox + +end ConNF diff --git a/ConNF/Setup/CoherentData.lean b/ConNF/Setup/CoherentData.lean index 9d89999f6c..d026c48781 100644 --- a/ConNF/Setup/CoherentData.lean +++ b/ConNF/Setup/CoherentData.lean @@ -9,8 +9,6 @@ In this file, we define the type of coherent data below a particular proper type ## 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 `α`. -/ diff --git a/ConNF/Setup/Enumeration.lean b/ConNF/Setup/Enumeration.lean index dbbe34e9d0..92de560bee 100644 --- a/ConNF/Setup/Enumeration.lean +++ b/ConNF/Setup/Enumeration.lean @@ -173,6 +173,35 @@ theorem mem_invImage {f : Y → X} {hf : f.Injective} (y : Y) : y ∈ E.invImage f hf ↔ f y ∈ E := Iff.rfl +def comp (E : Enumeration X) (r : Rel X Y) (hr : r.Coinjective) : Enumeration Y where + bound := E.bound + rel := E.rel.comp r + lt_bound := by + rintro i ⟨y, x, hy⟩ + exact E.lt_bound i ⟨x, hy.1⟩ + rel_coinjective := E.rel_coinjective.comp hr + +instance {G X : Type _} [Group G] [MulAction G X] : + SMul G (Enumeration X) where + smul π E := E.invImage (λ x ↦ π⁻¹ • x) (MulAction.injective π⁻¹) + +@[simp] +theorem smul_rel {G X : Type _} [Group G] [MulAction G X] + (π : G) (E : Enumeration X) (i : κ) (x : X) : + (π • E).rel i x ↔ E.rel i (π⁻¹ • x) := + Iff.rfl + +instance {G X : Type _} [Group G] [MulAction G X] : + MulAction G (Enumeration X) where + one_smul E := by + ext i x + · rfl + · rw [smul_rel, inv_one, one_smul] + mul_smul π₁ π₂ E := by + ext i x + · rfl + · rw [smul_rel, smul_rel, smul_rel, mul_inv_rev, mul_smul] + -- TODO: Some stuff about the partial order on enumerations and concatenation of enumerations. end Enumeration diff --git a/ConNF/Setup/Fuzz.lean b/ConNF/Setup/Fuzz.lean index a1a069375d..6e5a0aea1a 100644 --- a/ConNF/Setup/Fuzz.lean +++ b/ConNF/Setup/Fuzz.lean @@ -28,6 +28,25 @@ def fuzz (hβγ : β ≠ γ) : Tangle β → Litter := (⟨·, β, γ, hβγ⟩) ∘ funOfDeny card_le_of_position (λ t ↦ {pos t}) (λ _ ↦ (mk_singleton _).trans_lt (one_lt_aleph0.trans aleph0_lt_μ_ord_cof)) +theorem fuzz_β_eq {β' : TypeIndex} [ModelData β'] [Position (Tangle β')] {γ' : Λ} + {hβγ : β ≠ γ} {hβγ' : β' ≠ γ'} {t : Tangle β} {t' : Tangle β'} + (h : fuzz hβγ t = fuzz hβγ' t') : + β = β' := + congr_arg Litter.β h + +theorem fuzz_γ_eq {β' : TypeIndex} [ModelData β'] [Position (Tangle β')] {γ' : Λ} + {hβγ : β ≠ γ} {hβγ' : β' ≠ γ'} {t : Tangle β} {t' : Tangle β'} + (h : fuzz hβγ t = fuzz hβγ' t') : + γ = γ' := + congr_arg Litter.γ h + +theorem fuzz_injective {hβγ : β ≠ γ} {t₁ t₂ : Tangle β} (h : fuzz hβγ t₁ = fuzz hβγ t₂) : + t₁ = t₂ := by + refine Function.Injective.comp ?_ (funOfDeny_injective _ _ _) h + intro ν₁ ν₂ h + cases h + rfl + end fuzz class TypedNearLitters {α : Λ} [ModelData α] [Position (Tangle α)] where @@ -35,14 +54,4 @@ 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 diff --git a/ConNF/Setup/Path.lean b/ConNF/Setup/Path.lean index 99dea053b8..6cf9f44ee1 100644 --- a/ConNF/Setup/Path.lean +++ b/ConNF/Setup/Path.lean @@ -251,11 +251,22 @@ theorem Path.sderiv_index_injective {A : α ↝ β} {B : α ↝ γ} {hδβ : δ cases h rfl +theorem Path.sderivBot_index_injective {β γ : Λ} {A : α ↝ β} {B : α ↝ γ} + (h : A ↘. = B ↘.) : + β = γ := by + cases h + rfl + theorem Path.sderiv_path_injective {A B : α ↝ β} {hγ : γ < β} (h : A ↘ hγ = B ↘ hγ) : A = B := by cases h rfl +theorem Path.sderivBot_path_injective {β : Λ} {A B : α ↝ β} (h : A ↘. = B ↘.) : + A = B := by + cases h + rfl + theorem Path.deriv_left_injective {A B : α ↝ β} {C : β ↝ γ} (h : A ⇘ C = B ⇘ C) : A = B := by induction C with diff --git a/ConNF/Setup/PathEnumeration.lean b/ConNF/Setup/PathEnumeration.lean index 8aef9ee461..379da388af 100644 --- a/ConNF/Setup/PathEnumeration.lean +++ b/ConNF/Setup/PathEnumeration.lean @@ -22,6 +22,20 @@ variable [Params.{u}] namespace Enumeration +/-- A helper function for making relations with domain and codomain of the form `α ↝ ⊥ × X` +by defining it on each branch. -/ +def relWithPath {X Y : Type u} {α : TypeIndex} (f : α ↝ ⊥ → Rel X Y) : + Rel (α ↝ ⊥ × X) (α ↝ ⊥ × Y) := + λ x y ↦ x.1 = y.1 ∧ f x.1 x.2 y.2 + +theorem relWithPath_coinjective {X Y : Type u} {α : TypeIndex} {f : α ↝ ⊥ → Rel X Y} + (hf : ∀ A, (f A).Coinjective) : + (relWithPath f).Coinjective := by + constructor + rintro ⟨_, y₁⟩ ⟨_, y₂⟩ ⟨A, x⟩ ⟨rfl, h₁⟩ ⟨rfl, h₂⟩ + cases (hf A).coinjective h₁ h₂ + rfl + instance (X : Type u) (α β : TypeIndex) : Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β where deriv E A := E.invImage (λ x ↦ (x.1 ⇗ A, x.2)) @@ -68,7 +82,7 @@ instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] : smul π E := E.invImage (λ x ↦ (x.1, (π x.1)⁻¹ • x.2)) (mulAction_aux π) @[simp] -theorem smul_rel {X : Type _} {α : TypeIndex} [MulAction BasePerm X] +theorem smulPath_rel {X : Type _} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) (i : κ) (x : α ↝ ⊥ × X) : (π • E).rel i x ↔ E.rel i (x.1, (π x.1)⁻¹ • x.2) := Iff.rfl @@ -78,11 +92,11 @@ instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] : one_smul E := by ext i x · rfl - · rw [smul_rel, Tree.one_apply, inv_one, one_smul] + · rw [smulPath_rel, Tree.one_apply, inv_one, one_smul] mul_smul π₁ π₂ E := by ext i x · rfl - · rw [smul_rel, smul_rel, smul_rel, Tree.mul_apply, mul_inv_rev, mul_smul] + · rw [smulPath_rel, smulPath_rel, smulPath_rel, Tree.mul_apply, mul_inv_rev, mul_smul] theorem smul_eq_of_forall_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X] {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} @@ -100,7 +114,7 @@ theorem smul_eq_of_forall_smul_eq {X : Type _} {α : TypeIndex} [MulAction BaseP · intro hx have := h A x ⟨i, hx⟩ rw [← this] - rwa [smul_rel, inv_smul_smul] + rwa [smulPath_rel, inv_smul_smul] theorem smul_eq_of_mem_of_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X] {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} @@ -108,7 +122,6 @@ theorem smul_eq_of_mem_of_smul_eq {X : Type _} {α : TypeIndex} [MulAction BaseP π A • x = x := by obtain ⟨i, hx⟩ := hx have := congr_fun₂ (congr_arg rel h) i (A, x) - simp only [smul_rel, eq_iff_iff] at this have := E.rel_coinjective.coinjective hx (this.mpr hx) rw [Prod.mk.injEq, eq_inv_smul_iff] at this exact this.2 diff --git a/ConNF/Setup/StrPerm.lean b/ConNF/Setup/StrPerm.lean index 30772f29df..1e2974ea38 100644 --- a/ConNF/Setup/StrPerm.lean +++ b/ConNF/Setup/StrPerm.lean @@ -17,7 +17,7 @@ namespace ConNF variable [Params.{u}] {α : TypeIndex} -abbrev StrPerm : TypeIndex → Type _ := +abbrev StrPerm : TypeIndex → Type u := Tree BasePerm end ConNF diff --git a/ConNF/Setup/Support.lean b/ConNF/Setup/Support.lean index 515c1dbf13..9611e484f3 100644 --- a/ConNF/Setup/Support.lean +++ b/ConNF/Setup/Support.lean @@ -51,6 +51,41 @@ theorem ext {S T : BaseSupport} (h₁ : Sᴬ = Tᴬ) (h₂ : Sᴺ = Tᴺ) : S = cases h₂ rfl +instance : SMul BasePerm BaseSupport where + smul π S := ⟨π • Sᴬ, π • Sᴺ⟩ + +@[simp] +theorem smul_atoms (π : BasePerm) (S : BaseSupport) : + (π • S)ᴬ = π • Sᴬ := + rfl + +@[simp] +theorem smul_nearLitters (π : BasePerm) (S : BaseSupport) : + (π • S)ᴺ = π • Sᴺ := + rfl + +@[simp] +theorem smul_atoms_eq_of_smul_eq {π : BasePerm} {S : BaseSupport} + (h : π • S = S) : + π • Sᴬ = Sᴬ := by + rw [← smul_atoms, h] + +@[simp] +theorem smul_nearLitters_eq_of_smul_eq {π : BasePerm} {S : BaseSupport} + (h : π • S = S) : + π • Sᴺ = Sᴺ := by + rw [← smul_nearLitters, h] + +instance : MulAction BasePerm BaseSupport where + one_smul S := by + apply ext + · rw [smul_atoms, one_smul] + · rw [smul_nearLitters, one_smul] + mul_smul π₁ π₂ S := by + apply ext + · rw [smul_atoms, smul_atoms, smul_atoms, mul_smul] + · rw [smul_nearLitters, smul_nearLitters, smul_nearLitters, mul_smul] + end BaseSupport def baseSupportEquiv : BaseSupport ≃ Enumeration Atom × Enumeration NearLitter where @@ -157,6 +192,11 @@ instance {α : TypeIndex} : MulAction (StrPerm α) (Support α) where · rw [smul_atoms, smul_atoms, smul_atoms, mul_smul] · rw [smul_nearLitters, smul_nearLitters, smul_nearLitters, mul_smul] +@[simp] +theorem smul_derivBot {α : TypeIndex} (π : StrPerm α) (S : Support α) (A : α ↝ ⊥) : + (π • S) ⇘. A = π A • (S ⇘. A) := + rfl + end Support def supportEquiv {α : TypeIndex} : Support α ≃ diff --git a/ConNF/Setup/Tree.lean b/ConNF/Setup/Tree.lean index 32e6ffc864..022cf15ef3 100644 --- a/ConNF/Setup/Tree.lean +++ b/ConNF/Setup/Tree.lean @@ -74,6 +74,14 @@ theorem inv_apply [Group X] (T : Tree X α) (A : α ↝ ⊥) : T⁻¹ A = (T A)⁻¹ := rfl +/-- The partial order on the type of `α`-trees of `X` is given by "branchwise" comparison. -/ +instance partialOrder [PartialOrder X] : PartialOrder (Tree X α) := + Pi.partialOrder + +theorem le_iff [PartialOrder X] (T₁ T₂ : Tree X α) : + T₁ ≤ T₂ ↔ ∀ A, T₁ A ≤ T₂ A := + Iff.rfl + end Tree /-! diff --git a/blueprint/src/chapters/foa.tex b/blueprint/src/chapters/foa.tex index b390839beb..94353b69cf 100644 --- a/blueprint/src/chapters/foa.tex +++ b/blueprint/src/chapters/foa.tex @@ -169,6 +169,8 @@ \section{Structural approximations} \begin{definition} \uses{def:BaseApprox.LE,def:Tree} \label{def:StrApprox} + \lean{ConNF.StrApprox} + \leanok For a type index \( \beta \), a \emph{\( \beta \)-approximation} is a \( \beta \)-tree of base approximations. We define the partial order on \( \beta \)-approximations branchwise. We define an action of \( \beta \)-approximations \( \psi \) on \( \beta \)-supports \( S \) by \( (\psi(S))_A = \psi_A(S_A) \). @@ -176,6 +178,8 @@ \section{Structural approximations} \begin{definition} \uses{def:InflexiblePath} \label{def:Inflexible} + \lean{ConNF.Inflexible} + \leanok Let \( A \) be a \( \beta \)-extended type index. A litter \( L \) is \emph{\( A \)-inflexible} if there is an inflexible \( \beta \)-path \( I \) such that \( A = ((A_I)_{\varepsilon_I})_\bot \) and \( L = f_{\delta_I, \varepsilon_I}(t) \) for some \( t : \Tang_{\delta_I} \). The coderivative operation works in the obvious way. @@ -187,6 +191,8 @@ \section{Structural approximations} \begin{definition} \uses{def:StrApprox,def:Inflexible,def:smulApproxSupport} \label{def:StrApprox.Coherent} + \lean{ConNF.StrApprox.CoherentAt,ConNF.StrApprox.Coherent} + \leanok A \( \beta \)-approximation \( \psi \) is \emph{coherent} at \( (A, L_1, L_2) \) if: \begin{itemize} \item If \( L_1 \) is \( A \)-inflexible with inflexible \( \beta \)-path \( I = (\gamma, \delta, \varepsilon, B) \) and tangle \( t : \Tang_\delta \), then there is some \( \delta \)-allowable permutation \( \rho \) such that @@ -201,11 +207,14 @@ \section{Structural approximations} \begin{proposition}[adding orbits coherently] \uses{prop:BaseApprox.addOrbit,def:StrApprox.Coherent} \label{prop:StrApprox.addOrbit} + \lean{ConNF.StrApprox.addOrbit_coherent} + \leanok Suppose that \( \psi \) is an approximation and \( L : \mathbb Z \to \Litter \) is a function satisfying the hypotheses of \cref{prop:BaseApprox.addOrbit}. Let \( \chi \) be the extension produced by the structural version of this result.\footnote{We need the extension exactly as produced (as data), not an arbitrary extension satisfying the conclusion of the proposition.} If \( \psi \) is coherent, and is additionally coherent at \( (L(n), L(n+1)) \) for each integer \( n \), then \( \chi \) is coherent. \end{proposition} \begin{proof} + \leanok This proof just relies on the fact that if \( (\psi_B)_\delta(\supp(t)) = \rho(\supp(t)) \), then the same holds for every extension \( \chi \) of \( \psi \).\footnote{Maybe there's a better lemma to abstract out this idea for this and \cref{prop:StrApprox.chain}?} \end{proof} \begin{proposition}