Prove exists_combination_raisedSingleton

Signed-off-by: Sky Wilshaw <zeramorphic@proton.me>

ConNF/Counting/CodingFunction.lean

@@ -99,6 +99,16 @@ theorem ext {χ₁ χ₂ : CodingFunction β} (S : Support β) (x : TSet β)
   · apply ext_aux h₁ h₂
   · apply ext_aux h₂ h₁
 
+theorem exists_allPerm_of_rel {χ : CodingFunction β} {S T : Support β} {x y : TSet β}
+    (h₁ : χ.rel S x) (h₂ : χ.rel T y) :
+    ∃ ρ : AllPerm β, ρᵁ • S = T ∧ ρ • x = y := by
+  have := χ.orbit_eq_of_mem_dom ⟨x, h₁⟩ ⟨y, h₂⟩
+  rw [Support.orbit_eq_iff] at this
+  obtain ⟨ρ, hρ⟩ := this
+  refine ⟨ρ, hρ, ?_⟩
+  have := χ.smul_rel h₁ ρ
+  exact χ.rel_coinjective.coinjective this (hρ ▸ h₂)
+
 end CodingFunction
 
 def Tangle.code (t : Tangle β) : CodingFunction β where

ConNF/Counting/Recode.lean

@@ -5,11 +5,12 @@ import ConNF.Counting.CodingFunction
 # Recoding
 
 In this file, we show that all coding functions of level `β > γ` can be expressed in terms of a set
-of `γ`-coding functions.
+of a particular class of `γ`-coding functions, called *raised* coding functions.
 
 ## Main declarations
 
-* `ConNF.foo`: Something new.
+* `ConNF.exists_combination_raisedSingleton`: Each coding function at a level `β > γ` can be
+  expressed in terms of a set of `γ`-coding functions and a `β`-support orbit.
 -/
 
 noncomputable section
