refactor: Separate contractions

HEPLean · Jan 17, 2025 · 9c7c475 · 9c7c475
1 parent 6294923
commit 9c7c475
Show file tree

Hide file tree

Showing 9 changed files with 536 additions and 504 deletions.
diff --git a/HepLean.lean b/HepLean.lean
@@ -133,7 +133,6 @@ import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
 import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
 import HepLean.PerturbationTheory.FieldStatistics
 import HepLean.PerturbationTheory.FieldStruct.Basic
-import HepLean.PerturbationTheory.FieldStruct.Contractions
 import HepLean.PerturbationTheory.FieldStruct.CreateAnnihilate
 import HepLean.PerturbationTheory.FieldStruct.CreateAnnihilateAlgebra
 import HepLean.PerturbationTheory.FieldStruct.CreateAnnihilateSect

diff --git a/HepLean/PerturbationTheory/Contractions/Basic.lean b/HepLean/PerturbationTheory/Contractions/Basic.lean
@@ -23,15 +23,8 @@ namespace ContractionsNat
 variable {n : ℕ} (c : ContractionsNat n)
 open HepLean.List
 
-local instance : IsTotal (Fin n × Fin n) (fun a b => a.1 ≤ b.1) where
-  total := by
-    intro a b
-    exact le_total a.1 b.1
-
-local instance : IsTrans (Fin n × Fin n) (fun a b => a.1 ≤ b.1) where
-  trans := by
-    intro a b c ha hb
-    exact Fin.le_trans ha hb
+/-- The contraction consisting of no contracted pairs. -/
+def nil : ContractionsNat n := ⟨∅, by simp, by simp⟩
 
 def congr : {n m : ℕ} → (h : n = m) → ContractionsNat n ≃ ContractionsNat m
   | n, .(n), rfl => Equiv.refl _

