Coherence

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

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

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 :=

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