Model data

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

ConNF.lean

@@ -8,9 +8,11 @@ import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm
 import ConNF.Setup.Enumeration
 import ConNF.Setup.Litter
+import ConNF.Setup.ModelData
 import ConNF.Setup.NearLitter
 import ConNF.Setup.Params
 import ConNF.Setup.Path
+import ConNF.Setup.PathEnumeration
 import ConNF.Setup.Small
 import ConNF.Setup.StrPerm
 import ConNF.Setup.StrSet

ConNF/Setup/Enumeration.lean

@@ -1,5 +1,4 @@
 import ConNF.Aux.Rel
-import ConNF.Setup.Path
 import ConNF.Setup.Small
 
 /-!
@@ -53,6 +52,12 @@ theorem graph'_small (E : Enumeration X) :
     Small E.rel.graph' :=
   small_graph' E.dom_small E.coe_small
 
+noncomputable def empty : Enumeration X where
+  bound := 0
+  rel _ _ := False
+  lt_bound _ h := by cases h; contradiction
+  rel_coinjective := by constructor; intros; contradiction
+
 noncomputable def singleton (x : X) : Enumeration X where
   bound := 1
   rel i y := i = 0 ∧ y = x
@@ -168,38 +173,6 @@ theorem mem_invImage {f : Y → X} {hf : f.Injective} (y : Y) :
     y ∈ E.invImage f hf ↔ f y ∈ E :=
   Iff.rfl
 
-/-!
-## Enumerations over paths
--/
-
-instance (X : Type u) (α β : TypeIndex) :
-    Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β where
-  deriv E A := E.invImage (λ x ↦ (x.1 ⇗ A, x.2))
-    (λ x y h ↦ Prod.ext (Path.deriv_right_injective
-      ((Prod.mk.injEq _ _ _ _).mp h).1) ((Prod.mk.injEq _ _ _ _).mp h).2)
-
-instance (X : Type u) (α β : TypeIndex) :
-    Coderivative (Enumeration (β ↝ ⊥ × X)) (Enumeration (α ↝ ⊥ × X)) α β where
-  coderiv E A := E.image (λ x ↦ (x.1 ⇗ A, x.2))
-
-instance (X : Type u) (α : TypeIndex) :
-    BotDerivative (Enumeration (α ↝ ⊥ × X)) (Enumeration X) α where
-  botDeriv E A := E.invImage (λ x ↦ (A, x)) (Prod.mk.inj_left A)
-  botSderiv E := E.invImage (λ x ↦ (Path.nil ↘., x)) (Prod.mk.inj_left (Path.nil ↘.))
-  botDeriv_single E h := by
-    cases α using WithBot.recBotCoe with
-    | bot => cases lt_irrefl ⊥ h
-    | coe => rfl
-
-theorem ext_path {X : Type u} {α : TypeIndex} {E F : Enumeration (α ↝ ⊥ × X)}
-    (h : ∀ A, E ⇘. A = F ⇘. A) :
-    E = F := by
-  ext i x
-  · have := congr_arg bound (h (Path.nil ↘.))
-    exact this
-  · have := congr_arg rel (h x.1)
-    exact iff_of_eq (congr_fun₂ this i x.2)
-
 -- TODO: Some stuff about the partial order on enumerations and concatenation of enumerations.
 
 end Enumeration

ConNF/Setup/Litter.lean

@@ -55,20 +55,28 @@ theorem card_litter : #Litter = #μ := by
     cases h
     rfl
 
-/-- Typeclass for the `ᴸ` notation. -/
+/-- Typeclass for the `ᴸ` notation.  Used for converting to  litters, or extracting the
+"litter part" of an object. -/
 class SuperL (X : Type _) (Y : outParam <| Type _) where
   superL : X → Y
 
-/-- Typeclass for the `ᴬ` notation. -/
+/-- Typeclass for the `ᴬ` notation. Used for converting to atoms, or extracting the
+"atom part" of an object. -/
 class SuperA (X : Type _) (Y : outParam <| Type _) where
   superA : X → Y
 
-/-- Typeclass for the `ᴺ` notation. -/
+/-- Typeclass for the `ᴺ` notation. Used for converting to near-litters, or extracting the
+"near-litter part" of an object. -/
 class SuperN (X : Type _) (Y : outParam <| Type _) where
   superN : X → Y
 
+/-- Typeclass for the `ᵁ` notation. Used for forgetful operations. -/
+class SuperU (X : Type _) (Y : outParam <| Type _) where
+  superU : X → Y
+
 postfix:max "ᴸ" => SuperL.superL
 postfix:max "ᴬ" => SuperA.superA
 postfix:max "ᴺ" => SuperN.superN
+postfix:max "ᵁ" => SuperU.superU
 
 end ConNF

ConNF/Setup/ModelData.lean

