Move shells earlier

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

ConNF/Counting/Hypotheses.lean

@@ -18,28 +18,25 @@ variable [Params.{u}] [Level] [BasePositions]
 instance : LeLevel (0 : Λ) := ⟨WithBot.coe_le_coe.mpr (Params.Λ_zero_le _)⟩
 
 class CountingAssumptions extends FOAAssumptions where
-  toPretangle (β : TypeIndex) [LeLevel β] : Tangle β → Pretangle β
-  toPretangle_smul (β : TypeIndex) [LeLevel β] (ρ : Allowable β) (t : Tangle β) :
-    toPretangle β (ρ • t) = ρ • toPretangle β t
   /-- Tangles contain only tangles. -/
   eq_toPretangle_of_mem (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
     (h : (γ : TypeIndex) < β) (t₁ : Tangle β) (t₂ : Pretangle γ) :
-    t₂ ∈ Pretangle.ofCoe (toPretangle β t₁) γ h → ∃ t₂' : Tangle γ, t₂ = toPretangle γ t₂'
+    t₂ ∈ Pretangle.ofCoe (toPretangle t₁) γ h → ∃ t₂' : Tangle γ, t₂ = toPretangle t₂'
   /-- Tangles are extensional at every proper level `γ < β`. -/
   toPretangle_ext (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) (t₁ t₂ : Tangle β) :
     (∀ t : Pretangle γ,
-      t ∈ Pretangle.ofCoe (toPretangle β t₁) γ h ↔ t ∈ Pretangle.ofCoe (toPretangle β t₂) γ h) →
-    toPretangle β t₁ = toPretangle β t₂
+      t ∈ Pretangle.ofCoe (toPretangle t₁) γ h ↔ t ∈ Pretangle.ofCoe (toPretangle t₂) γ h) →
+    toPretangle t₁ = toPretangle t₂
   tangle_ext (β : Λ) [LeLevel β] (t₁ t₂ : Tangle β) :
-    toPretangle β t₁ = toPretangle β t₂ → t₁.support = t₂.support → t₁ = t₂
+    toPretangle t₁ = toPretangle t₂ → t₁.support = t₂.support → t₁ = t₂
   /-- Any `γ`-tangle can be treated as a singleton at level `β` if `γ < β`. -/
   singleton (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) : Tangle β
   singleton_support (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) :
     (singleton β γ h t).support = t.support.image (fun c => ⟨(Hom.toPath h).comp c.1, c.2⟩)
   singleton_toPretangle (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) :
-    Pretangle.ofCoe (toPretangle β (singleton β γ h t)) γ h = {toPretangle γ t}
+    Pretangle.ofCoe (toPretangle (singleton β γ h t)) γ h = {toPretangle t}
 
-export CountingAssumptions (toPretangle toPretangle_smul eq_toPretangle_of_mem toPretangle_ext
+export CountingAssumptions (eq_toPretangle_of_mem toPretangle_ext
   tangle_ext singleton singleton_support singleton_toPretangle)
 
 variable [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : γ < β)

ConNF/Counting/Shell.lean

@@ -13,56 +13,8 @@ namespace ConNF
 
 variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions] {β : Λ} [LeLevel β]
 
-/-- The "shell" of a tangle, reducing it just to the information that it used to come from
-a tangle. -/
-@[ext]
-structure Shell (β : Λ) [LeLevel β] : Type u where
-  p : Pretangle β
-  h : ∃ t : Tangle β, p = toPretangle β t
-
 namespace Shell
 
