From 0eccb77459e317b44dcfdb75a4791f124ac8b19e Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 6 Feb 2025 08:10:04 +0000 Subject: [PATCH] feat: Update FieldSpecification and asymptotic fields --- HepLean.lean | 1 - .../FieldOpAlgebra/Basic.lean | 12 ++-- .../FieldOpFreeAlgebra/Basic.lean | 12 ++-- .../FieldSpecification/Basic.lean | 69 ++++++++++++------- .../FieldSpecification/Examples.lean | 40 ----------- scripts/MetaPrograms/notes.lean | 1 - 6 files changed, 55 insertions(+), 80 deletions(-) delete mode 100644 HepLean/PerturbationTheory/FieldSpecification/Examples.lean diff --git a/HepLean.lean b/HepLean.lean index 0b677c1..3ea8b57 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -148,7 +148,6 @@ import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder import HepLean.PerturbationTheory.FieldSpecification.Basic import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp import HepLean.PerturbationTheory.FieldSpecification.CrAnSection -import HepLean.PerturbationTheory.FieldSpecification.Examples import HepLean.PerturbationTheory.FieldSpecification.Filters import HepLean.PerturbationTheory.FieldSpecification.NormalOrder import HepLean.PerturbationTheory.FieldSpecification.TimeOrder diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean index e224ca8..dbd052f 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean @@ -512,18 +512,18 @@ def anPart (Ο† : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (anPartF Ο†) lemma anPart_eq_ΞΉ_anPartF (Ο† : 𝓕.FieldOp) : anPart Ο† = ΞΉ (anPartF Ο†) := rfl @[simp] -lemma anPart_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma anPart_negAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : anPart (FieldOp.inAsymp Ο†) = 0 := by simp [anPart, anPartF] @[simp] -lemma anPart_position (Ο† : 𝓕.Fields Γ— SpaceTime) : +lemma anPart_position (Ο† : 𝓕.positionDOF Γ— SpaceTime) : anPart (FieldOp.position Ο†) = ofCrAnFieldOp ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ := by simp [anPart, ofCrAnFieldOp] @[simp] -lemma anPart_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma anPart_posAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : anPart (FieldOp.outAsymp Ο†) = ofCrAnFieldOp ⟨FieldOp.outAsymp Ο†, ()⟩ := by simp [anPart, ofCrAnFieldOp] @@ -533,18 +533,18 @@ def crPart (Ο† : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (crPartF Ο†) lemma crPart_eq_ΞΉ_crPartF (Ο† : 𝓕.FieldOp) : crPart Ο† = ΞΉ (crPartF Ο†) := rfl @[simp] -lemma crPart_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma crPart_negAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : crPart (FieldOp.inAsymp Ο†) = ofCrAnFieldOp ⟨FieldOp.inAsymp Ο†, ()⟩ := by simp [crPart, ofCrAnFieldOp] @[simp] -lemma crPart_position (Ο† : 𝓕.Fields Γ— SpaceTime) : +lemma crPart_position (Ο† : 𝓕.positionDOF Γ— SpaceTime) : crPart (FieldOp.position Ο†) = ofCrAnFieldOp ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ := by simp [crPart, ofCrAnFieldOp] @[simp] -lemma crPart_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma crPart_posAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : crPart (FieldOp.outAsymp Ο†) = 0 := by simp [crPart] diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean index 2c31d04..3aa932c 100644 --- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean @@ -131,18 +131,18 @@ def crPartF : 𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra := fun Ο† => | FieldOp.outAsymp _ => 0 @[simp] -lemma crPartF_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma crPartF_negAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : crPartF (FieldOp.inAsymp Ο†) = ofCrAnOpF ⟨FieldOp.inAsymp Ο†, ()⟩ := by simp [crPartF] @[simp] -lemma crPartF_position (Ο† : 𝓕.Fields Γ— SpaceTime) : +lemma crPartF_position (Ο† : 𝓕.positionDOF Γ— SpaceTime) : crPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ := by simp [crPartF] @[simp] -lemma crPartF_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma crPartF_posAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : crPartF (FieldOp.outAsymp Ο†) = 0 := by simp [crPartF] @@ -156,18 +156,18 @@ def anPartF : 𝓕.FieldOp β†’ 𝓕.FieldOpFreeAlgebra := fun Ο† => | FieldOp.outAsymp Ο† => ofCrAnOpF ⟨FieldOp.outAsymp Ο†, ()⟩ @[simp] -lemma anPartF_negAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma anPartF_negAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : anPartF (FieldOp.inAsymp Ο†) = 0 := by simp [anPartF] @[simp] -lemma anPartF_position (Ο† : 𝓕.Fields Γ— SpaceTime) : +lemma anPartF_position (Ο† : 𝓕.positionDOF Γ— SpaceTime) : anPartF (FieldOp.position Ο†) = ofCrAnOpF ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ := by simp [anPartF] @[simp] -lemma anPartF_posAsymp (Ο† : 𝓕.Fields Γ— Lorentz.Contr 4) : +lemma anPartF_posAsymp (Ο† : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ)) : anPartF (FieldOp.outAsymp Ο†) = ofCrAnOpF ⟨FieldOp.outAsymp Ο†, ()⟩ := by simp [anPartF] diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean index d734363..adddb8c 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean @@ -23,44 +23,57 @@ From each field we can create three different types of `FieldOp`. These states carry the same field statistic as the field they are derived from. +## Some references + +- https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf + -/ -remark fieldSpecification_intro := "The raw ingredients of a field theory are: - - The specification of the fields. - - Whether each field is a boson or a fermion. - - Vertices present in the Lagrangian. - - The coefficent of each vertex. - - We call the first two of these ingredients the `FieldSpecification` of the theory. " - -/-- A field specification is a type, `Fields`, elements of which are fields - present in a theory, and a map `statistics` from `Fields` to `FieldStatistic` which - identifies each field as a boson or a fermion. -/ +/-- A field specification is defined as a structure containing the basic data needed to write down + position and asymptotic field operators for a theory. It contains: + - A type `positionDOF` containing the degree-of-freedom in position-based field + operators (excluding space-time position). Thus a sutible (but not unique) choice + - Real-scalar fields correspond to a single element of `positionDOF`. + - Complex-scalar fields correspond to two elements of `positionDOF`, one for the field and one + for its conjugate. + - Dirac fermions correspond to eight elements of `positionDOF`. One for each Lorentz index of the + field and its conjugate. (These are not all independent) + - Weyl fermions correspond to four elements of `positionDOF`. One for each Lorentz index of the + field. (These are not all independent) + - A type `asymptoticDOF` containing the degree-of-freedom in asymptotic field operators. Thus a + sutible (but not unique) choice is + - Real-scalar fields correspond to a single element of `asymptoticDOF`. + - Complex-scalar fields correspond to two elements of `asymptoticDOF`, one for the field and one + for its conjugate. + - Dirac fermions correspond to four elements of `asymptoticDOF`, two for each type of spin. + - Weyl fermions correspond to two elements of `asymptoticDOF`, one for each spin. + - A specification `statisticsPos` on a `positionDOF` is Fermionic or Bosonic. + - A specification `statisticsAsym` on a `asymptoticDOF` is Fermionic or Bosonic. +-/ structure FieldSpecification where - /-- The type of fields. This also includes anti-states. -/ - Fields : Type - /-- The specification if a field is bosonic or fermionic. -/ - statistics : Fields β†’ FieldStatistic + /-- Degrees of freedom for position based field operators. -/ + positionDOF : Type + /-- Degrees of freedom for asymptotic based field operators. -/ + asymptoticDOF : Type + /-- The specification if the `positionDOF` are Fermionic or Bosonic. -/ + statisticsPos : positionDOF β†’ FieldStatistic + /-- The specification if the `asymptoticDOF` are Fermionic or Bosonic. -/ + statisticsAsym : asymptoticDOF β†’ FieldStatistic namespace FieldSpecification variable (𝓕 : FieldSpecification) /-- For a field specification `𝓕`, the type `𝓕.FieldOp` is defined such that every element of `FieldOp` corresponds either to: -- an incoming asymptotic field operator `.inAsymp` specified by a field and a `4`-momentum. +- an incoming asymptotic field operator `.inAsymp` specified by a field and a `3`-momentum. - an position operator `.position` specified by a field and a point in spacetime. -- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `4`-momentum. +- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `3`-momentum. -/ inductive FieldOp (𝓕 : FieldSpecification) where - | inAsymp : 𝓕.Fields Γ— Lorentz.Contr 4 β†’ 𝓕.FieldOp - | position : 𝓕.Fields Γ— SpaceTime β†’ 𝓕.FieldOp - | outAsymp : 𝓕.Fields Γ— Lorentz.Contr 4 β†’ 𝓕.FieldOp + | inAsymp : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ) β†’ 𝓕.FieldOp + | position : 𝓕.positionDOF Γ— SpaceTime β†’ 𝓕.FieldOp + | outAsymp : 𝓕.asymptoticDOF Γ— (Fin 3 β†’ ℝ) β†’ 𝓕.FieldOp -/-- Taking a field operator to its underlying field. -/ -def fieldOpToField : 𝓕.FieldOp β†’ 𝓕.Fields - | FieldOp.inAsymp Ο† => Ο†.1 - | FieldOp.position Ο† => Ο†.1 - | FieldOp.outAsymp Ο† => Ο†.1 /-- The bool on `FieldOp` which is true only for position field operator. -/ def statesIsPosition : 𝓕.FieldOp β†’ Bool @@ -68,7 +81,11 @@ def statesIsPosition : 𝓕.FieldOp β†’ Bool | _ => false /-- The statistics associated to a field operator. -/ -def statesStatistic : 𝓕.FieldOp β†’ FieldStatistic := 𝓕.statistics ∘ 𝓕.fieldOpToField +def statesStatistic : 𝓕.FieldOp β†’ FieldStatistic := fun f => + match f with + | FieldOp.inAsymp (a, _) => 𝓕.statisticsAsym a + | FieldOp.position (a, _) => 𝓕.statisticsPos a + | FieldOp.outAsymp (a, _) => 𝓕.statisticsAsym a /-- The field statistics associated with a field operator. -/ scoped[FieldSpecification] notation 𝓕 "|>β‚›" Ο† => statesStatistic 𝓕 Ο† diff --git a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean deleted file mode 100644 index c1461dc..0000000 --- a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean +++ /dev/null @@ -1,40 +0,0 @@ -/- -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.FieldSpecification.Basic -/-! - -# Specific examples of field specifications - --/ - -namespace FieldSpecification -variable (𝓕 : FieldSpecification) - -/-- The Field specification corresponding to a single bosonic field. - The type of fields is the unit type, and the statistic of the unique element of the unit - type is bosonic. -/ -def singleBoson : FieldSpecification where - Fields := Unit - statistics := fun _ => FieldStatistic.bosonic - -/-- The Field specification corresponding to a single fermionic field. - The type of fields is the unit type, and the statistic of the unique element of the unit - type is fermionic. -/ -def singleFermion : FieldSpecification where - Fields := Unit - statistics := fun _ => FieldStatistic.fermionic - -/-- The Field specification corresponding to two bosonic fields and two fermionic fields. - The type of fields is `Fin 2 βŠ• Fin 2`, and the statistic of the two `.inl` (left) elements - is bosonic and the statistic of the two `.inr` (right) elements is fermionic. -/ -def doubleBosonDoubleFermion : FieldSpecification where - Fields := Fin 2 βŠ• Fin 2 - statistics := fun b => - match b with - | Sum.inl _ => FieldStatistic.bosonic - | Sum.inr _ => FieldStatistic.fermionic - -end FieldSpecification diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 4168a8e..1be3757 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -130,7 +130,6 @@ def perturbationTheory : Note where .name `FieldStatistic.instCommGroup, .name `FieldStatistic.exchangeSign, .h2 "Field specifications", - .name `fieldSpecification_intro, .name `FieldSpecification, .h2 "Field operators", .name `FieldSpecification.FieldOp,