@@ -0,0 +1,116 @@
+import ConNF.Setup.StrSet
+import ConNF.Setup.Support
+
+/-!
+# Model data
+
+In this file, we define what model data at a type index means.
+
+## Main declarations
+
+* `ConNF.ModelData`: The type of model data at a given type index.
+-/
+
+universe u
+
+open Cardinal
+
+namespace ConNF
+
+variable [Params.{u}]
+
+/-- The same as `ModelData` but without the propositions. -/
+class PreModelData (α : TypeIndex) where
+  TSet : Type u
+  AllPerm : Type u
+  [allPermGroup : Group AllPerm]
+  [allAction : MulAction AllPerm TSet]
+  tSetForget : TSet → StrSet α
+  allPermForget : AllPerm → StrPerm α
+
+export PreModelData (TSet AllPerm)
+
+attribute [instance] PreModelData.allPermGroup PreModelData.allAction
+
+instance {α : TypeIndex} [PreModelData α] : SuperU (TSet α) (StrSet α) where
+  superU := PreModelData.tSetForget
+
+instance {α : TypeIndex} [PreModelData α] : SuperU (AllPerm α) (StrPerm α) where
+  superU := PreModelData.allPermForget
+
+structure Support.Supports {X : Type _} {α : TypeIndex} [PreModelData α] [MulAction (AllPerm α) X]
+    (S : Support α) (x : X) : Prop where
+  supports (ρ : AllPerm α) : ρᵁ • S = S → ρ • x = x
+  nearLitters_eq_empty_of_bot : α = ⊥ → Sᴺ = .empty
+
+class ModelData (α : TypeIndex) extends PreModelData α where
+  allPermForget_one : (1 : AllPerm)ᵁ = 1
+  allPermForget_mul (ρ₁ ρ₂ : AllPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ
+  smul_forget (ρ : AllPerm) (x : TSet) : (ρ • x)ᵁ = ρᵁ • xᵁ
+  exists_support (x : TSet) : ∃ S : Support α, S.Supports x
+
+@[ext]
+structure Tangle (α : TypeIndex) [ModelData α] where
+  set : TSet α
+  support : Support α
+  support_supports : support.Supports set
+
+/-!
+## Criteria for supports
+-/
+
+theorem Support.supports_coe {α : Λ} {X : Type _} [PreModelData α] [MulAction (AllPerm α) X]
+    (S : Support α) (x : X)
+    (h : ∀ ρ : AllPerm α,
+      (∀ A : α ↝ ⊥, ∀ a ∈ (S ⇘. A)ᴬ, ρᵁ A • a = a) →
+      (∀ A : α ↝ ⊥, ∀ N ∈ (S ⇘. A)ᴺ, ρᵁ A • N = N) → ρ • x = x) :
+    S.Supports x := by
+  constructor
+  · intro ρ h'
+    apply h
+    · intro A a ha
+      exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_atoms_eq_of_smul_eq h') A a ha
+    · intro A N hN
+      exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_nearLitters_eq_of_smul_eq h') A N hN
+  · intro h
+    cases h
+
+theorem Support.supports_bot {X : Type _} [PreModelData ⊥] [MulAction (AllPerm ⊥) X]
+    (E : Enumeration (⊥ ↝ ⊥ × Atom)) (x : X)
+    (h : ∀ ρ : AllPerm ⊥, (∀ A : ⊥ ↝ ⊥, ∀ x : Atom, (A, x) ∈ E → ρᵁ A • x = x) → ρ • x = x) :
+    (⟨E, .empty⟩ : Support ⊥).Supports x := by
+  constructor
+  · intro ρ h'
+    apply h
+    intro A x hx
+    exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_atoms_eq_of_smul_eq h') A x hx
+  · intro
+    rfl
+
+/-!
+## Model data at level `⊥`
+-/
+
+def botPreModelData : PreModelData ⊥ where
+  TSet := Atom
+  AllPerm := BasePerm
+  tSetForget := StrSet.botEquiv.symm
+  allPermForget ρ _ := ρ
+
+def botModelData : ModelData ⊥ where
+  allPermForget_one := rfl
+  allPermForget_mul _ _ := rfl
+  smul_forget ρ x := by
+    apply StrSet.botEquiv.injective
+    have : ∀ x : TSet ⊥, xᵁ = StrSet.botEquiv.symm x := λ _ ↦ rfl
+    simp only [this, Equiv.apply_symm_apply, StrSet.strPerm_smul_bot]
+    rfl
+  exists_support x := by
+    use ⟨.singleton (Path.nil, x), .empty⟩
+    apply Support.supports_bot
+    intro ρ hc
+    apply hc Path.nil x
+    rw [Enumeration.mem_singleton_iff]
+  __ := botPreModelData
+
+end ConNF

ConNF/Setup/PathEnumeration.lean

@@ -0,0 +1,123 @@
+import ConNF.Setup.Enumeration
+import ConNF.Setup.StrPerm
+
+/-!
+# Enumerations over paths
+
+In this file, we provide extra features to `Enumeration`s that take values of the form `α ↝ ⊥ × X`.
+
+## Main declarations
+
+* `ConNF.ext_path`: An extensionality principle for such `Enumeration`s.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+
+namespace ConNF
+
+variable [Params.{u}]
+
+namespace Enumeration
+
+instance (X : Type u) (α β : TypeIndex) :
+    Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β where
+  deriv E A := E.invImage (λ x ↦ (x.1 ⇗ A, x.2))
+    (λ x y h ↦ Prod.ext (Path.deriv_right_injective
+      ((Prod.mk.injEq _ _ _ _).mp h).1) ((Prod.mk.injEq _ _ _ _).mp h).2)
+
+@[simp]
+theorem deriv_rel {X : Type _} {α β : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ β)
+    (i : κ) (x : β ↝ ⊥ × X) :
+    (E ⇘ A).rel i x ↔ E.rel i (x.1 ⇗ A, x.2) :=
+  Iff.rfl
+
+instance (X : Type u) (α β : TypeIndex) :
+    Coderivative (Enumeration (β ↝ ⊥ × X)) (Enumeration (α ↝ ⊥ × X)) α β where
+  coderiv E A := E.image (λ x ↦ (x.1 ⇗ A, x.2))
+
+instance (X : Type u) (α : TypeIndex) :
+    BotDerivative (Enumeration (α ↝ ⊥ × X)) (Enumeration X) α where
+  botDeriv E A := E.invImage (λ x ↦ (A, x)) (Prod.mk.inj_left A)
+  botSderiv E := E.invImage (λ x ↦ (Path.nil ↘., x)) (Prod.mk.inj_left (Path.nil ↘.))
+  botDeriv_single E h := by
+    cases α using WithBot.recBotCoe with
+    | bot => cases lt_irrefl ⊥ h
+    | coe => rfl
+
+theorem ext_path {X : Type u} {α : TypeIndex} {E F : Enumeration (α ↝ ⊥ × X)}
+    (h : ∀ A, E ⇘. A = F ⇘. A) :
+    E = F := by
+  ext i x
+  · have := congr_arg bound (h (Path.nil ↘.))
+    exact this
+  · have := congr_arg rel (h x.1)
+    exact iff_of_eq (congr_fun₂ this i x.2)
+
+theorem mulAction_aux {X : Type _} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) :
+    Function.Injective (λ x : α ↝ ⊥ × X ↦ (x.1, (π x.1)⁻¹ • x.2)) := by
+  rintro ⟨A₁, x₁⟩ ⟨A₂, x₂⟩ h
+  rw [Prod.mk.injEq] at h
+  cases h.1
+  exact Prod.ext h.1 (smul_left_cancel _ h.2)
+
+instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] :
+    SMul (StrPerm α) (Enumeration (α ↝ ⊥ × X)) where
+  smul π E := E.invImage (λ x ↦ (x.1, (π x.1)⁻¹ • x.2)) (mulAction_aux π)
+
+@[simp]
+theorem smul_rel {X : Type _} {α : TypeIndex} [MulAction BasePerm X]
+    (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) (i : κ) (x : α ↝ ⊥ × X) :
+    (π • E).rel i x ↔ E.rel i (x.1, (π x.1)⁻¹ • x.2) :=
+  Iff.rfl
+
+instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] :
+    MulAction (StrPerm α) (Enumeration (α ↝ ⊥ × X)) where
+  one_smul E := by
+    ext i x
+    · rfl
+    · rw [smul_rel, Tree.one_apply, inv_one, one_smul]
+  mul_smul π₁ π₂ E := by
+    ext i x
+    · rfl
+    · rw [smul_rel, smul_rel, smul_rel, Tree.mul_apply, mul_inv_rev, mul_smul]
+
+theorem smul_eq_of_forall_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X]
+    {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)}
+    (h : ∀ A : α ↝ ⊥, ∀ x : X, (A, x) ∈ E → π A • x = x) :
+    π • E = E := by
+  ext i x
+  · rfl
+  · obtain ⟨A, x⟩ := x
+    constructor
+    · intro hx
+      have := h A ((π A)⁻¹ • x) ⟨i, hx⟩
+      rw [smul_inv_smul] at this
+      rw [this]
+      exact hx
+    · intro hx
+      have := h A x ⟨i, hx⟩
+      rw [← this]
+      rwa [smul_rel, inv_smul_smul]
+
+theorem smul_eq_of_mem_of_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X]
+    {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)}
+    (h : π • E = E) (A : α ↝ ⊥) (x : X) (hx : (A, x) ∈ E) :
+    π A • x = x := by
+  obtain ⟨i, hx⟩ := hx
+  have := congr_fun₂ (congr_arg rel h) i (A, x)
+  simp only [smul_rel, eq_iff_iff] at this
+  have := E.rel_coinjective.coinjective hx (this.mpr hx)
+  rw [Prod.mk.injEq, eq_inv_smul_iff] at this
+  exact this.2
+
+theorem smul_eq_iff {X : Type _} {α : TypeIndex} [MulAction BasePerm X]
+    (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) :
+    π • E = E ↔ ∀ A : α ↝ ⊥, ∀ x : X, (A, x) ∈ E → π A • x = x :=
+  ⟨smul_eq_of_mem_of_smul_eq, smul_eq_of_forall_smul_eq⟩
+
+end Enumeration
+
+end ConNF