@@ -23,7 +24,7 @@ variable [Params.{u}] [Level] [CoherentData] {β γ : Λ} [LeLevel β] [LeLevel
     (hγ : (γ : TypeIndex) < β)
 
 def Combination (x : TSet β) (S : Support β) (χs : Set (CodingFunction β)) : Prop :=
-  ∀ y : TSet γ, y ∈[hγ] x ↔ ∃ χ ∈ χs, ∃ T z, χ.rel T z ∧ S ≤ T ∧ y ∈[hγ] z
+  ∀ y : TSet γ, y ∈[hγ] x ↔ ∃ χ ∈ χs, ∃ T z, χ.rel T z ∧ S.Subsupport T ∧ y ∈[hγ] z
 
 theorem combination_unique {x₁ x₂ : TSet β} {S : Support β} {χs : Set (CodingFunction β)}
     (hx₁ : Combination hγ x₁ S χs) (hx₂ : Combination hγ x₂ S χs) :
@@ -39,11 +40,11 @@ theorem Combination.smul {x : TSet β} {S : Support β} {χs : Set (CodingFuncti
   rw [TSet.mem_smul_iff, h]
   constructor
   · rintro ⟨χ, hχ, T, z, hTz, hST, hyz⟩
-    refine ⟨χ, hχ, ρᵁ • T, ρ • z, χ.smul_rel hTz ρ, Support.smul_le_smul hST ρᵁ, ?_⟩
+    refine ⟨χ, hχ, ρᵁ • T, ρ • z, χ.smul_rel hTz ρ, Support.smul_subsupport_smul hST ρᵁ, ?_⟩
     rwa [TSet.mem_smul_iff]
   · rintro ⟨χ, hχ, T, z, hTz, hST, hyz⟩
     refine ⟨χ, hχ, ρ⁻¹ᵁ • T, ρ⁻¹ • z, χ.smul_rel hTz ρ⁻¹, ?_, ?_⟩
-    · have := Support.smul_le_smul hST ρ⁻¹ᵁ
+    · have := Support.smul_subsupport_smul hST ρ⁻¹ᵁ
       simp only [allPermForget_inv, inv_smul_smul] at this ⊢
       exact this
     · rwa [TSet.mem_smul_iff, inv_inv, allPerm_inv_sderiv, smul_inv_smul]
@@ -87,7 +88,7 @@ theorem smul_raisedRel (s : Set (CodingFunction β)) (o : SupportOrbit β)
   · rwa [Support.smul_orbit]
   · exact hx.smul hγ ρ
 
-def raised (s : Set (CodingFunction β)) (o : SupportOrbit β)
+def raisedCodingFunction (s : Set (CodingFunction β)) (o : SupportOrbit β)
     (hso : ∀ S, S.orbit = o → ∃ x, Combination hγ x S s ∧ S.Supports x) : CodingFunction β where
   rel := RaisedRel hγ s o
   rel_coinjective := raisedRel_coinjective hγ s o
@@ -133,4 +134,61 @@ theorem raisedSingleton_supports (S : Support β) (y : TSet γ) :
 def raisedSingleton (S : Support β) (y : TSet γ) : CodingFunction β :=
   (Tangle.mk (singleton hγ y) (S + designatedSupport y ↗ hγ) (raisedSingleton_supports hγ S y)).code
 
+theorem combination_raisedSingleton (x : TSet β) (S : Support β) (hxS : S.Supports x) :
+    Combination hγ x S (raisedSingleton hγ S '' {y | y ∈[hγ] x}) := by
+  intro y
+  constructor
+  · intro hy
+    refine ⟨raisedSingleton hγ S y, ⟨y, hy, rfl⟩, S + designatedSupport y ↗ hγ, singleton hγ y,
+        ?_, ?_, ?_⟩
+    · exact Tangle.code_rel_self _
+    · exact subsupport_add
+    · rw [typedMem_singleton_iff]
+  · rintro ⟨_, ⟨w, hw, rfl⟩, T, z, hTz, hST, hyz⟩
+    have : (raisedSingleton hγ _ _).rel (S + designatedSupport w ↗ hγ) (singleton hγ w) :=
+        Tangle.code_rel_self ⟨singleton hγ w, _, raisedSingleton_supports hγ S w⟩
+    obtain ⟨ρ, h₁, h₂⟩ := CodingFunction.exists_allPerm_of_rel hTz this
+    rw [smul_eq_iff_eq_inv_smul] at h₂
+    subst h₂
+    rw [TSet.mem_smul_iff, inv_inv, typedMem_singleton_iff] at hyz
+    subst hyz
+    have : S.Subsupport (ρᵁ • T) := h₁.symm ▸ subsupport_add
+    have := smul_eq_of_subsupport hST this
+    rw [← hxS.smul_eq_of_smul_eq this] at hw
+    rwa [Set.mem_setOf_eq, TSet.mem_smul_iff, allPerm_inv_sderiv, inv_smul_smul] at hw
+
+def RaisedSingleton : Type u :=
+  { χ : CodingFunction β // ∃ S : Support β, ∃ y : TSet γ, χ = raisedSingleton hγ S y }
+
+theorem exists_combination_raisedSingleton (χ : CodingFunction β) :
+    ∃ s : Set (RaisedSingleton hγ), ∃ o : SupportOrbit β,
+    ∃ hso : ∀ S, S.orbit = o → ∃ x, Combination hγ x S (Subtype.val '' s) ∧ S.Supports x,
+      χ = raisedCodingFunction hγ (Subtype.val '' s) o hso := by
+  obtain ⟨S, x, hχ⟩ := χ.rel_dom_nonempty
+  refine ⟨(λ y ↦ ⟨raisedSingleton hγ S y, S, y, rfl⟩) '' {y : TSet γ | y ∈[hγ] x}, S.orbit, ?_, ?_⟩
+  · intro T hT
+    rw [Support.orbit_eq_iff] at hT
+    obtain ⟨ρ, rfl⟩ := hT
+    refine ⟨ρ⁻¹ • x, ?_, ?_⟩
+    · have := (combination_raisedSingleton hγ x (ρᵁ • T) (χ.supports_of_rel hχ)).smul hγ ρ⁻¹
+      rw [allPermForget_inv, inv_smul_smul] at this
+      convert this using 1
+      ext χ'
+      constructor
+      · rintro ⟨_, ⟨y, hy, rfl⟩, rfl⟩
+        exact ⟨y, hy, rfl⟩
+      · rintro ⟨y, hy, rfl⟩
+        exact ⟨_, ⟨y, hy, rfl⟩, rfl⟩
+    · have := (χ.supports_of_rel hχ).smul ρ⁻¹
+      rwa [allPermForget_inv, inv_smul_smul] at this
+  · apply CodingFunction.ext S x hχ
+    refine ⟨S, rfl, x, ?_⟩
+    convert combination_raisedSingleton hγ x S (χ.supports_of_rel hχ) using 1
+    ext χ'
+    constructor
+    · rintro ⟨_, ⟨y, hy, rfl⟩, rfl⟩
+      exact ⟨y, hy, rfl⟩
+    · rintro ⟨y, hy, rfl⟩
+      exact ⟨_, ⟨y, hy, rfl⟩, rfl⟩
+
 end ConNF

ConNF/Setup/ModelData.lean

@@ -101,6 +101,14 @@ theorem Support.Supports.smul_eq_smul {X : Type _} {α : TypeIndex}
   · rwa [mul_smul, inv_smul_eq_iff] at this
   · rwa [allPermForget_mul, mul_smul, allPermForget_inv, inv_smul_eq_iff]
 
+theorem Support.Supports.smul_eq_of_smul_eq {X : Type _} {α : TypeIndex}
+    [ModelData α] [MulAction (AllPerm α) X]
+    {S : Support α} {x : X} (h : S.Supports x) {ρ : AllPerm α} (hρ : ρᵁ • S = S) :
+    ρ • x = x := by
+  have := smul_eq_smul (ρ₁ := ρ) (ρ₂ := 1) h ?_
+  · rwa [one_smul] at this
+  · rwa [allPermForget_one, one_smul]
+
 theorem Support.Supports.smul {X : Type _} {α : TypeIndex}
     [ModelData α] [MulAction (AllPerm α) X]
     {S : Support α} {x : X} (h : S.Supports x) (ρ : AllPerm α) :

ConNF/Setup/Support.lean

@@ -338,6 +338,10 @@ theorem card_support {α : TypeIndex} : #(Support α) = #μ := by
   · rw [mk_prod, lift_id, lift_id, card_atom,
       mul_eq_right aleph0_lt_μ.le (card_path_lt' α ⊥).le (card_path_ne_zero α)]
 
+/-!
+## Orders on supports
+-/
+
 instance : LE BaseSupport where
   le S T := (∀ a ∈ Sᴬ, a ∈ Tᴬ) ∧ (∀ N ∈ Sᴺ, N ∈ Tᴺ)
 
@@ -353,6 +357,17 @@ theorem BaseSupport.smul_le_smul {S T : BaseSupport} (h : S ≤ T) (π : BasePer
   · intro N
     exact h.2 (π⁻¹ • N)
 
+def BaseSupport.Subsupport (S T : BaseSupport) : Prop :=
+  Sᴬ.rel ≤ Tᴬ.rel ∧ Sᴺ.rel ≤ Tᴺ.rel
+
+theorem BaseSupport.smul_subsupport_smul {S T : BaseSupport} (h : S.Subsupport T) (π : BasePerm) :
+    (π • S).Subsupport (π • T) := by
+  constructor
+  · intro i a ha
+    exact h.1 i _ ha
+  · intro i N hN
+    exact h.2 i _ hN
+
 instance {α : TypeIndex} : LE (Support α) where
   le S T := ∀ A, S ⇘. A ≤ T ⇘. A
 
@@ -386,4 +401,42 @@ theorem le_add_left {α : TypeIndex} {S T : Support α} :
     simp only [Support.add_derivBot, BaseSupport.add_nearLitters, Enumeration.mem_add_iff]
     exact Or.inr hN
 
+def Support.Subsupport {α : TypeIndex} (S T : Support α) : Prop :=
+  ∀ A, (S ⇘. A).Subsupport (T ⇘. A)
+
+theorem Support.smul_subsupport_smul {α : TypeIndex} {S T : Support α}
+    (h : S.Subsupport T) (π : StrPerm α) :
+    (π • S).Subsupport (π • T) :=
+  λ A ↦ BaseSupport.smul_subsupport_smul (h A) (π A)
+
+theorem subsupport_add {α : TypeIndex} {S T : Support α} :
+    S.Subsupport (S + T) := by
+  intro A
+  constructor
+  · intro i a ha
+    simp only [Support.add_derivBot, BaseSupport.add_atoms, Enumeration.rel_add_iff]
+    exact Or.inl ha
+  · intro i N hN
+    simp only [Support.add_derivBot, BaseSupport.add_atoms, Enumeration.rel_add_iff]
+    exact Or.inl hN
+
+theorem smul_eq_of_subsupport {α : TypeIndex} {S T : Support α} {π : StrPerm α}
+    (h₁ : S.Subsupport T) (h₂ : S.Subsupport (π • T)) :
+    π • S = S := by
+  rw [Support.smul_eq_iff]
+  intro A
+  constructor
+  · rintro a ⟨i, hi⟩
+    have hi₁ := (h₁ A).1 i a hi
+    have hi₂ := (h₂ A).1 i a hi
+    have := (T ⇘. A)ᴬ.rel_coinjective.coinjective hi₁ hi₂
+    dsimp only at this
+    rwa [smul_eq_iff_eq_inv_smul]
+  · rintro N ⟨i, hi⟩
+    have hi₁ := (h₁ A).2 i N hi
+    have hi₂ := (h₂ A).2 i N hi
+    have := (T ⇘. A)ᴺ.rel_coinjective.coinjective hi₁ hi₂
+    dsimp only at this
+    rwa [smul_eq_iff_eq_inv_smul]
+
 end ConNF