Skip to content

Commit

Permalink
Maximal extensions
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Sep 11, 2024
1 parent 7ad902f commit cef9f5a
Show file tree
Hide file tree
Showing 9 changed files with 347 additions and 9 deletions.
104 changes: 103 additions & 1 deletion ConNF/Aux/Rel.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import Mathlib.Data.Rel
import Mathlib.Order.Chain

open Set
open scoped symmDiff
Expand Down Expand Up @@ -212,7 +213,7 @@ theorem preimage_subset_dom (r : Rel α β) (t : Set β) :
exact ⟨y, h⟩

theorem image_subset_codom (r : Rel α β) (s : Set α) :
r.image s ⊆ r.codom :=
r.image s ⊆ r.codom :=
r.inv.preimage_subset_dom s

theorem image_empty_of_disjoint_dom {r : Rel α β} {s : Set α} (h : Disjoint r.dom s) :
Expand Down Expand Up @@ -305,6 +306,107 @@ theorem sup_permutative {r s : Rel α α} (hr : r.Permutative) (hs : s.Permutati
sup_coinjective hr.toCoinjective hs.toCoinjective h⟩,
sup_codomEqDom hr.toCodomEqDom hs.toCodomEqDom⟩

@[simp]
theorem inv_le_inv_iff {r s : Rel α β} :
r.inv ≤ s.inv ↔ r ≤ s := by
constructor
· intro h x y
exact h y x
· intro h y x
exact h x y

@[simp]
theorem iSup_apply_iff {T : Type _} {r : T → Rel α β} (x : α) (y : β) :
(⨆ t, r t) x y ↔ ∃ t, r t x y := by
constructor
· rintro ⟨_, ⟨⟨_, ⟨_, t, rfl⟩, rfl⟩, rfl⟩, ht⟩
exact ⟨t, ht⟩
· rintro ⟨t, ht⟩
exact ⟨_, ⟨⟨_, ⟨_, t, rfl⟩, rfl⟩, rfl⟩, ht⟩

@[simp]
theorem biSup_apply_iff {T : Type _} {r : T → Rel α β} {s : Set T} (x : α) (y : β) :
(⨆ t ∈ s, r t) x y ↔ ∃ t ∈ s, r t x y := by
have := iSup_apply_iff (r := λ t : s ↦ r t) x y
simp only [iSup_subtype'', Subtype.exists, exists_prop] at this
exact this

theorem iSup_dom {T : Type _} (r : T → Rel α β) :
(⨆ t, r t).dom = ⋃ t, (r t).dom := by
simp only [dom, iSup_apply_iff, Set.ext_iff, mem_setOf_eq, mem_iUnion]
exact λ x ↦ exists_comm

theorem biSup_dom {T : Type _} (r : T → Rel α β) (s : Set T) :
(⨆ t ∈ s, r t).dom = ⋃ t ∈ s, (r t).dom := by
have := iSup_dom (λ t : s ↦ r t)
rwa [iSup_subtype'', iUnion_coe_set] at this

theorem isChain_inv {T : Type _} {r : T → Rel α β} (h : IsChain (· ≤ ·) (Set.range r)) :
IsChain (· ≤ ·) (Set.range (λ t ↦ (r t).inv)) := by
rintro _ ⟨t₁, rfl⟩ _ ⟨t₂, rfl⟩ _
dsimp only
rw [inv_le_inv_iff, inv_le_inv_iff]
apply h.total ⟨t₁, rfl⟩ ⟨t₂, rfl⟩

theorem iSup_inv {T : Type _} {r : T → Rel α β} :
(⨆ t, (r t).inv) = (⨆ t, r t).inv := by
apply le_antisymm <;>
· rintro x y h
simp only [inv, iSup_apply_iff, flip] at h ⊢
exact h

theorem iSup_injective_of_isChain {T : Type _} {r : T → Rel α β}
(h₁ : ∀ t, (r t).Injective) (h₂ : IsChain (· ≤ ·) (Set.range r)) :
(⨆ t, r t).Injective := by
constructor
intro x₁ x₂ y hx₁ hx₂
rw [iSup_apply_iff] at hx₁ hx₂
obtain ⟨t₁, hx₁⟩ := hx₁
obtain ⟨t₂, hx₂⟩ := hx₂
obtain (h | h) := h₂.total ⟨t₁, rfl⟩ ⟨t₂, rfl⟩
· exact (h₁ t₂).injective (h x₁ y hx₁) hx₂
· exact (h₁ t₁).injective hx₁ (h x₂ y hx₂)

theorem iSup_coinjective_of_isChain {T : Type _} {r : T → Rel α β}
(h₁ : ∀ t, (r t).Coinjective) (h₂ : IsChain (· ≤ ·) (Set.range r)) :
(⨆ t, r t).Coinjective := by
have := iSup_injective_of_isChain (r := λ t ↦ (r t).inv) ?_ (isChain_inv h₂)
· rwa [iSup_inv, inv_injective_iff] at this
· intro t
rw [inv_injective_iff]
exact h₁ t

theorem iSup_codomEqDom_of_isChain {T : Type _} {r : T → Rel α α} (h : ∀ t, (r t).CodomEqDom) :
(⨆ t, r t).CodomEqDom := by
simp only [codomEqDom_iff'] at h ⊢
simp only [iSup_apply_iff]
constructor
· rintro x y ⟨t, ht⟩
obtain ⟨u, hu⟩ := (h t).1 x y ht
exact ⟨u, t, hu⟩
· rintro x y ⟨t, ht⟩
obtain ⟨u, hu⟩ := (h t).2 x y ht
exact ⟨u, t, hu⟩

theorem iSup_oneOne_of_isChain {T : Type _} {r : T → Rel α β}
(h₁ : ∀ t, (r t).OneOne) (h₂ : IsChain (· ≤ ·) (Set.range r)) :
(⨆ t, r t).OneOne :=
⟨iSup_injective_of_isChain (λ t ↦ (h₁ t).toInjective) h₂,
iSup_coinjective_of_isChain (λ t ↦ (h₁ t).toCoinjective) h₂⟩

theorem iSup_permutative_of_isChain {T : Type _} {r : T → Rel α α}
(h₁ : ∀ t, (r t).Permutative) (h₂ : IsChain (· ≤ ·) (Set.range r)) :
(⨆ t, r t).Permutative :=
⟨iSup_oneOne_of_isChain (λ t ↦ (h₁ t).toOneOne) h₂,
iSup_codomEqDom_of_isChain (λ t ↦ (h₁ t).toCodomEqDom)⟩

theorem biSup_permutative_of_isChain {T : Type _} {r : T → Rel α α} {s : Set T}
(h₁ : ∀ t ∈ s, (r t).Permutative) (h₂ : IsChain (· ≤ ·) (r '' s)) :
(⨆ t ∈ s, r t).Permutative := by
have := iSup_permutative_of_isChain (T := s) (λ t ↦ h₁ t t.prop) ?_
· rwa [iSup_subtype] at this
· rwa [image_eq_range] at h₂

-- Compare Mathlib.Data.Rel and Mathlib.Logic.Relator.

end Rel
90 changes: 85 additions & 5 deletions ConNF/FOA/Approximates.lean
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,11 @@ def Approximates (ψ : StrApprox β) (ρ : AllPerm β) : Prop :=
def ExactlyApproximates (ψ : StrApprox β) (ρ : AllPerm β) : Prop :=
∀ A, (ψ A).ExactlyApproximates (ρᵁ A)

theorem ExactlyApproximates.toApproximates {ψ : StrApprox β} {ρ : AllPerm β}
(h : ψ.ExactlyApproximates ρ) :
ψ.Approximates ρ :=
λ A ↦ (h A).toApproximates

def FreedomOfAction (β : TypeIndex) [LeLevel β] : Prop :=
∀ ψ : StrApprox β, ψ.Coherent → ∃ ρ, ψ.ExactlyApproximates ρ

Expand Down Expand Up @@ -187,8 +192,8 @@ theorem smul_support_zpow {ψ : StrApprox β} {ρ : AllPerm β} (h : ψ.Approxim
exact hLN B _ hN

theorem addInflexible'_coherent {ψ : StrApprox β} {A : β ↝ ⊥}
{P : InflexiblePath β} {t : Tangle P.δ} {hA : A = P.A ↘ P.hε ↘.}
{ρ : AllPerm P.δ} {hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ}
{P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.)
{ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ)
{hL : ∀ n : ℤ, fuzz P.hδε (ρ ^ n • t) ∉ (ψ A)ᴸ.dom}
(hψ : ψ.Coherent)
(hLA : ∀ B, ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴬ.dom)
Expand All @@ -207,9 +212,9 @@ theorem addInflexible'_coherent {ψ : StrApprox β} {A : β ↝ ⊥}
· rw [add_comm, zpow_add, zpow_one, mul_smul]

theorem mem_dom_of_inflexible {ψ : StrApprox β} {A : β ↝ ⊥} {L : Litter}
{P : InflexiblePath β} {t : Tangle P.δ} {hA : A = P.A ↘ P.hε ↘.} {ht : L = fuzz P.hδε t}
{ρ : AllPerm P.δ} {hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ}
{n : ℤ} {hL : fuzz P.hδε (ρ ^ n • t) ∈ (ψ A)ᴸ.dom}
{P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.) (ht : L = fuzz P.hδε t)
{ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ)
{n : ℤ} (hL : fuzz P.hδε (ρ ^ n • t) ∈ (ψ A)ᴸ.dom)
(hψ : ψ.Coherent)
(hLA : ∀ B, ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴬ.dom)
(hLN : ∀ B, ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴺ.dom) :
Expand Down Expand Up @@ -247,6 +252,81 @@ theorem mem_dom_of_inflexible {ψ : StrApprox β} {A : β ↝ ⊥} {L : Litter}
· simp only [Tree.sderiv_apply, Tree.deriv_apply, Path.deriv_scoderiv]
exact hLN

open scoped Classical in
def addInflexible (ψ : StrApprox β) (A : β ↝ ⊥)
(P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : StrApprox β :=
if hL : ∀ n : ℤ, fuzz P.hδε (ρ ^ n • t) ∉ (ψ A)ᴸ.dom then ψ.addInflexible' P t ρ hL else ψ

theorem le_addInflexible (ψ : StrApprox β) (A : β ↝ ⊥)
(P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) :
ψ ≤ ψ.addInflexible A P t ρ := by
rw [addInflexible]
split_ifs
· exact le_addOrbit
· exact le_rfl

theorem addInflexible_coherent {ψ : StrApprox β} {A : β ↝ ⊥}
{P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.)
{ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ)
(hψ : ψ.Coherent)
(hLA : ∀ B, ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴬ.dom)
(hLN : ∀ B, ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴺ.dom) :
(ψ.addInflexible A P t ρ).Coherent := by
rw [addInflexible]
split_ifs
· exact addInflexible'_coherent hA hρ hψ hLA hLN
· exact hψ

theorem mem_addInflexible_dom {ψ : StrApprox β} {A : β ↝ ⊥} {L : Litter}
{P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ P.hε ↘.) (hL : L = fuzz P.hδε t)
{ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ P.hδ) ρ)
(hψ : ψ.Coherent)
(hLA : ∀ B, ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴬ.dom)
(hLN : ∀ B, ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴺ.dom) :
L ∈ (ψ.addInflexible A P t ρ A)ᴸ.dom := by
rw [addInflexible]
split_ifs with hL'
· rw [addInflexible', addOrbit_apply, BaseApprox.addOrbit_litters, Rel.sup_dom,
BaseApprox.addOrbitLitters_dom]
right
use 0
simp only [zpow_zero, one_smul, hL]
· push_neg at hL'
obtain ⟨n, hn⟩ := hL'
exact mem_dom_of_inflexible hA hL hρ hn hψ hLA hLN

theorem exists_extension_of_minimal (ψ : StrApprox β) (A : β ↝ ⊥) (L : Litter) (hψ : ψ.Coherent)
(foa : ∀ δ < β, [LeLevel δ] → FreedomOfAction δ)
(hLA : ∀ B, ∀ a, pos a < pos L → a ∈ (ψ B)ᴬ.dom)
(hLN : ∀ B, ∀ N, pos N < pos L → N ∈ (ψ B)ᴺ.dom) :
∃ χ ≥ ψ, χ.Coherent ∧ L ∈ (χ A)ᴸ.dom := by
obtain (⟨P, t, hA, ht⟩ | hL) := inflexible_cases A L
· obtain ⟨ρ, hρ⟩ := foa P.δ (P.hδ.trans_le P.A.le) (ψ ⇘ (P.A ↘ P.hδ)) (hψ.comp (P.A ↘ P.hδ))
have h₁ : ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴬ.dom := by
intro B a ha
apply hLA
rw [ht]
exact (pos_atom_lt_pos t B a ha).trans (pos_fuzz P.hδε t)
have h₂ : ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ P.hδ ⇘ B))ᴺ.dom := by
intro B N hN
apply hLN
rw [ht]
exact (pos_nearLitter_lt_pos t B N hN).trans (pos_fuzz P.hδε t)
refine ⟨addInflexible ψ A P t ρ, le_addInflexible ψ A P t ρ, ?_, ?_⟩
· refine addInflexible_coherent hA ?_ hψ h₁ h₂
rw [Tree.deriv_sderiv]
exact hρ.toApproximates
· refine mem_addInflexible_dom hA ht ?_ hψ h₁ h₂
rw [Tree.deriv_sderiv]
exact hρ.toApproximates
· by_cases hL' : L ∈ (ψ A)ᴸ.dom
· use ψ
· refine ⟨addFlexible ψ A L hL', le_addOrbit, addFlexible_coherent hψ hL, ?_⟩
rw [addFlexible, addOrbit_apply, BaseApprox.addOrbit_litters, Rel.sup_dom,
BaseApprox.addOrbitLitters_dom]
right
use 0

end StrApprox

end ConNF
53 changes: 53 additions & 0 deletions ConNF/FOA/BaseApprox.lean
Original file line number Diff line number Diff line change
Expand Up @@ -411,6 +411,16 @@ def addOrbitLitters (f : ℤ → Litter) :
Rel Litter Litter :=
λ L₁ L₂ ↦ ∃ n : ℤ, L₁ = f n ∧ L₂ = f (n + 1)

@[simp]
theorem addOrbitLitters_dom (f : ℤ → Litter) :
(addOrbitLitters f).dom = Set.range f := by
ext L
constructor
· rintro ⟨_, n, rfl, rfl⟩
exact ⟨n, rfl⟩
· rintro ⟨n, rfl⟩
exact ⟨_, n, rfl, rfl⟩

theorem addOrbitLitters_codomEqDom (f : ℤ → Litter) :
(addOrbitLitters f).CodomEqDom := by
constructor
Expand Down Expand Up @@ -468,6 +478,49 @@ theorem le_addOrbit :

end addOrbit

theorem upperBound_exceptions_small (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) (L : Litter) :
Small (Lᴬ ∩ (⨆ ψ ∈ c, ψ.exceptions).dom) := by
rw [biSup_dom]
obtain (rfl | ⟨ψ, hψ⟩) := c.eq_empty_or_nonempty
· simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty, inter_empty, small_empty]
· suffices ⋃ ψ ∈ c, ψ.exceptions.dom = ψ.exceptions.dom by
rw [this]
exact ψ.exceptions_small L
ext a
rw [mem_iUnion₂]
constructor
· rintro ⟨χ, hχ₁, hχ₂⟩
obtain (h | h) := hc.total hψ hχ₁
· rwa [h.1]
· rwa [← h.1]
· intro h
exact ⟨ψ, hψ, h⟩

