Headway on existence of flexible approximations

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

ConNF.lean

@@ -8,6 +8,7 @@ import ConNF.Aux.WellOrder
 import ConNF.FOA.Approximates
 import ConNF.FOA.BaseAction
 import ConNF.FOA.BaseApprox
+import ConNF.FOA.StrAction
 import ConNF.FOA.StrApprox
 import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm

ConNF/Aux/PermutativeExtension.lean

@@ -8,20 +8,21 @@ namespace Rel
 
 variable {α β : Type _}
 
+/-- TODO: Fix the paper version of this. -/
 structure OrbitRestriction (s : Set α) (β : Type _) where
   sandbox : Set α
   sandbox_disjoint : Disjoint s sandbox
   categorise : α → β
   catPerm : Equiv.Perm β
-  le_card_categorise (b : β) : max ℵ₀ (max #s #sandbox) ≤ #(sandbox ∩ categorise ⁻¹' {b} : Set α)
+  le_card_categorise (b : β) : max ℵ₀ #s ≤ #(sandbox ∩ categorise ⁻¹' {b} : Set α)
 
 theorem le_card_categorise {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) :
     #((r.dom ∪ r.codom : Set α) × ℕ) ≤ #(R.sandbox ∩ R.categorise ⁻¹' {b} : Set α) := by
   rw [Cardinal.mk_prod, Cardinal.lift_id', Cardinal.mk_eq_aleph0 ℕ, Cardinal.lift_aleph0]
   refine le_trans ?_ (R.le_card_categorise b)
   apply mul_le_of_le
   · exact le_max_left ℵ₀ _
-  · simp only [le_max_iff, le_refl, true_or, or_true]
+  · exact le_max_right ℵ₀ _
   · exact le_max_left ℵ₀ _
 
 def catInj {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (b : β) :

ConNF/Aux/Rel.lean

@@ -43,6 +43,10 @@ structure CodomEqDom (r : Rel α α) : Prop where
 @[mk_iff]
 structure Permutative (r : Rel α α) extends r.OneOne, r.CodomEqDom : Prop
 
+theorem CodomEqDom.dom_union_codom {r : Rel α α} (h : r.CodomEqDom) :
+    r.dom ∪ r.codom = r.dom := by
+  rw [h.codom_eq_dom, union_self]
+
 theorem CodomEqDom.mem_dom {r : Rel α α} (h : r.CodomEqDom) {x y : α} (hxy : r x y) :
     y ∈ r.dom := by
   rw [← h.codom_eq_dom]
@@ -470,6 +474,10 @@ theorem toEquiv_rel (r : Rel α β) (hr : r.Bijective) (a : α) :
     r a (r.toEquiv hr a) :=
   toFunction_rel r hr.toFunctional a
 
+theorem toEquiv_eq_iff (r : Rel α β) (hr : r.Bijective) (a : α) (b : β) :
+    r.toEquiv hr a = b ↔ r a b :=
+  toFunction_eq_iff r hr.toFunctional a b
+
 theorem toFunction_image (r : Rel α β) (hr : r.Functional) (s : Set α) :
     r.toFunction hr '' s = r.image s := by
   ext y

ConNF/FOA/BaseAction.lean

@@ -155,6 +155,18 @@ theorem litters_coinjective (ξ : BaseAction) : ξᴸ.Coinjective := by
   obtain ⟨N₄, N₂, h₄, rfl, h₂⟩ := h₂
   exact (litter_eq_litter_iff h₁ h₂).mp (h₃.trans h₄.symm)
 
+theorem litters_dom_small (ξ : BaseAction) : Small ξᴸ.dom := by
+  have := mk_le_of_surjective (f := λ (N : ξᴺ.dom) ↦
+      (⟨N.valᴸ, N.prop.chooseᴸ, ⟨N.prop.choose_spec⟩⟩ : ξᴸ.dom)) ?_
+  · exact this.trans_lt ξ.nearLitters_dom_small
+  · rintro ⟨L₁, L₂, hL⟩
+    rw [litters_iff] at hL
+    obtain ⟨N₁, N₂, rfl, rfl, h⟩ := hL
+    exact ⟨⟨N₁, N₂, h⟩, rfl⟩
+
+theorem litters_codom_small (ξ : BaseAction) : Small ξᴸ.codom :=
+  small_codom_of_small_dom ξ.litters_coinjective ξ.litters_dom_small
+
 @[simp]
 theorem inv_litters (ξ : BaseAction) : ξ⁻¹ᴸ = ξᴸ.inv := by
   ext L₁ L₂

ConNF/FOA/StrAction.lean

@@ -0,0 +1,162 @@
+import ConNF.Aux.PermutativeExtension
+import ConNF.FOA.StrApprox
+import ConNF.FOA.BaseAction
+
+/-!
+# Structural actions
+
+In this file, we define structural actions.
+
+## Main declarations
+
+* `ConNF.StrAction`: Structural actions.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+open scoped symmDiff
+
+namespace ConNF
+namespace BaseAction
+
+variable [Params.{u}]
+
+structure FlexApprox [Level] [CoherentData] {β : TypeIndex} [LeLevel β]
+    (A : β ↝ ⊥) (ξ : BaseAction) (ψ : BaseApprox) : Prop where
+  atoms_le_atoms : ξᴬ ≤ ψ.exceptions
+  flexible_of_mem_dom {L : Litter} : L ∈ ψᴸ.dom → ¬Inflexible A L
+  litters_of_flexible {L₁ L₂ : Litter} : ¬Inflexible A L₁ → ξᴸ L₁ L₂ → ψᴸ L₁ L₂
+  symmDiff_subset_dom {N : NearLitter} : N ∈ ξᴺ.dom → Nᴬ ∆ Nᴸᴬ ⊆ ψᴬ.dom
+  symmDiff_subset_codom {N : NearLitter} : N ∈ ξᴺ.codom → Nᴬ ∆ Nᴸᴬ ⊆ ψᴬ.codom
+  mem_iff_mem {N₁ N₂ : NearLitter} : ξᴺ N₁ N₂ → ∀ a₂,
+    a₂ ∈ N₂ᴬ ↔ (∃ a₁ ∈ N₁ᴬ, ψ.exceptions a₁ a₂) ∨ (a₂ ∉ ψ.exceptions.dom ∧ a₂ᴸ = N₂ᴸ)
+
+section FlexApprox
+
+theorem card_litter_dom_compl {ξ : BaseAction} : #((ξᴸ.dom ∪ ξᴸ.codom)ᶜ : Set Litter) = #μ := by
+  have : Infinite Litter := by
+    rw [infinite_iff, card_litter]
+    exact aleph0_le_of_isSuccLimit μ_isStrongLimit.isSuccLimit
+  refine (mk_compl_of_infinite _ ?_).trans card_litter
+  rw [card_litter]
+  apply (mk_union_le _ _).trans_lt
+  apply add_lt_of_lt (aleph0_le_of_isSuccLimit μ_isStrongLimit.isSuccLimit)
+  · exact ξ.litters_dom_small.trans κ_lt_μ
+  · exact ξ.litters_codom_small.trans κ_lt_μ
+
+theorem litter_dom_compl_infinite {ξ : BaseAction} : (ξᴸ.dom ∪ ξᴸ.codom)ᶜ.Infinite := by
+  rw [← Set.infinite_coe_iff, infinite_iff, card_litter_dom_compl]
+  exact aleph0_le_of_isSuccLimit μ_isStrongLimit.isSuccLimit
+
+def littersExtension' (ξ : BaseAction) : Rel Litter Litter :=
+  ξᴸ.permutativeExtension' ξ.litters_oneOne (ξᴸ.dom ∪ ξᴸ.codom)ᶜ litter_dom_compl_infinite
+    (ξ.litters_dom_small.le.trans (κ_le_μ.trans card_litter_dom_compl.symm.le))
+    disjoint_compl_right
+
+theorem le_littersExtension' (ξ : BaseAction) :
+    ξᴸ ≤ ξ.littersExtension' :=
+  Rel.le_permutativeExtension'
+
+theorem littersExtension'_permutative (ξ : BaseAction) :
+    ξ.littersExtension'.Permutative :=
+  Rel.permutativeExtension'_permutative
+
+def littersExtension (ξ : BaseAction) : Rel Litter Litter :=
+  ξ.littersExtension' ⊔ (λ L₁ L₂ ↦ L₁ = L₂ ∧ L₁ ∉ ξ.littersExtension'.dom)
+
+theorem le_littersExtension (ξ : BaseAction) :
+    ξᴸ ≤ ξ.littersExtension :=
+  ξ.le_littersExtension'.trans le_sup_left
+
+theorem littersExtension_bijective (ξ : BaseAction) :
+    ξ.littersExtension.Bijective := by
+  constructor <;> constructor <;> constructor
+  · rintro L₁ L₂ L₃ (h | ⟨rfl, h⟩) (h' | ⟨rfl, h'⟩)
+    · exact ξ.littersExtension'_permutative.coinjective h h'
+    · cases h' ⟨L₁, h⟩
+    · cases h ⟨L₂, h'⟩
+    · rfl
+  · intro L
+    by_cases h : L ∈ ξ.littersExtension'.dom
+    · obtain ⟨L', h⟩ := h
+      exact ⟨L', Or.inl h⟩
+    · exact ⟨L, Or.inr ⟨rfl, h⟩⟩
+  · rintro L₁ L₂ L₃ (h | ⟨rfl, h⟩) (h' | ⟨rfl, h'⟩)
+    · exact ξ.littersExtension'_permutative.injective h h'
+    · cases h' (ξ.littersExtension'_permutative.mem_dom h)
+    · cases h (ξ.littersExtension'_permutative.mem_dom h')
+    · rfl
+  · intro L
+    by_cases h : L ∈ ξ.littersExtension'.dom
+    · obtain ⟨L', h⟩ := ξ.littersExtension'_permutative.codom_eq_dom ▸ h
+      exact ⟨L', Or.inl h⟩
+    · exact ⟨L, Or.inr ⟨rfl, h⟩⟩
+
+def litterPerm (ξ : BaseAction) : Equiv.Perm Litter :=
+  ξ.littersExtension.toEquiv ξ.littersExtension_bijective
+
+theorem litterPerm_eq {ξ : BaseAction} {L₁ L₂ : Litter} (h : ξᴸ L₁ L₂) :
+    ξ.litterPerm L₁ = L₂ := by
+  apply (ξ.littersExtension.toEquiv_eq_iff ξ.littersExtension_bijective L₁ L₂).mpr
+  apply le_littersExtension
+  exact h
+
+def insideAll (ξ : BaseAction) : Set Atom :=
+  {a | ∀ N, (N ∈ ξᴺ.dom ∨ N ∈ ξᴺ.codom) → Nᴸ = aᴸ → a ∈ Nᴬ}
+
+theorem diff_insideAll_small (ξ : BaseAction) (L : Litter) :
+    Small (Lᴬ \ ξ.insideAll) := by
+  have : Lᴬ \ ξ.insideAll ⊆ (⋃ N ∈ {N | (N ∈ ξᴺ.dom ∨ N ∈ ξᴺ.codom) ∧ Nᴸ = L}, Lᴬ \ Nᴬ) := by
+    rintro a ⟨rfl, ha⟩
+    rw [insideAll, Set.mem_setOf_eq] at ha
+    push_neg at ha
+    obtain ⟨N, hN, h₁, h₂⟩ := ha
+    exact Set.mem_biUnion (x := N) ⟨hN, h₁⟩ ⟨rfl, h₂⟩
+  apply Small.mono this
+  apply small_biUnion
+  · apply (small_union ξ.nearLitters_dom_small ξ.nearLitters_codom_small).mono
+    exact Set.sep_subset _ _
+  · rintro N ⟨_, rfl⟩
+    exact N.diff_small'
+
+theorem card_insideAll_inter (ξ : BaseAction) (L : Litter) :
+    #(ξ.insideAll \ (ξᴬ.dom ∪ ξᴬ.codom) ∩ Lᴬ : Set Atom) = #κ := by
+  apply le_antisymm
+  · refine le_of_le_of_eq ?_ L.card_atoms
+    apply mk_le_mk_of_subset
+    exact Set.inter_subset_right
+  · rw [← not_lt]
+    intro h
+    apply L.atoms_not_small
+    apply (small_union (small_union (small_union h (ξ.diff_insideAll_small L))
+      ξ.atoms_dom_small) ξ.atoms_codom_small).mono
+    intro a ha
+    simp only [Set.mem_union, Set.mem_inter_iff, Set.mem_diff, not_or, mem_litter_atoms_iff]
+    tauto
+
+def orbitRestriction (ξ : BaseAction) : Rel.OrbitRestriction (ξᴬ.dom ∪ ξᴬ.codom) Litter where
+  sandbox := ξ.insideAll \ (ξᴬ.dom ∪ ξᴬ.codom)
+  sandbox_disjoint := Set.disjoint_sdiff_left.symm
+  categorise a := aᴸ
+  catPerm := ξ.litterPerm
+  le_card_categorise L := by
+    change _ ≤ #(ξ.insideAll \ (ξᴬ.dom ∪ ξᴬ.codom) ∩ Lᴬ : Set Atom)
+    rw [card_insideAll_inter, max_le_iff]
+    constructor
+    · exact κ_isRegular.aleph0_le
+    · apply (mk_union_le _ _).trans
+      apply add_le_of_le κ_isRegular.aleph0_le
+      · exact ξ.atoms_dom_small.le
+      · exact ξ.atoms_codom_small.le
+
+def atomPerm (ξ : BaseAction) : Rel Atom Atom :=
+  ξᴬ.permutativeExtension ξ.orbitRestriction
+
+variable [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {A : β ↝ ⊥} {ξ : BaseAction}
+
+end FlexApprox
+
+end BaseAction
+end ConNF