-instance : MulAction (Allowable β) (Shell β) where
-  smul ρ t := ⟨ρ • t.p, by
-    obtain ⟨s, hs⟩ := t.h
-    refine ⟨ρ • s, ?_⟩
-    rw [hs]
-    rw [toPretangle_smul]⟩
-  one_smul := by
-    rintro ⟨p, h⟩
-    refine Shell.ext _ _ ?_
-    change 1 • p = p
-    rw [one_smul]
-  mul_smul := by
-    rintro ρ₁ ρ₂ ⟨p, h⟩
-    refine Shell.ext _ _ ?_
-    change (ρ₁ * ρ₂) • p = ρ₁ • ρ₂ • p
-    rw [mul_smul]
-
-@[simp]
-theorem smul_p (ρ : Allowable β) (t : Shell β) :
-    (ρ • t).p = ρ • t.p :=
-  rfl
-
-def ofTangle (t : Tangle β) : Shell β :=
-  ⟨toPretangle β t, t, rfl⟩
-
-theorem exists_eq_ofTangle (s : Shell β) :
-    ∃ t : Tangle β, s = ofTangle t := by
-  obtain ⟨p, t, rfl⟩ := s
-  exact ⟨t, rfl⟩
-
-@[simp]
-theorem ofTangle_p (t : Tangle β) :
-    (ofTangle t).p = toPretangle β t :=
-  rfl
-
-theorem smul_ofTangle (ρ : Allowable β) (t : Tangle β) :
-    ρ • ofTangle t = ofTangle (ρ • t) := by
-  refine Shell.ext _ _ ?_
-  simp only [smul_p, ofTangle_p]
-  rw [toPretangle_smul]
-
 protected theorem eq_toPretangle_of_mem (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
     (h : (γ : TypeIndex) < β) (t₁ : Shell β) (t₂ : Pretangle γ) :
     t₂ ∈ Pretangle.ofCoe t₁.p γ h → ∃ t₂' : Shell γ, t₂ = t₂'.p := by
@@ -72,7 +24,7 @@ protected theorem eq_toPretangle_of_mem (β : Λ) [LeLevel β] (γ : Λ) [LeLeve
   exact ⟨ofTangle t₂', ht₂'⟩
 
 theorem ofTangle_eq_iff (t₁ t₂ : Tangle β) :
-    toPretangle β t₁ = toPretangle β t₂ ↔ ofTangle t₁ = ofTangle t₂ := by
+    toPretangle t₁ = toPretangle t₂ ↔ ofTangle t₁ = ofTangle t₂ := by
   constructor
   · intro h
     ext
@@ -156,7 +108,7 @@ theorem out_injective (s₁ s₂ : Shell β) (h : s₁.out = s₂.out) : s₁ =
   rw [eq_ofTangle_out s₁, eq_ofTangle_out s₂, h]
 
 @[simp]
-theorem out_toPretangle (s : Shell β) : toPretangle β s.out = s.p := by
+theorem out_toPretangle (s : Shell β) : toPretangle s.out = s.p := by
   conv_rhs => rw [eq_ofTangle_out s]
 
 noncomputable def support (s : Shell β) : Support β :=

ConNF/Fuzz.lean

@@ -1,3 +1,4 @@
 import ConNF.Fuzz.Position
 import ConNF.Fuzz.Hypotheses
 import ConNF.Fuzz.Construction
+import ConNF.Fuzz.Shell

ConNF/Fuzz/Hypotheses.lean

@@ -46,8 +46,13 @@ class TangleData (α : TypeIndex) where
     haveI : MulAction Allowable (Address α) :=
       MulAction.compHom _ allowableToStructPerm
     MulAction.Supports Allowable (support t : Set (Address α)) t
+  toPretangle : Tangle → Pretangle α
+  toPretangle_smul (ρ : Allowable) (t : Tangle) :
+    haveI : MulAction Allowable (Pretangle α) :=
+      MulAction.compHom _ allowableToStructPerm
+    toPretangle (ρ • t) = ρ • toPretangle t
 
-export TangleData (Tangle Allowable)
+export TangleData (Tangle Allowable toPretangle toPretangle_smul)
 
 attribute [instance] TangleData.allowableGroup TangleData.allowableAction
 
@@ -210,6 +215,8 @@ instance Bot.tangleData : TangleData ⊥
     simp only [Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
       NearLitterPerm.smul_address_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h
     exact h
+  toPretangle := Pretangle.ofBot
+  toPretangle_smul _ _ := rfl
 
 /-- The position function at level `⊥`, taken from the `BasePositions`. -/
 instance Bot.positionedTangles [BasePositions] : PositionedTangles ⊥ :=

ConNF/Fuzz/Shell.lean

@@ -0,0 +1,68 @@
+import Mathlib.GroupTheory.GroupAction.Basic
+import ConNF.Fuzz.Hypotheses
+
+/-!
+# Coding functions
+-/
+
+open MulAction Set Sum
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [BasePositions] {β : Λ} [TangleData β]
+
+/-- The "shell" of a tangle, reducing it just to the information that it used to come from
+a tangle. -/
+@[ext]
+structure Shell (β : Λ) [TangleData β] : Type u where
+  p : Pretangle β
+  h : ∃ t : Tangle β, p = toPretangle t
+
+namespace Shell
+
+instance : MulAction (Allowable β) (Shell β) where
+  smul ρ t := ⟨ρ • t.p, by
+    obtain ⟨s, hs⟩ := t.h
+    refine ⟨ρ • s, ?_⟩
+    rw [hs]
+    rw [toPretangle_smul]⟩
+  one_smul := by
+    rintro ⟨p, h⟩
+    refine Shell.ext _ _ ?_
+    change 1 • p = p
+    rw [one_smul]
+  mul_smul := by
+    rintro ρ₁ ρ₂ ⟨p, h⟩
+    refine Shell.ext _ _ ?_
+    change (ρ₁ * ρ₂) • p = ρ₁ • ρ₂ • p
+    rw [mul_smul]
+
+@[simp]
+theorem smul_p (ρ : Allowable β) (t : Shell β) :
+    (ρ • t).p = ρ • t.p :=
+  rfl
+
+def ofTangle (t : Tangle β) : Shell β :=
+  ⟨toPretangle t, t, rfl⟩
+
+theorem exists_eq_ofTangle (s : Shell β) :
+    ∃ t : Tangle β, s = ofTangle t := by
+  obtain ⟨p, t, rfl⟩ := s
+  exact ⟨t, rfl⟩
+
+@[simp]
+theorem ofTangle_p (t : Tangle β) :
+    (ofTangle t).p = toPretangle t :=
+  rfl
+
+theorem smul_ofTangle (ρ : Allowable β) (t : Tangle β) :
+    ρ • ofTangle t = ofTangle (ρ • t) := by
+  refine Shell.ext _ _ ?_
+  simp only [smul_p, ofTangle_p]
+  rw [toPretangle_smul]
+
+end Shell
+
+end ConNF

ConNF/Model/Construction.lean

@@ -38,6 +38,10 @@ structure IH (α : Λ) where
     ρ • typedNearLitter N =
     typedNearLitter ((allowableToStructPerm ρ) (Hom.toPath <| bot_lt_coe α) • N)
   toPretangle : Tangle → Pretangle α
+  toPretangle_smul (ρ : Allowable) (t : Tangle) :
+    haveI : MulAction Allowable (Pretangle α) :=
+      MulAction.compHom _ allowableToStructPerm
+    toPretangle (ρ • t) = ρ • toPretangle t
 
 instance {α : Λ} {ih : IH α} : Group ih.Allowable := ih.allowableGroup
 instance {α : Λ} {ih : IH α} : MulAction ih.Allowable ih.Tangle := ih.allowableAction
@@ -52,6 +56,8 @@ def IH.tangleData {α : Λ} (ih : IH α) : TangleData α where
   allowableToStructPerm := ih.allowableToStructPerm
   support := ih.support
   support_supports := ih.support_supports
+  toPretangle := ih.toPretangle
+  toPretangle_smul := ih.toPretangle_smul
 
 def IH.positionedTangles {α : Λ} (ih : IH α) :
     letI := ih.tangleData
@@ -151,16 +157,25 @@ structure IHProp (α : Λ) (ih : ∀ β ≤ α, IH β) : Prop where
       (_hfα : ∀ ρ : (ih α le_rfl).Allowable,
         (ih α le_rfl).allowableToStructPerm ρ (Hom.toPath (bot_lt_coe _)) = fα ρ),
       fα ρ = π)
-  toPretangle_smul (t : (ih α le_rfl).Tangle) (ρ : (ih α le_rfl).Allowable) :
-    (ih α le_rfl).toPretangle (ρ • t) = ρ • (ih α le_rfl).toPretangle t
   eq_toPretangle_of_mem (β : Λ) (hβ : β < α) (t₁ : (ih α le_rfl).Tangle) (t₂ : Pretangle β) :
     t₂ ∈ Pretangle.ofCoe ((ih α le_rfl).toPretangle t₁) β (coe_lt_coe.mpr hβ) →
     ∃ t₂' : (ih β hβ.le).Tangle, t₂ = (ih β hβ.le).toPretangle t₂'
+  toPretangle_ext (β : Λ) (hβ : β < α) (t₁ t₂ : (ih α le_rfl).Tangle) :
+    (∀ t : Pretangle β,
+      t ∈ Pretangle.ofCoe ((ih α le_rfl).toPretangle t₁) β (coe_lt_coe.mpr hβ) ↔
+      t ∈ Pretangle.ofCoe ((ih α le_rfl).toPretangle t₂) β (coe_lt_coe.mpr hβ)) →
+    (ih α le_rfl).toPretangle t₁ = (ih α le_rfl).toPretangle t₂
+  tangle_ext (t₁ t₂ : (ih α le_rfl).Tangle) :
+    (ih α le_rfl).toPretangle t₁ = (ih α le_rfl).toPretangle t₂ →
+    (ih α le_rfl).support t₁ = (ih α le_rfl).support t₂ →
+    t₁ = t₂
   /-- It's useful to keep this `Prop`-valued, because then there is no data in `IH` that
   crosses levels. -/
   has_singletons (β : Λ) (hβ : β < α) :
     ∃! S : (ih β hβ.le).Tangle ↪ (ih α le_rfl).Tangle,
     ∀ t : (ih β hβ.le).Tangle,
+      (ih α le_rfl).support (S t) =
+        ((ih β hβ.le).support t).image (fun c => ⟨(Hom.toPath (coe_lt_coe.mpr hβ)).comp c.1, c.2⟩) ∧
       Pretangle.ofCoe ((ih α le_rfl).toPretangle (S t)) β (coe_lt_coe.mpr hβ) =
       {(ih β hβ.le).toPretangle t}
 
@@ -181,6 +196,8 @@ def tangleDataStep (α : Λ) (ihs : (β : Λ) → β < α → IH β) : TangleDat
       refine Enumeration.ext' rfl ?_
       intro i hS _
       exact h ⟨i, hS, rfl⟩
+    toPretangle := sorry
+    toPretangle_smul := sorry
   }
 
 def typedObjectsStep (α : Λ) (ihs : (β : Λ) → β < α → IH β) :
@@ -1227,12 +1244,12 @@ theorem toPretangleLt_smul (α : Λ) (ihs : (β : Λ) → β < α → IH β)
   refine WithBot.recBotCoe ?_ ?_ β
   · intro ihs _ iβ ρ t
     rfl
-  · intro β ihs h iβ ρ t
+  · intro β ihs _ iβ ρ t
     letI : Level := ⟨α⟩
     letI : FOAData := buildStepFOAData α ihs
     have hβ' := coe_lt_coe.mp iβ.elim
     rw [toPretangleStepLt_coe α ihs β hβ', toPretangleStepLt_coe α ihs β hβ']
-    rw [foaData_allowable_lt_equiv_smul, (h β hβ').toPretangle_smul]
+    rw [foaData_allowable_lt_equiv_smul, (ihs β hβ').toPretangle_smul]
     rw [Allowable.toStructPerm_smul, foaData_allowable_lt_equiv_toStructPerm]
     rfl
 
@@ -1331,15 +1348,44 @@ theorem eq_toPretangle_of_mem_step (α : Λ) (ihs : (β : Λ) → β < α → IH
 
 theorem toPretangle_ext_step (α : Λ) (ihs : (β : Λ) → β < α → IH β)
     (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ)))
-    (β : Λ) [iβ : letI : Level := ⟨α⟩; LeLevel β]
-    (γ : Λ) [iγ : letI : Level := ⟨α⟩; LeLevel γ]
+    (β : Λ) (γ : Λ)
+    [iβ : letI : Level := ⟨α⟩; LeLevel β] [iγ : letI : Level := ⟨α⟩; LeLevel γ]
     (hγβ : (γ : TypeIndex) < β)
     (t₁ t₂ :
       letI : Level := ⟨α⟩
       letI : FOAData := buildStepFOAData α ihs
       Tangle β) :
     (∀ t : Pretangle γ, t ∈ Pretangle.ofCoe (toPretangleStep α ihs β iβ t₁) γ hγβ ↔
-      t ∈ Pretangle.ofCoe (toPretangleStep α ihs β iβ t₂) γ hγβ) → t₁ = t₂ := sorry
+      t ∈ Pretangle.ofCoe (toPretangleStep α ihs β iβ t₂) γ hγβ) →
+    toPretangleStep α ihs β iβ t₁ = toPretangleStep α ihs β iβ t₂ := by
+  letI : Level := ⟨α⟩
+  letI iγ : LtLevel γ := ⟨hγβ.trans_le iβ.elim⟩
+  letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+  letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+  letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+  letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+  by_cases hβ : β = α
+  · cases hβ
+    intro ht
+    simp only [NewTangle.toPretangle, toPretangleStep_eq] at ht ⊢
+    have := Semitangle.ext (γ := γ) (foaData_tangle_eq_equiv α ihs t₁).t
+      (foaData_tangle_eq_equiv α ihs t₂).t ?_
+    · rw [this]
+    simp only [Semitangle.toPretangle, Pretangle.ofCoe_symm, exists_and_right,
+      Pretangle.ofCoe_toCoe, mem_setOf_eq] at ht
+    ext s
+    constructor
+    · intro hs
+      obtain ⟨s', hs'⟩ := (ht _).mp ⟨s, hs, rfl⟩
+      rw [toPretangleStepLt_coe α ihs γ (coe_lt_coe.mp iγ.elim),
+        toPretangleStepLt_coe α ihs γ (coe_lt_coe.mp iγ.elim)] at hs'
+      sorry
+    · sorry
+  · intro ht
+    have hβ' := lt_of_le_of_ne (coe_le_coe.mp iβ.elim) hβ
+    simp only [toPretangleStep_lt' α ihs β (coe_lt_coe.mpr hβ'),
+      toPretangleStepLt_coe α ihs β hβ'] at ht ⊢
+    exact (h β hβ').toPretangle_ext γ (coe_lt_coe.mp hγβ) _ _ ht
 
 noncomputable def buildStepCountingAssumptions (α : Λ) (ihs : (β : Λ) → β < α → IH β)
     (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) :
@@ -1348,10 +1394,8 @@ noncomputable def buildStepCountingAssumptions (α : Λ) (ihs : (β : Λ) → β
   letI : Level := ⟨α⟩
   letI : FOAAssumptions := buildStepFOAAssumptions α ihs h
   {
-    toPretangle := toPretangleStep α ihs
-    toPretangle_smul := toPretangle_smul_step α ihs h
-    eq_toPretangle_of_mem := eq_toPretangle_of_mem_step α ihs h
-    toPretangle_ext := sorry
+    eq_toPretangle_of_mem := sorry -- eq_toPretangle_of_mem_step α ihs h
+    toPretangle_ext := sorry -- toPretangle_ext_step α ihs h
     tangle_ext := sorry
     singleton := sorry
     singleton_support := sorry