feat: Field struct and creation and annihilation sections

HepLean/PerturbationTheory/CreateAnnihilate.lean

@@ -0,0 +1,50 @@
+/-
+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 Mathlib.Order.Defs.Unbundled
+import Mathlib.Data.Fintype.Basic
+/-!
+
+# Creation and annihlation parts of fields
+
+-/
+
+/-- The type specifing whether an operator is a creation or annihilation operator. -/
+inductive CreateAnnihilate where
+  | create : CreateAnnihilate
+  | annihilate : CreateAnnihilate
+deriving Inhabited, BEq, DecidableEq
+
+namespace CreateAnnihilate
+
+/-- The type `CreateAnnihilate` is finite. -/
+instance : Fintype CreateAnnihilate where
+  elems := {create, annihilate}
+  complete := by
+    intro c
+    cases c
+    · exact Finset.mem_insert_self create {annihilate}
+    · refine Finset.insert_eq_self.mp ?_
+      exact rfl
+
+/-- The normal ordering on creation and annihlation operators.
+  Creation operators are put to the left. -/
+def normalOrder : CreateAnnihilate → CreateAnnihilate → Prop
+  | create, create => True
+  | annihilate, annihilate => True
+  | create, annihilate => True
+  | annihilate, create => False
+
+/-- Normal ordering is total. -/
+instance : IsTotal CreateAnnihilate normalOrder where
+  total a b := by
+    cases a <;> cases b <;> simp [normalOrder]
+
+/-- Normal ordering is transitive. -/
+instance : IsTrans CreateAnnihilate normalOrder where
+  trans a b c := by
+    cases a <;> cases b <;> cases c <;> simp [normalOrder]
+
+end CreateAnnihilate

HepLean/PerturbationTheory/FieldStruct/Basic.lean

@@ -0,0 +1,74 @@
+/-
+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.Wick.OperatorMap
+import HepLean.Mathematics.Fin.Involutions
+import HepLean.Lorentz.RealVector.Basic
+import HepLean.SpaceTime.Basic
+/-!
+
+# Field structures
+
+-/
+
+/-- A field structure is a type of fields plus a specification of the
+  statistics (fermionic or bosonic) of each field. -/
+structure FieldStruct where
+  /-- The type of fields. -/
+  Fields : Type
+  /-- The specification if a field is bosonic or fermionic. -/
+  statistics : 𝓕 → FieldStatistic
+
+namespace FieldStruct
+variable (𝓕 : FieldStruct)
+
+/-- Negative asymptotic states are specified by a field and a momentum. -/
+def AsymptoticNegTime : Type := 𝓕.Fields × Lorentz.Contr 4
+
+/-- Positive asymptotic states are specified by a field and a momentum. -/
+def AsymptoticPosTime : Type := 𝓕.Fields × Lorentz.Contr 4
+
+/-- States specified by a field and a space-time position. -/
+def PositionStates : Type := 𝓕.Fields × SpaceTime
+
+/-- The combintation of asymptotic states and position states. -/
+inductive States (𝓕 : FieldStruct) where
+  | negAsymp : 𝓕.AsymptoticNegTime → 𝓕.States
+  | position : 𝓕.PositionStates → 𝓕.States
+  | posAsymp : 𝓕.AsymptoticPosTime → 𝓕.States
+
+/-- Taking a state to its underlying field. -/
+def statesToField : 𝓕.States → 𝓕.Fields
+  | States.negAsymp φ => φ.1
+  | States.position φ => φ.1
+  | States.posAsymp φ => φ.1
+
+/-- The statistics associated to a state. -/
+def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField
+
+/-- Returns true if `timeOrder a b` is true if `a` has time greater then or equal to `b`.
+  This will put the stats at the greatest time to left. -/
+def timeOrder : 𝓕.States → 𝓕.States → Prop
+  | States.posAsymp _, _ => True
+  | States.position φ0, States.position φ1 => φ1.2 0 ≤ φ0.2 0
+  | States.position _, States.negAsymp _ => True
+  | States.position _, States.posAsymp _ => False
+  | States.negAsymp _, States.posAsymp _ => False
+  | States.negAsymp _, States.position _ => False
+  | States.negAsymp _, States.negAsymp _ => True
+
+/-- Time ordering is total. -/
+instance : IsTotal 𝓕.States 𝓕.timeOrder where
+  total a b := by
+    cases a <;> cases b <;> simp [timeOrder]
+    exact LinearOrder.le_total _ _
+
+/-- Time ordering is transitive. -/
+instance : IsTrans 𝓕.States 𝓕.timeOrder where
+  trans a b c := by
+    cases a <;> cases b <;> cases c <;> simp [timeOrder]
+    exact fun h1 h2 => Preorder.le_trans _ _ _ h2 h1
+
+end FieldStruct

