Base permutations

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

ConNF.lean

@@ -4,6 +4,7 @@ import ConNF.Aux.Set
 import ConNF.Aux.Transfer
 import ConNF.Aux.WellOrder
 import ConNF.Setup.Atom
+import ConNF.Setup.BasePerm
 import ConNF.Setup.Litter
 import ConNF.Setup.NearLitter
 import ConNF.Setup.Params

ConNF/Aux/Set.lean

@@ -1,6 +1,7 @@
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Data.Set.Pointwise.SMul
 
-open scoped symmDiff
+open scoped symmDiff Pointwise
 
 theorem Set.symmDiff_trans_subset {α : Type _} (s t u : Set α) :
     s ∆ u ⊆ s ∆ t ∪ t ∆ u := by
@@ -28,3 +29,7 @@ theorem Set.inter_subset_symmDiff_union_symmDiff {α : Type _} {s t u v : Set α
   simp only [Set.disjoint_iff, subset_def, mem_empty_iff_false] at h
   simp only [mem_inter_iff, mem_union, and_imp, mem_symmDiff]
   tauto
+
+theorem Set.smulSet_def {α β : Type _} {x : α} {s : Set β} [SMul α β] :
+    x • s = (x • ·) '' s :=
+  rfl

ConNF/Setup/Atom.lean

@@ -47,7 +47,6 @@ theorem mem_litter_atoms_iff (a : Atom) (L : Litter) :
     a ∈ Lᴬ ↔ aᴸ = L :=
   Iff.rfl
 
-@[ext]
 theorem Atom.ext {a₁ a₂ : Atom} (h : a₁ᴸ = a₂ᴸ) (h' : a₁.index = a₂.index) : a₁ = a₂ := by
   obtain ⟨L₁, i₁⟩ := a₁
   obtain ⟨L₂, i₂⟩ := a₂

ConNF/Setup/BasePerm.lean

@@ -0,0 +1,161 @@
+import Mathlib.Logic.Equiv.Defs
+import ConNF.Setup.NearLitter
+
+/-!
+# Base permutations
+
+In this file, we define the group of base permutations, and their actions on atoms, litters, and
+near-litters.
+
+## Main declarations
+
+* `ConNF.BasePerm`: The type of base permutations.
+-/
+
+universe u
+
+open Cardinal Equiv
+open scoped Pointwise
+
+namespace ConNF
+
+variable [Params.{u}]
+
+structure BasePerm where
+  atoms : Perm Atom
+  litters : Perm Litter
+  apply_near_apply (s : Set Atom) (L : Litter) : Near s Lᴬ → Near (atoms '' s) (litters L)ᴬ
+
+namespace BasePerm
+
+instance : SuperA BasePerm (Perm Atom) where
+  superA := atoms
+
+instance : SuperL BasePerm (Perm Litter) where
+  superL := litters
+
+instance : SMul BasePerm Atom where
+  smul π a := πᴬ a
+
+instance : SMul BasePerm Litter where
+  smul π L := πᴸ L
+
+theorem smul_near_smul (π : BasePerm) (s : Set Atom) (L : Litter) :
+    Near s Lᴬ → Near (π • s) (π • L)ᴬ :=
+  π.apply_near_apply s L
+
+instance : SMul BasePerm NearLitter where
+  smul π N := ⟨π • Nᴸ, π • Nᴬ, π.smul_near_smul Nᴬ Nᴸ N.atoms_near_litter⟩
+
+theorem smul_atom_def (π : BasePerm) (a : Atom) :
+    π • a = πᴬ a :=
+  rfl
+
+theorem smul_litter_def (π : BasePerm) (L : Litter) :
+    π • L = πᴸ L :=
+  rfl
+
+@[simp]
+theorem smul_nearLitter_atoms (π : BasePerm) (N : NearLitter) :
+    (π • N)ᴬ = π • Nᴬ :=
+  rfl
+
+@[ext]
+theorem ext {π₁ π₂ : BasePerm} (h : ∀ a : Atom, π₁ • a = π₂ • a) :
+    π₁ = π₂ := by
+  obtain ⟨πa₁, πl₁, h₁⟩ := π₁
+  obtain ⟨πa₂, πl₂, h₂⟩ := π₂
+  rw [mk.injEq]
+  have : πa₁ = πa₂ := by ext a; exact h a
+  refine ⟨this, ?_⟩
+  ext L
+  have h₁' := h₁ Lᴬ L near_rfl
+  have h₂' := h₂ Lᴬ L near_rfl
+  rw [this] at h₁'
+  exact litter_eq_of_near <| near_trans (near_symm h₁') h₂'
+
+instance : One BasePerm where
+  one := ⟨1, 1, λ s L h ↦ by simpa only [Perm.coe_one, id_eq, Set.image_id']⟩
+
+@[simp]
+theorem one_atom :
+    (1 : BasePerm)ᴬ = 1 :=
+  rfl
+
+@[simp]
+theorem one_litter :
+    (1 : BasePerm)ᴸ = 1 :=
+  rfl
+
+instance : Mul BasePerm where
+  mul π₁ π₂ := ⟨π₁ᴬ * π₂ᴬ, π₁ᴸ * π₂ᴸ, λ s L h ↦ by
+    have := π₁.smul_near_smul _ _ <| π₂.smul_near_smul s L h
+    simpa only [Set.smulSet_def, Set.image_image] using this⟩
+
+@[simp]
+theorem mul_atom (π₁ π₂ : BasePerm) :
+    (π₁ * π₂)ᴬ = π₁ᴬ * π₂ᴬ :=
+  rfl
+
+@[simp]
+theorem mul_litter (π₁ π₂ : BasePerm) :
+    (π₁ * π₂)ᴸ = π₁ᴸ * π₂ᴸ :=
+  rfl
+
+theorem inv_smul_near_inv_smul (π : BasePerm) (s : Set Atom) (L : Litter) :
+    Near s Lᴬ → Near (πᴬ⁻¹ • s) (πᴸ⁻¹ • L)ᴬ := by
+  intro h
+  apply near_trans (near_image h ↑πᴬ⁻¹)
+  have := π.smul_near_smul (πᴸ⁻¹ L)ᴬ (πᴸ⁻¹ L) near_rfl
+  have := near_image this ↑πᴬ⁻¹
+  simp only [smul_litter_def, smul_atom_def, Perm.apply_inv_self, Set.smulSet_def,
+    Perm.image_inv, preimage_image] at this
+  rw [Perm.image_inv]
+  exact near_symm this
+
+instance : Inv BasePerm where
+  inv π := ⟨πᴬ⁻¹, πᴸ⁻¹, π.inv_smul_near_inv_smul⟩
+
+@[simp]
+theorem inv_atom (π : BasePerm) :
+    π⁻¹ᴬ = πᴬ⁻¹ :=
+  rfl
+
+@[simp]
+theorem inv_litter (π : BasePerm) :
+    π⁻¹ᴸ = πᴸ⁻¹ :=
+  rfl
+
+instance : Group BasePerm where
+  mul_assoc π₁ π₂ π₃ := by
+    ext a
+    simp only [smul_atom_def, mul_atom, mul_assoc]
+  one_mul π := by
+    ext a
+    simp only [smul_atom_def, mul_atom, one_atom, one_mul]
+  mul_one π := by
+    ext a
+    simp only [smul_atom_def, mul_atom, one_atom, mul_one]
+  inv_mul_cancel π := by
+    ext a
+    simp only [smul_atom_def, mul_atom, inv_atom, inv_mul_cancel, Perm.coe_one, id_eq, one_atom]
+
+instance : MulAction BasePerm Atom where
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+instance : MulAction BasePerm Litter where
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+instance : MulAction BasePerm NearLitter where
+  one_smul N := by
+    ext a
+    simp only [smul_nearLitter_atoms, one_smul]
+  mul_smul π₁ π₂ N := by
+    ext a
+    simp only [smul_nearLitter_atoms, mul_smul]
+
+end BasePerm
+
+end ConNF

ConNF/Setup/NearLitter.lean

@@ -13,7 +13,6 @@ In this file, we define near-litters.
     difference if the two near-litters are near, and equal to their intersection if they are not.
 -/
 
-noncomputable section
 universe u
 
 open Cardinal Set

ConNF/Setup/Small.lean

@@ -131,6 +131,9 @@ theorem near_trans (h₁ : Near s t) (h₂ : Near t u) : Near s u :=
 theorem near_symmDiff_self_of_small (h : Small s) : Near (s ∆ t) t := by
   rwa [Near, symmDiff_symmDiff_cancel_right]
 
+theorem near_image (h : Near s t) (f : α → β) : Near (f '' s) (f '' t) :=
+  (h.image f).mono subset_image_symmDiff
+
 theorem card_le_of_near (h₁ : Near s t) (h₂ : ¬Small t) : #t ≤ #s := by
   rw [Near, Small, Set.symmDiff_def, mk_union_of_disjoint disjoint_sdiff_sdiff] at h₁
   rw [Small, not_lt] at h₂

blueprint/src/chapters/environment.tex

@@ -104,6 +104,8 @@ \section{Model parameters}
 \begin{definition}[base permutation]
   \label{def:BasePerm}
   \uses{def:Atom,def:Litter,def:NearLitter}
+  \lean{ConNF.BasePerm}
+  \leanok
   A \emph{base permutation} is a pair \( \pi = (\pi^\Atom, \pi^\Litter) \), where \( \pi^\Atom \) is a permutation \( \Atom \simeq \Atom \) and \( \pi^\Litter \) is a permutation \( \Litter \simeq \Litter \), such that
   \[ \pi^\Atom[\LS(L)] \near \LS(\pi^\Litter(L)) \]
   Base permutations have a natural group structure, they act on atoms by \( \pi^\Atom \), they act on litters by \( \pi^\Litter \), and they act on near-litters by\footnote{We need to emphasise these properties, rather than emphasising the real definition \( \pi(N) = (\pi(N^\circ), \pi[N]) \).}
@@ -239,7 +241,7 @@ \section{The structural hierarchy}
 \end{definition}
 \begin{definition}[structural support]
   \label{def:StrSupport}
-  \uses{def:BaseSupport,def:Tree}
+  \uses{def:BaseSupport}
   A \emph{\( \beta \)-structural support} (or just \emph{\( \beta \)-support}) is a pair \( S = (S^\Atom, S^\NearLitter) \) where \( S^\Atom \) is an enumeration of \( (\beta \tpath \bot) \times \Atom \) and \( S^\NearLitter \) is an enumeration of \( (\beta \tpath \bot) \times \NearLitter \).
   The type of \( \beta \)-supports is written \( \StrSupp_\beta \).
   There are precisely \( \#\mu \) structural supports for any type index \( \beta \).