/-- An upper bound for a chain of base approximations. -/
def upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) : BaseApprox where
exceptions := ⨆ ψ ∈ c, ψ.exceptions
litters := ⨆ ψ ∈ c, ψᴸ
exceptions_permutative := biSup_permutative_of_isChain
(λ ψ _ ↦ ψ.exceptions_permutative) (hc.image _ _ (λ _ _ h ↦ h.1.le))
litters_permutative' := biSup_permutative_of_isChain
(λ ψ _ ↦ ψ.litters_permutative) (hc.image _ _ (λ _ _ h ↦ h.2))
exceptions_small := upperBound_exceptions_small c hc

theorem le_upperBound (c : Set BaseApprox) (hc : IsChain (· ≤ ·) c) :
∀ ψ ∈ c, ψ ≤ upperBound c hc := by
intro ψ hψ
constructor
· ext a₁ a₂
simp only [upperBound, biSup_dom, biSup_apply_iff]
constructor
· intro h
exact ⟨ψ, hψ, h⟩
· rintro ⟨χ, hχ₁, hχ₂⟩
obtain (h | h) := hc.total hψ hχ₁
· rwa [h.1]
· rwa [← h.1]
· exact le_biSup _ hψ

end BaseApprox

end ConNF
64 changes: 64 additions & 0 deletions ConNF/FOA/StrApprox.lean
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,28 @@ theorem smul_support_smul_eq_iff (ψ : StrApprox β) (S : Support β) (π : StrP
rw [inv_smul_smul] at this
rw [this]

/-- An upper bound for a chain of approximations. -/
def upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) : StrApprox β :=
λ A ↦ BaseApprox.upperBound ((· A) '' c) (hc.image _ _ (λ _ _ h ↦ h A))