HepLean/PerturbationTheory/FieldStruct/CreateAnnihilate.lean

@@ -0,0 +1,78 @@
+/-
+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.FieldStruct.Basic
+import HepLean.PerturbationTheory.CreateAnnihilate
+/-!
+
+# Creation and annihlation parts of fields
+
+-/
+
+namespace FieldStruct
+variable (𝓕 : FieldStruct)
+
+/-- To each state the specificaition of the type of creation and annihlation parts.
+  For asymptotic staes there is only one allowed part, whilst for position states
+  there is two. -/
+def statesToCreateAnnihilateType : 𝓕.States → Type
+  | States.negAsymp _ => Unit
+  | States.position _ => CreateAnnihilate
+  | States.posAsymp _ => Unit
+
+/-- The instance of a finite type on `𝓕.statesToCreateAnnihilateType i`. -/
+instance : ∀ i, Fintype (𝓕.statesToCreateAnnihilateType i) := fun i =>
+  match i with
+  | States.negAsymp _ => inferInstanceAs (Fintype Unit)
+  | States.position _ => inferInstanceAs (Fintype CreateAnnihilate)
+  | States.posAsymp _ => inferInstanceAs (Fintype Unit)
+
+/-- The instance of a decidable equality on `𝓕.statesToCreateAnnihilateType i`. -/
+instance : ∀ i, DecidableEq (𝓕.statesToCreateAnnihilateType i) := fun i =>
+  match i with
+  | States.negAsymp _ => inferInstanceAs (DecidableEq Unit)
+  | States.position _ => inferInstanceAs (DecidableEq CreateAnnihilate)
+  | States.posAsymp _ => inferInstanceAs (DecidableEq Unit)
+
+/-- The equivalence between `𝓕.statesToCreateAnnihilateType i` and
+  `𝓕.statesToCreateAnnihilateType j` from an equality `i = j`. -/
+def statesToCreateAnnihilateTypeCongr : {i j : 𝓕.States} → i = j →
+  𝓕.statesToCreateAnnihilateType i ≃ 𝓕.statesToCreateAnnihilateType j
+  | _, _, rfl => Equiv.refl _
+
+/-- A creation and annihlation state is a state plus an valid specification of the
+  creation or annihliation part of that state. (For asympotic states there is only one valid
+  choice). -/
+def CreateAnnihilateStates : Type := Σ (s : 𝓕.States), 𝓕.statesToCreateAnnihilateType s
+
+/-- The map from creation and annihlation states to their underlying states. -/
+def createAnnihilateStatesToStates : 𝓕.CreateAnnihilateStates → 𝓕.States := Sigma.fst
+
+@[simp]
+lemma createAnnihilateStatesToStates_prod (s : 𝓕.States) (t : 𝓕.statesToCreateAnnihilateType s) :
+  𝓕.createAnnihilateStatesToStates ⟨s, t⟩ = s := rfl
+
+/-- The map from creation and annihlation states to the type `CreateAnnihilate`
+  specifying if a state is a creation or an annihilation state. -/
+def createAnnihlateStatesToCreateAnnihilate : 𝓕.CreateAnnihilateStates → CreateAnnihilate
+  | ⟨States.negAsymp _, _⟩ => CreateAnnihilate.create
+  | ⟨States.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create
+  | ⟨States.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
+  | ⟨States.posAsymp _, _⟩ => CreateAnnihilate.annihilate
+
+/-- The normal ordering on creation and annihlation states. -/
+def normalOrder : 𝓕.CreateAnnihilateStates → 𝓕.CreateAnnihilateStates → Prop :=
+  fun a b => CreateAnnihilate.normalOrder (𝓕.createAnnihlateStatesToCreateAnnihilate a)
+    (𝓕.createAnnihlateStatesToCreateAnnihilate b)
+
+/-- Normal ordering is total. -/
+instance : IsTotal 𝓕.CreateAnnihilateStates 𝓕.normalOrder where
+  total _ _ := total_of CreateAnnihilate.normalOrder _ _
+
+/-- Normal ordering is transitive. -/
+instance : IsTrans 𝓕.CreateAnnihilateStates 𝓕.normalOrder where
+  trans _ _ _ := fun h h' => IsTrans.trans (α := CreateAnnihilate) _ _ _ h h'
+
+end FieldStruct