diff --git a/HepLean/PerturbationTheory/Contractions/ExtractEquiv.lean b/HepLean/PerturbationTheory/Contractions/ExtractEquiv.lean
@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Contractions.Insert
+/-!
+
+# Equivalence extracting element from contraction
+
+
+-/
+
+namespace FieldStruct
+variable {𝓕 : FieldStruct}
+
+namespace ContractionsNat
+variable {n : ℕ} (c : ContractionsNat n)
+open HepLean.List
+open HepLean.Fin
+
+
+lemma extractEquiv_equiv {c1 c2 : (c : ContractionsNat n) × Option c.uncontracted}
+    (h : c1.1 = c2.1) (ho : c1.2 = uncontractedCongr (by rw [h]) c2.2) : c1 = c2 := by
+  cases c1
+  cases c2
+  simp_all
+  simp at h
+  subst h
+  simp [uncontractedCongr]
+  rename_i a
+  match a with
+  | none => simp
+  | some a =>
+    simp
+    ext
+    simp
+
+
+def extractEquiv (i : Fin n.succ) : ContractionsNat n.succ ≃
+    (c : ContractionsNat n) × Option c.uncontracted  where
+  toFun := fun c => ⟨erase c i, getDualErase c i⟩
+  invFun := fun ⟨c, j⟩ => insert c i j
+  left_inv f := by
+    simp
+  right_inv f := by
+    refine extractEquiv_equiv ?_ ?_
+    simp
+    simp
+    have h1 := insert_getDualErase f.fst i f.snd
+    exact insert_getDualErase _ i _
+
+lemma extractEquiv_symm_none_uncontracted (i : Fin n.succ)  (c : ContractionsNat n) :
+    ((extractEquiv i).symm ⟨c, none⟩).uncontracted =
+    (Insert.insert i (c.uncontracted.map i.succAboveEmb)) := by
+  exact insert_none_uncontracted c i
+
+@[simp]
+lemma extractEquiv_apply_congr_symm_apply {n m : ℕ} (k : ℕ)
+    (hnk :  k < n.succ) (hkm : k < m.succ) (hnm : n = m) (c : ContractionsNat n)
+     (i  : c.uncontracted) :
+    congr (by rw [hnm]) ((extractEquiv ⟨k, hkm⟩
+    (congr (by rw [hnm]) ((extractEquiv ⟨k, hnk⟩).symm ⟨c, i⟩)))).1 = c := by
+  subst hnm
+  simp
+
+instance fintype_zero : Fintype (ContractionsNat 0) where
+  elems := {nil}
+  complete := by
+    intro c
+    simp
+    apply Subtype.eq
+    simp [nil]
+    ext a
+    apply Iff.intro
+    · intro h
+      have hc := c.2.1 a h
+      rw [Finset.card_eq_two] at hc
+      obtain ⟨x, y, hxy, ha⟩ := hc
+      exact Fin.elim0 x
+    · simp
+
+lemma sum_contractionsNat_nil (f : ContractionsNat 0 → M) [AddCommMonoid M] :
+    ∑ c, f c = f nil := by
+  rw [Finset.sum_eq_single_of_mem]
+  simp
+  intro b hb
+  fin_cases b
+  simp
+
+instance fintype_succ : (n : ℕ) → Fintype (ContractionsNat n)
+  | 0 => fintype_zero
+  | Nat.succ n => by
+    letI := fintype_succ n
+    exact Fintype.ofEquiv _ (extractEquiv 0).symm
+
+
+lemma sum_extractEquiv_congr [AddCommMonoid M] {n m : ℕ} (i : Fin n) (f : ContractionsNat n → M)
+    (h : n = m.succ) :
+    ∑ c, f c = ∑ (c : ContractionsNat m), ∑ (k : Option c.uncontracted),
+    f (congr h.symm ((extractEquiv (finCongr h i)).symm ⟨c, k⟩))  := by
+  subst h
+  simp only [finCongr_refl, Equiv.refl_apply, congr_refl]
+  rw [← (extractEquiv i).symm.sum_comp]
+  rw [Finset.sum_sigma']
+  rfl
+
+end ContractionsNat
+
+end FieldStruct
diff --git a/HepLean/PerturbationTheory/Contractions/Insert.lean b/HepLean/PerturbationTheory/Contractions/Insert.lean
@@ -684,248 +684,6 @@ lemma insertLiftSome_bijective {c : ContractionsNat n} (i : Fin n.succ) (j : c.u
   ⟨insertLiftSome_injective i j, insertLiftSome_surjective i j⟩
 
 
-/-!
-
-## Inserting an element into a list
-
--/
-
-def insertList (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted)) :
-    ContractionsNat (φs.insertIdx i φ).length :=
-    congr (by simp) (c.insert i j)
-
-@[simp]
-lemma insertList_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted))
-    (a : c.1) : (insertList φ φs c i j).fstFieldOfContract
-    (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
-    finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (c.fstFieldOfContract a)) := by
-  simp [insertList]
-
-@[simp]
-lemma insertList_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted))
-    (a : c.1) : (insertList φ φs c i j).sndFieldOfContract
-    (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
-    finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (c.sndFieldOfContract a)) := by
-  simp [insertList]
-
-@[simp]
-lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-      (insertList φ φs c i (some j)).fstFieldOfContract
-      (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) =
-      if i < i.succAbove j.1 then
-      finCongr (insertIdx_length_fin φ φs i).symm i else
-      finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) := by
-  split
-  · rename_i h
-    refine (insertList φ φs c i (some j)).eq_fstFieldOfContract_of_mem
-      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
-      (i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=
-        finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_
-    · simp [congrLift]
-    · simp [congrLift]
-    · rw [Fin.lt_def] at h ⊢
-      simp_all
-  · rename_i h
-    refine (insertList φ φs c i (some j)).eq_fstFieldOfContract_of_mem
-      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
-       (i :=
-        finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
-        (j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_
-    · simp [congrLift]
-    · simp [congrLift]
-    · rw [Fin.lt_def] at h ⊢
-      simp_all
-      have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
-      omega
-
-/-!
-
-## insertList and getDual?
-
--/
-@[simp]
-lemma insertList_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ)  :
-    (insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by
-  simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans,
-    Fin.cast_eq_self, Option.map_eq_none']
-  have h1 := c.insert_none_getDual?_isNone i
-  simpa using h1
-
-@[simp]
-lemma insertList_isSome_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-    ((insertList φ φs c i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)).isSome := by
-  simp [insertList, getDual?_congr]
-
-
-@[simp]
-lemma insertList_some_getDual?_self_not_none (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-    ¬ ((insertList φ φs c i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)) = none := by
-  simp [insertList, getDual?_congr]
-
-@[simp]
-lemma insertList_some_getDual?_self_eq (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-    ((insertList φ φs c i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i))
-    =  some (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) := by
-  simp [insertList, getDual?_congr]
-
-
-@[simp]
-lemma insertList_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-    ((insertList φ φs c i (some j)).getDual?
-      (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)))
-    =  some (Fin.cast (insertIdx_length_fin φ φs i).symm i) := by
-  rw [getDual?_eq_some_iff_mem]
-  rw [@Finset.pair_comm]
-  rw [← getDual?_eq_some_iff_mem]
-  simp
-
-@[simp]
-lemma insertList_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
-    (insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove j)) = none ↔ c.getDual? j = none := by
-  simp [insertList, getDual?_congr]
-
-@[simp]
-lemma insertList_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
-    (k : c.uncontracted) (hkj : j ≠ k.1) :
-    (insertList φ φs c i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove j)) = Option.map (Fin.cast (insertIdx_length_fin φ φs i).symm ∘ i.succAbove ) (c.getDual? j) := by
-  simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans,
-    Fin.cast_eq_self, ne_eq, hkj, not_false_eq_true, insert_some_getDual?_of_neq, Option.map_map]
-  rfl
-
-
-@[simp]
-lemma insertList_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
-    ((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove j))).isSome ↔  (c.getDual? j).isSome := by
-  rw [← not_iff_not]
-  simp
-
-@[simp]
-lemma insertList_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States)
-      (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
-      (h : ((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove j))).isSome):
-      ((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove j))).get h = Fin.cast (insertIdx_length_fin φ φs i).symm
-      (i.succAbove ((c.getDual? j).get (by simpa using h))) := by
-  simp [insertList, getDual?_congr_get]
-
-
-/-........................................... -/
-@[simp]
-lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) : (insertList φ φs c i (some j)).sndFieldOfContract
-      (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) =
-      if i < i.succAbove j.1 then
-      finCongr (insertIdx_length_fin φ φs i).symm  (i.succAbove j.1) else
-      finCongr (insertIdx_length_fin φ φs i).symm  i := by
-  split
-  · rename_i h
-    refine (insertList φ φs c i (some j)).eq_sndFieldOfContract_of_mem
-      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
-      (i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=
-        finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_
-    · simp [congrLift]
-    · simp [congrLift]
-    · rw [Fin.lt_def] at h ⊢
-      simp_all
-  · rename_i h
-    refine (insertList φ φs c i (some j)).eq_sndFieldOfContract_of_mem
-      (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
-       (i :=
-        finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
-        (j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_
-    · simp [congrLift]
-    · simp [congrLift]
-    · rw [Fin.lt_def] at h ⊢
-      simp_all
-      have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
-      omega
-
-lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ)
-    (f : (c.insertList φ φs i none).1 → M) [CommMonoid M] :
-    ∏ a, f a = ∏ (a : c.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i none a)) := by
-  let e1 := Equiv.ofBijective (c.insertLift i none) (insertLift_none_bijective i)
-  let e2 := Equiv.ofBijective (congrLift (insertIdx_length_fin φ φs i).symm)
-    ((c.insert i none).congrLift_bijective ((insertIdx_length_fin φ φs i).symm))
-  erw [← e2.prod_comp]
-  erw [← e1.prod_comp]
-  rfl
-
-
-lemma insertList_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : ContractionsNat φs.length) (i : Fin φs.length.succ) (j : c.uncontracted)
-    (f : (c.insertList φ φs i (some j)).1 → M) [CommMonoid M] :
-    ∏ a, f a = f (congrLift (insertIdx_length_fin φ φs i).symm
-      ⟨{i, i.succAbove j}, by simp [insert]⟩) *
-    ∏ (a : c.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i (some j) a)) := by
-  let e2 := Equiv.ofBijective (congrLift (insertIdx_length_fin φ φs i).symm)
-    ((c.insert i (some j)).congrLift_bijective ((insertIdx_length_fin φ φs i).symm))
-  erw [← e2.prod_comp]
-  let e1 := Equiv.ofBijective (c.insertLiftSome i j) (insertLiftSome_bijective i j)
-  erw [← e1.prod_comp]
-  rw [Fintype.prod_sum_type]
-  simp
-  rfl
-
-def insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States}
-    (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
-    Finset (Fin (φs.insertIdx i φ).length) :=
-    (a.map (Fin.succAboveEmb i)).map
-      (finCongr (insertIdx_length_fin φ φs i).symm).toEmbedding
-
-@[simp]
-lemma self_not_mem_insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States}
-    (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
-    Fin.cast (insertIdx_length_fin φ φs i).symm i ∉ insertListLiftFinset φ i a := by
-  simp [insertListLiftFinset]
-  intro x
-  exact fun a => Fin.succAbove_ne i x
-
-lemma succAbove_mem_insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States}
-    (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) (j : Fin φs.length) :
-    Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j) ∈ insertListLiftFinset φ i a ↔
-    j ∈ a := by
-  simp [insertListLiftFinset]
-  apply Iff.intro
-  · intro h
-    obtain ⟨x, hx1, hx2⟩ := h
-    rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hx2
-    simp_all
-  · intro h
-    use j
-
-lemma insert_fin_eq_self (φ : 𝓕.States) {φs : List 𝓕.States}
-    (i : Fin φs.length.succ) (j : Fin (List.insertIdx i φ φs).length) :
-    j = Fin.cast (insertIdx_length_fin φ φs i).symm i
-    ∨ ∃ k, j = Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) := by
-  obtain ⟨k, hk⟩ := (finCongr (insertIdx_length_fin φ φs i).symm).surjective j
-  subst hk
-  by_cases hi : k = i
-  · simp [hi]
-  · simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hi
-    obtain ⟨z, hk⟩ := hi
-    subst hk
-    right
-    use z
-    rfl
-
-
 end ContractionsNat
 
 end FieldStruct