theorem le_upperBound (c : Set (StrApprox β)) (hc : IsChain (· ≤ ·) c) :
∀ ψ ∈ c, ψ ≤ upperBound c hc :=
λ ψ hψ _ ↦ BaseApprox.le_upperBound _ _ _ ⟨ψ, hψ, rfl⟩

theorem exists_isMax (ψ : StrApprox β) : ∃ χ ≥ ψ, IsMax χ := by
have := zorn_le₀ {χ | ψ ≤ χ} ?_
· obtain ⟨χ, hχ₁, hχ₂⟩ := this
refine ⟨χ, hχ₁, ?_⟩
intro χ' h
exact hχ₂ (hχ₁.trans h) h
· intro c hc₁ hc₂
obtain rfl | hc₃ := c.eq_empty_or_nonempty
· refine ⟨ψ, ?_, ?_⟩
· exact le_refl ψ
· simp only [Set.mem_empty_iff_false, false_implies, implies_true]
· obtain ⟨ψ', hψ'⟩ := hc₃
exact ⟨upperBound c hc₂, (hc₁ hψ').trans (le_upperBound c hc₂ ψ' hψ'), le_upperBound c hc₂⟩

end StrApprox

@[ext]
Expand All @@ -104,6 +126,14 @@ structure InflexiblePath (β : TypeIndex) where
hδε : δ ≠ ε
A : β ↝ γ

instance {β β' : TypeIndex} : Coderivative (InflexiblePath β) (InflexiblePath β') β' β where
coderiv P B := ⟨P.γ, P.δ, P.ε, P.hδ, P.hε, P.hδε, B ⇘ P.A⟩

@[simp]
theorem InflexiblePath.coderiv_A {β β' : TypeIndex} (P : InflexiblePath β) (B : β' ↝ β) :
(P ⇗ B).A = B ⇘ P.A :=
rfl

variable [Level] [CoherentData]

instance [LeLevel β] (P : InflexiblePath β) : LeLevel P.γ :=
Expand All @@ -128,6 +158,14 @@ theorem not_inflexible_iff [LeLevel β] (A : β ↝ ⊥) (L : Litter) :
push_neg
rfl

theorem inflexible_deriv [LeLevel β] {A : β ↝ ⊥} {L : Litter} (h : Inflexible A L)
{β' : TypeIndex} [LeLevel β'] (B : β' ↝ β) :
Inflexible (B ⇘ A) L := by
obtain ⟨P, t, hA, ht⟩ := h
refine ⟨P ⇗ B, t, ?_, ht⟩
rw [hA]
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 _
Expand Down Expand Up @@ -291,6 +329,32 @@ theorem addOrbit_coherent [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {f :
intro hL
exact (hψ B L₁ L₂ hL).mono le_addOrbit

theorem Coherent.comp [LeLevel β] {ψ : StrApprox β} (hψ : ψ.Coherent)
{γ : TypeIndex} [LeLevel γ] (A : β ↝ γ) :
Coherent (ψ ⇘ A) := by
intro B L₁ L₂ h
specialize hψ (A ⇘ B) L₁ L₂ h
constructor
· intro P t hA ht
have := hψ.inflexible (P ⇗ A) t ?_ ht
· obtain ⟨ρ, hρ₁, hρ₂⟩ := this
refine ⟨ρ, ?_, hρ₂⟩
rwa [InflexiblePath.coderiv_A, ← Tree.deriv_deriv] at hρ₁
· rw [hA]
rfl
· intro hL₁ hL₂
obtain (hL₁' | hL₁') := inflexible_cases (A ⇘ B) L₁
· obtain ⟨P, t, rfl, ht⟩ := hL₂
obtain ⟨P', t', hA', ht'⟩ := hL₁'
suffices P' = P ⇗ A by
cases this
cases hL₁ ⟨P, t', rfl, ht'⟩
rw [coherentAt_inflexible hA' ht'] at hψ
obtain ⟨ρ, hρ₁, hρ₂⟩ := hψ
rw [Path.deriv_sderivBot, Path.deriv_sderiv] at hA'
exact inflexiblePath_subsingleton hA' rfl hρ₂ ht
· cases hψ.flexible hL₁' (inflexible_deriv hL₂ A)

end StrApprox

end ConNF
Loading

0 comments on commit cef9f5a

Please sign in to comment.