HepLean/PerturbationTheory/FieldStruct/CreateAnnihilateSect.lean

@@ -0,0 +1,216 @@
+/-
+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.FieldStruct.CreateAnnihilate
+import HepLean.PerturbationTheory.CreateAnnihilate
+/-!
+
+# Creation and annihlation sections
+
+-/
+
+namespace FieldStruct
+variable {𝓕 : FieldStruct}
+
+/-- The sections in `𝓕.CreateAnnihilateStates` over a list `φs : List 𝓕.States`.
+  In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
+  each field as a `creation` or an `annilation` operator. E.g. the number of terms
+  `φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
+  operators at this point (e.g. ansymptotic states) this is accounted for. -/
+def CreateAnnihilateSect (φs : List 𝓕.States) : Type :=
+  {ψs : List 𝓕.CreateAnnihilateStates //
+    List.map 𝓕.createAnnihilateStatesToStates ψs = φs}
+  -- Π i, 𝓕.statesToCreateAnnihilateType (φs.get i)
+
+namespace CreateAnnihilateSect
+
+variable {𝓕 : FieldStruct} {φs : List 𝓕.States}
+
+@[simp]
+lemma length_eq (ψs : CreateAnnihilateSect φs) : ψs.1.length = φs.length := by
+  simpa using congrArg List.length ψs.2
+
+/-- The tail of a section for `φs`. -/
+def tail : {φs : List 𝓕.States} → (ψs : CreateAnnihilateSect φs) → CreateAnnihilateSect φs.tail
+  | [], ⟨[], h⟩ => ⟨[], h⟩
+  | φ :: φs, ⟨[], h⟩ => False.elim (by simp at h)
+  | φ :: φs, ⟨ψ :: ψs, h⟩ => ⟨ψs, by rw [List.map_cons, List.cons.injEq] at h; exact h.2⟩
+
+lemma head_state_eq {φ : 𝓕.States} : (ψs : CreateAnnihilateSect (φ :: φs)) →
+    (ψs.1.head (by simp [← List.length_pos_iff_ne_nil])).1 = φ
+  | ⟨[], h⟩ => False.elim (by simp at h)
+  | ⟨ψ :: ψs, h⟩ => by
+    simp at h
+    exact h.1
+
+/-- The head of a section for `φ :: φs` as an element in `𝓕.statesToCreateAnnihilateType φ`. -/
+def head : {φ : 𝓕.States} → (ψs : CreateAnnihilateSect (φ :: φs)) →
+    𝓕.statesToCreateAnnihilateType φ
+  | φ, ⟨[], h⟩ => False.elim (by simp at h)
+  | φ, ⟨ψ :: ψs, h⟩ => 𝓕.statesToCreateAnnihilateTypeCongr (by
+    simpa using head_state_eq ⟨ψ :: ψs, h⟩) ψ.2
+
+lemma eq_head_cons_tail {φ : 𝓕.States} {ψs : CreateAnnihilateSect (φ :: φs)} :
+    ψs.1 = ⟨φ, head ψs⟩ :: ψs.tail.1 := by
+  match ψs with
+  | ⟨[], h⟩ => exact False.elim (by simp at h)
+  | ⟨ψ :: ψs, h⟩ =>
+    have h2 := head_state_eq ⟨ψ :: ψs, h⟩
+    simp at h2
+    subst h2
+    rfl
+
+/-- The creation of a section from for `φ : φs` from a section for `φs` and a
+  element of `𝓕.statesToCreateAnnihilateType φ`. -/
+def cons {φ : 𝓕.States} (ψ : 𝓕.statesToCreateAnnihilateType φ) (ψs : CreateAnnihilateSect φs) :
+    CreateAnnihilateSect (φ :: φs) := ⟨⟨φ, ψ⟩ :: ψs.1, by
+  simp [List.map_cons, ψs.2]⟩
+
+/-- The creation and annihlation sections for a singleton list is given by
+  a choice of `𝓕.statesToCreateAnnihilateType φ`. If `φ` is a asymptotic state
+  there is no choice here, else there are two choices. -/
+def singletonEquiv {φ : 𝓕.States} : CreateAnnihilateSect [φ] ≃
+    𝓕.statesToCreateAnnihilateType φ where
+  toFun ψs := ψs.head
+  invFun ψ := ⟨[⟨φ, ψ⟩], by simp⟩
+  left_inv ψs := by
+    apply Subtype.ext
+    simp
+    have h1 := eq_head_cons_tail (ψs := ψs)
+    rw [h1]
+    have h2 := ψs.tail.2
+    simp at h2
+    simp [h2]
+  right_inv ψ := by
+    simp [head]
+    rfl
+
+/-- An equivalence seperating the head of a creation and annhilation section
+  from the tail. -/
+def consEquiv {φ : 𝓕.States} {φs : List 𝓕.States} : CreateAnnihilateSect (φ :: φs) ≃
+    𝓕.statesToCreateAnnihilateType φ × CreateAnnihilateSect φs where
+  toFun ψs := ⟨ψs.head, ψs.tail⟩
+  invFun ψψs :=
+    match ψψs with
+    | (ψ, ψs) => cons ψ ψs
+  left_inv ψs := by
+    apply Subtype.ext
+    exact Eq.symm eq_head_cons_tail
+  right_inv ψψs := by
+    match ψψs with
+    | (ψ, ψs) => rfl
+
+/-- The equivalence between `CreateAnnihilateSect φs` and
+  `CreateAnnihilateSect φs'` induced by an equality `φs = φs'`. -/
+def congr : {φs φs' : List 𝓕.States} → (h : φs = φs') →
+    CreateAnnihilateSect φs ≃ CreateAnnihilateSect φs'
+  | _, _, rfl => Equiv.refl _
+
+@[simp]
+lemma congr_fst {φs φs' : List 𝓕.States} (h : φs = φs') (ψs : CreateAnnihilateSect φs) :
+    (congr h ψs).1 = ψs.1 := by
+  cases h
+  rfl
+
+/-- Returns the first `n` elements of a section and its underlying list. -/
+def take (n : ℕ) (ψs : CreateAnnihilateSect φs) : CreateAnnihilateSect (φs.take n) :=
+  ⟨ψs.1.take n, by simp [ψs.2]⟩
+
+/-- Removes the first `n` elements of a section and its underlying list. -/
+def drop (n : ℕ) (ψs : CreateAnnihilateSect φs) : CreateAnnihilateSect (φs.drop n) :=
+  ⟨ψs.1.drop n, by simp [ψs.2]⟩
+
+/-- Appends two sections and their underlying lists. -/
+def append {φs φs' : List 𝓕.States} (ψs : CreateAnnihilateSect φs)
+    (ψs' : CreateAnnihilateSect φs') : CreateAnnihilateSect (φs ++ φs') :=
+  ⟨ψs.1 ++ ψs'.1, by simp [ψs.2, ψs'.2]⟩
+
+@[simp]
+lemma take_append_drop {n : ℕ} (ψs : CreateAnnihilateSect φs) :
+    append (take n ψs) (drop n ψs) = congr (List.take_append_drop n φs).symm ψs := by
+  apply Subtype.ext
+  simp [take, drop, append]
+
+@[simp]
+lemma congr_append {φs1 φs1' φs2 φs2' : List 𝓕.States}
+    (h1 : φs1 = φs1') (h2 : φs2 = φs2')
+    (ψs1 : CreateAnnihilateSect φs1) (ψs2 : CreateAnnihilateSect φs2) :
+    (append (congr h1 ψs1) (congr h2 ψs2)) = congr (by rw [h1, h2]) (append ψs1 ψs2) := by
+  subst h1 h2
+  rfl
+
+@[simp]
+lemma take_left {φs φs' : List 𝓕.States} (ψs : CreateAnnihilateSect φs)
+    (ψs' : CreateAnnihilateSect φs') :
+    take φs.length (ψs.append ψs') = congr (by simp) ψs := by
+  apply Subtype.ext
+  simp [take, append]
+
+@[simp]
+lemma drop_left {φs φs' : List 𝓕.States} (ψs : CreateAnnihilateSect φs)
+    (ψs' : CreateAnnihilateSect φs') :
+    drop φs.length (ψs.append ψs') = congr (by simp) ψs' := by
+  apply Subtype.ext
+  simp [drop, append]
+
+/-- The equivalence between `CreateAnnihilateSect (φs ++ φs')` and
+  `CreateAnnihilateSect φs × CreateAnnihilateSect φs` formed by `append`, `take`
+  and `drop` and their interrelationship. -/
+def appendEquiv {φs φs' : List 𝓕.States} : CreateAnnihilateSect (φs ++ φs') ≃
+    CreateAnnihilateSect φs × CreateAnnihilateSect φs' where
+  toFun ψs := (congr (List.take_left φs φs') (take φs.length ψs),
+    congr (List.drop_left φs φs') (drop φs.length ψs))
+  invFun ψsψs' := append ψsψs'.1 ψsψs'.2
+  left_inv ψs := by
+    apply Subtype.ext
+    simp
+  right_inv ψsψs' := by
+    match ψsψs' with
+    | (ψs, ψs') =>
+    simp
+    refine And.intro (Subtype.ext ?_) (Subtype.ext ?_)
+    · simp
+    · simp
+
+@[simp]
+lemma _root_.List.map_eraseIdx {α β : Type} (f : α → β) : (l : List α) → (n : ℕ) →
+    List.map f (l.eraseIdx n) = (List.map f l).eraseIdx n
+  | [], _ => rfl
+  | a :: l, 0 => rfl
+  | a :: l, n+1 => by
+    simp only [List.eraseIdx, List.map_cons, List.cons.injEq, true_and]
+    exact List.map_eraseIdx f l n
+
+/-- Erasing an element from a section and it's underlying list. -/
+def eraseIdx (n : ℕ) (ψs : CreateAnnihilateSect φs) : CreateAnnihilateSect (φs.eraseIdx n) :=
+  ⟨ψs.1.eraseIdx n, by simp [ψs.2]⟩
+
+/-- The equivalence formed by extracting an element from a section. -/
+def eraseIdxEquiv (n : ℕ) (φs : List 𝓕.States) (hn : n < φs.length) :
+    CreateAnnihilateSect φs ≃ 𝓕.statesToCreateAnnihilateType φs[n] ×
+    CreateAnnihilateSect (φs.eraseIdx n) :=
+  (congr (by simp only [List.take_concat_get', List.take_append_drop])).trans <|
+  appendEquiv.trans <|
+  (Equiv.prodCongr (appendEquiv.trans (Equiv.prodComm _ _)) (Equiv.refl _)).trans <|
+  (Equiv.prodAssoc _ _ _).trans <|
+  Equiv.prodCongr singletonEquiv <|
+  appendEquiv.symm.trans <|
+  congr (List.eraseIdx_eq_take_drop_succ φs n).symm
+
+@[simp]
+lemma eraseIdxEquiv_apply_snd {n : ℕ} (ψs : CreateAnnihilateSect φs) (hn : n < φs.length) :
+    (eraseIdxEquiv n φs hn ψs).snd = eraseIdx n ψs := by
+  apply Subtype.ext
+  simp only [eraseIdxEquiv, appendEquiv, take, List.take_concat_get', List.length_take, drop,
+    append, Equiv.trans_apply, Equiv.coe_fn_mk, congr_fst, Equiv.prodCongr_apply, Equiv.coe_trans,
+    Equiv.coe_prodComm, Equiv.coe_refl, Prod.map_apply, Function.comp_apply, Prod.swap_prod_mk,
+    id_eq, Equiv.prodAssoc_apply, Equiv.coe_fn_symm_mk, eraseIdx]
+  rw [Nat.min_eq_left (Nat.le_of_succ_le hn), Nat.min_eq_left hn, List.take_take]
+  simp only [Nat.succ_eq_add_one, le_add_iff_nonneg_right, zero_le, inf_of_le_left]
+  exact Eq.symm (List.eraseIdx_eq_take_drop_succ ψs.1 n)
+
+end CreateAnnihilateSect
+
+end FieldStruct