feat: Wick algebras
This commit is contained in:
jstoobysmith
parent
76250a0fe7
commit
db9f7ebfa9
6 changed files with 419 additions and 72 deletions
|
|
@ -62,8 +62,11 @@ unsafe def HTMLNote.ofInformal (name : Name) : MetaM HTMLNote := do
|
|||
++ "</div>"
|
||||
else if Informal.isInformalLemma constInfo then
|
||||
let X ← Informal.constantInfoToInformalLemma constInfo
|
||||
content := "Informal definition: " ++ name.toString ++ "\n" ++ X.math
|
||||
content := "Informal lemma: " ++ name.toString
|
||||
content := "<div class=\"informal-def\">"
|
||||
++ "<a href=\"" ++ webAddress ++ "\" class=\"button\">Improve/Formalize</a>"
|
||||
++"<b>Informal lemma:</b> " ++ name.toString ++ "<br>"
|
||||
++ X.math.replace "\n" "<br>"
|
||||
++ "</div>"
|
||||
pure { content := content, fileName := fileName, line := line }
|
||||
|
||||
end HepLean
|
||||
|
|
|
|||
|
|
@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.PerturbationTheory.Wick.Species
|
||||
import HepLean.Lorentz.RealVector.Basic
|
||||
import HepLean.Mathematics.Fin
|
||||
import HepLean.SpaceTime.Basic
|
||||
import HepLean.Mathematics.SuperAlgebra.Basic
|
||||
import HepLean.Meta.Notes.Basic
|
||||
import Init.Data.List.Sort.Basic
|
||||
/-!
|
||||
|
||||
# Operator algebra
|
||||
|
|
@ -60,71 +64,402 @@ the following super-commutators are zero:
|
|||
This basic structure constitutes what we call a Wick Algebra:
|
||||
"
|
||||
|
||||
informal_definition_note WickAlgebra where
|
||||
math :≈ "
|
||||
Modifications of this may be needed.
|
||||
A structure with the following data:
|
||||
- A super algebra A.
|
||||
- A map from `ψ : S.𝓯 × SpaceTime → A` where S.𝓯 are field colors.
|
||||
- A map `ψc : S.𝓯 × SpaceTime → A`.
|
||||
- A map `ψd : S.𝓯 × SpaceTime → A`.
|
||||
Subject to the conditions:
|
||||
- The sum of `ψc` and `ψd` is `ψ`.
|
||||
- All maps land on homogeneous elements.
|
||||
- Two fields super-commute if there colors are not dual to each other.
|
||||
- The super-commutator of two fields is always in the
|
||||
center of the algebra.
|
||||
Asympotic states:
|
||||
- `φc : S.𝓯 × MomentumSpace → A`. The creation asympotic state (incoming).
|
||||
- `φd : S.𝓯 × MomentumSpace → A`. The destruction asympotic state (outgoing).
|
||||
Subject to the conditions:
|
||||
...
|
||||
"
|
||||
physics :≈ "This is defined to be an
|
||||
abstraction of the notion of an operator algebra."
|
||||
ref :≈ "https://physics.stackexchange.com/questions/24157/"
|
||||
deps :≈ [``SuperAlgebra, ``SuperAlgebra.superCommuator]
|
||||
/-- The abstract notion of a operator algebra containing all the necessary ingrediants
|
||||
to do perturbation theory.
|
||||
Warning: The definition here is not complete. -/
|
||||
@[note_attr]
|
||||
structure WickAlgebra (S : Species) where
|
||||
/-- The underlying operator algebra. -/
|
||||
A : Type
|
||||
/-- The type `A` is a semiring. -/
|
||||
[A_semiring : Semiring A]
|
||||
/-- The type `A` is an algebra. -/
|
||||
[A_algebra : Algebra ℂ A]
|
||||
/-- Position based field operators. -/
|
||||
ψ : S.𝓯 → SpaceTime → A
|
||||
/-- Position based constructive operators. -/
|
||||
ψc : S.𝓯 → SpaceTime → A
|
||||
/-- Position based destructive operators. -/
|
||||
ψd : S.𝓯 → SpaceTime → A
|
||||
/-- Constructive asymptotic operators. -/
|
||||
φc : S.𝓯 → Lorentz.Contr 3 → A
|
||||
/-- Distructive asymptotic operators. -/
|
||||
φd : S.𝓯 → Lorentz.Contr 3 → A
|
||||
ψc_ψd : ∀ i x, ψc i x + ψd i x = ψ i x
|
||||
/- Self comutators. -/
|
||||
ψc_comm_ψc : ∀ i j x y, ψc i x * ψc j y + (S.commFactor i j) • ψc j y * ψc i x = 0
|
||||
ψd_comm_ψd : ∀ i j x y, ψd i x * ψd j y + (S.commFactor i j) • ψd j y * ψd i x = 0
|
||||
φc_comm_φc : ∀ i j x y, φc i x * φc j y + (S.commFactor i j) • φc j y * φc i x = 0
|
||||
φd_comm_φd : ∀ i j x y, φd i x * φd j y + (S.commFactor i j) • φd j y * φd i x = 0
|
||||
/- Cross comutators. -/
|
||||
|
||||
informal_definition WickMonomial where
|
||||
math :≈ "The type of elements of the Wick algebra which is a product of fields."
|
||||
deps :≈ [``WickAlgebra]
|
||||
namespace WickAlgebra
|
||||
|
||||
namespace WickMonomial
|
||||
variable {S : Species} (𝓞 : WickAlgebra S)
|
||||
|
||||
informal_definition toWickAlgebra where
|
||||
math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
|
||||
returns the product of the fields in the monomial."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
/-- The type `A` of a Wick algebra is a semi-ring. -/
|
||||
instance : Semiring 𝓞.A := 𝓞.A_semiring
|
||||
|
||||
/-- The type `A` of a Wick algebra is an algebra. -/
|
||||
instance : Algebra ℂ 𝓞.A := 𝓞.A_algebra
|
||||
|
||||
end WickAlgebra
|
||||
|
||||
namespace Species
|
||||
|
||||
variable (S : Species)
|
||||
|
||||
note r"
|
||||
<h2>Order</h2>
|
||||
"
|
||||
Suppose we have a type $I$ with a order $r$, a map $g : I \to \mathbb{Z}/2$,
|
||||
and a map $f : I \to A$ such that $f(i) \in A_{g(i)}$.
|
||||
Consider the free algebra generated by $I$, which we will denote $A_I$.
|
||||
The map $f$ can be extended to a map $T_r : A_I \to A$ such that
|
||||
a monomial $i_1 \cdots i_n$ gets mapped to $(-1)^{K(σ)}f(i_{σ(1)})...f(i_{σ(n)})$ where $σ$ is the
|
||||
permutation oredering the $i$'s by $r$ (preserving the order of terms which are equal under $r$),
|
||||
and $K(σ)$ is the Koszul sign factor. (see e.g. PSE:24157)
|
||||
<br><br>
|
||||
There are two types $I$ we are intrested in.
|
||||
"
|
||||
|
||||
informal_definition_note timeOrder where
|
||||
math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
|
||||
returns the monomial with the fields time ordered, with the correct sign
|
||||
determined by the Koszul sign factor.
|
||||
/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
|
||||
for each fermion-fermion cross. -/
|
||||
def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
|
||||
List I → ℂ
|
||||
| [] => 1
|
||||
| b :: l => if r a b then 1 else
|
||||
if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
|
||||
|
||||
If two fields have the same time, then their order is preserved e.g.
|
||||
T(ψ₁(t)ψ₂(t)) = ψ₁(t)ψ₂(t)
|
||||
and
|
||||
T(ψ₂(t)ψ₁(t)) = ψ₂(t)ψ₁(t).
|
||||
This allows us to make sense of the construction in e.g.
|
||||
https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf
|
||||
which permits normal-ordering within time-ordering.
|
||||
"
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
|
||||
lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
|
||||
(ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| b :: l => by
|
||||
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
|
||||
intro _
|
||||
simp only [ha, Fin.isValue, zero_ne_one, false_and, ↓reduceIte]
|
||||
exact koszulSignInsert_boson r q a ha l
|
||||
|
||||
informal_definition_note normalOrder where
|
||||
math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
|
||||
returns the element in `WickAlgebra` defined as follows
|
||||
- The ψd fields are move to the right.
|
||||
- The ψc fields are moved to the left.
|
||||
- Othewise the order of the fields is preserved."
|
||||
ref :≈ "https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf"
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
|
||||
a list of based on `r`. -/
|
||||
def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
|
||||
List I → ℂ
|
||||
| [] => 1
|
||||
| a :: l => koszulSignInsert r q a l * koszulSign r q l
|
||||
|
||||
end WickMonomial
|
||||
@[simp]
|
||||
lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
|
||||
change koszulSign r q [i] = 1
|
||||
simp only [koszulSign, mul_one]
|
||||
rfl
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra ℂ (FreeMonoid I)` by `r` giving it
|
||||
a signed dependent on `q`. -/
|
||||
def koszulOrderMonoidAlgebra {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
|
||||
MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
|
||||
Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid I)) ℂ (List I)
|
||||
(fun i => Finsupp.lsingle (R := ℂ) (List.insertionSort r i) (koszulSign r q i))
|
||||
|
||||
@[simp]
|
||||
lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [DecidableRel r]
|
||||
(q : I → Fin 2) (i : List I) :
|
||||
koszulOrderMonoidAlgebra r q (MonoidAlgebra.of ℂ (FreeMonoid I) i) =
|
||||
(koszulSign r q i) • (MonoidAlgebra.of ℂ (FreeMonoid I) (List.insertionSort r i)) := by
|
||||
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
|
||||
MonoidAlgebra.smul_single', mul_one]
|
||||
rw [MonoidAlgebra.ext_iff]
|
||||
intro x
|
||||
erw [Finsupp.lift_apply]
|
||||
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
|
||||
one_mul]
|
||||
|
||||
@[simp]
|
||||
lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(l : FreeMonoid I) (x : ℂ) :
|
||||
koszulOrderMonoidAlgebra r q (MonoidAlgebra.single l x)
|
||||
= (koszulSign r q l) • (MonoidAlgebra.single (List.insertionSort r l) x) := by
|
||||
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
|
||||
rw [MonoidAlgebra.ext_iff]
|
||||
intro x'
|
||||
erw [Finsupp.lift_apply]
|
||||
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
|
||||
one_mul, MonoidAlgebra.single]
|
||||
congr 2
|
||||
rw [NonUnitalNormedCommRing.mul_comm]
|
||||
|
||||
/-- Given a relation `r` on `I` sorts elements of `FreeAlgebra ℂ I` by `r` giving it
|
||||
a signed dependent on `q`. -/
|
||||
def koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
|
||||
FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
|
||||
∘ₗ koszulOrderMonoidAlgebra r q
|
||||
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
|
||||
|
||||
lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i : I) :
|
||||
koszulOrder r q (FreeAlgebra.ι ℂ i) = FreeAlgebra.ι ℂ i := by
|
||||
simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
|
||||
koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, LinearMap.coe_comp, Function.comp_apply,
|
||||
AlgEquiv.toLinearMap_apply]
|
||||
rw [AlgEquiv.symm_apply_eq]
|
||||
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
|
||||
AlgEquiv.ofAlgHom_apply, FreeAlgebra.lift_ι_apply]
|
||||
rw [@MonoidAlgebra.ext_iff]
|
||||
intro x
|
||||
erw [Finsupp.lift_apply]
|
||||
simp only [MonoidAlgebra.smul_single', List.insertionSort, List.orderedInsert,
|
||||
koszulSign_freeMonoid_of, mul_one, Finsupp.single_zero, Finsupp.sum_single_index]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(l : FreeMonoid I) :
|
||||
koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
|
||||
= FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
|
||||
(MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
|
||||
simp [koszulOrder]
|
||||
|
||||
end
|
||||
|
||||
/-- The indexing set of constructive and destructive position based operators. -/
|
||||
def ConstDestAlgebra.index : Type := Fin 2 × S.𝓯 × SpaceTime
|
||||
|
||||
/-- The free algebra generated by constructive and destructive parts of fields position-based
|
||||
fields. -/
|
||||
abbrev ConstDestAlgebra := FreeAlgebra ℂ (ConstDestAlgebra.index S)
|
||||
|
||||
/-- The indexing set of position based field operators. -/
|
||||
def FieldAlgebra.index : Type := S.𝓯 × SpaceTime
|
||||
|
||||
/-- The free algebra generated by fields. -/
|
||||
abbrev FieldAlgebra := FreeAlgebra ℂ (FieldAlgebra.index S)
|
||||
|
||||
namespace ConstDestAlgebra
|
||||
|
||||
variable {S} (𝓞 : WickAlgebra S)
|
||||
|
||||
/-- The inclusion of constructive and destructive fields into the full operator algebra. -/
|
||||
def toWickAlgebra : ConstDestAlgebra S →ₐ[ℂ] 𝓞.A :=
|
||||
FreeAlgebra.lift ℂ (fun (i, f, x) =>
|
||||
match i with
|
||||
| 0 => 𝓞.ψc f x
|
||||
| 1 => 𝓞.ψd f x)
|
||||
|
||||
@[simp]
|
||||
lemma toWickAlgebra_ι_zero (x : S.𝓯 × SpaceTime) :
|
||||
toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ (0, x)) = 𝓞.ψc x.1 x.2 := by
|
||||
simp [toWickAlgebra]
|
||||
|
||||
@[simp]
|
||||
lemma toWickAlgebra_ι_one (x : S.𝓯 × SpaceTime) :
|
||||
toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ (1, x)) = 𝓞.ψd x.1 x.2 := by
|
||||
simp [toWickAlgebra]
|
||||
|
||||
/-- The time ordering relation on constructive and destructive operators. -/
|
||||
def timeOrderRel : index S → index S → Prop := fun x y => x.2.2 0 ≤ y.2.2 0
|
||||
|
||||
/-- The normal ordering relation on constructive and destructive operators. -/
|
||||
def normalOrderRel : index S → index S → Prop := fun x y => x.1 ≤ y.1
|
||||
|
||||
/-- The normal ordering relation of constructive and destructive operators is decidable. -/
|
||||
instance : DecidableRel (@normalOrderRel S) := fun a b => a.1.decLe b.1
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- The time ordering relation of constructive and destructive operators is decidable. -/
|
||||
instance : DecidableRel (@timeOrderRel S) :=
|
||||
fun a b => Real.decidableLE (a.2.2 0) (b.2.2 0)
|
||||
|
||||
/-- The time ordering of constructive and destructive operators. -/
|
||||
def timeOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
|
||||
koszulOrder timeOrderRel q
|
||||
|
||||
/-- The normal ordering of constructive and destructive operators. -/
|
||||
def normalOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
|
||||
koszulOrder normalOrderRel q
|
||||
|
||||
/-- Contraction of constructive and destructive operators, defined as their time
|
||||
ordering minus their normal ordering. -/
|
||||
def contract (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[ℂ] S.ConstDestAlgebra :=
|
||||
timeOrder q - normalOrder q
|
||||
|
||||
end
|
||||
|
||||
end ConstDestAlgebra
|
||||
|
||||
namespace FieldAlgebra
|
||||
|
||||
variable {S} (𝓞 : WickAlgebra S)
|
||||
|
||||
/-- The inclusion fo the field algebra into the operator algebra. -/
|
||||
def toWickAlgebra : FieldAlgebra S →ₐ[ℂ] 𝓞.A :=
|
||||
FreeAlgebra.lift ℂ (fun i => 𝓞.ψ i.1 i.2)
|
||||
|
||||
@[simp]
|
||||
lemma toWickAlgebra_ι (i : index S) : toWickAlgebra 𝓞 (FreeAlgebra.ι ℂ i) = 𝓞.ψ i.1 i.2 := by
|
||||
simp [toWickAlgebra]
|
||||
|
||||
/-- The map from the field algebra to the algebra of constructive and destructive fields. -/
|
||||
def toConstDestAlgebra : FieldAlgebra S →ₐ[ℂ] ConstDestAlgebra S :=
|
||||
FreeAlgebra.lift ℂ (fun i => FreeAlgebra.ι ℂ (0, i) + FreeAlgebra.ι ℂ (1, i))
|
||||
|
||||
@[simp]
|
||||
lemma toConstDestAlgebra_ι (i : index S) : toConstDestAlgebra (FreeAlgebra.ι ℂ i) =
|
||||
FreeAlgebra.ι ℂ (0, i) + FreeAlgebra.ι ℂ (1, i) := by
|
||||
simp [toConstDestAlgebra]
|
||||
|
||||
/-- Given a list of fields and a map `f` tell us which field is constructive and
|
||||
which is destructive, a list of constructive and destructive fields. -/
|
||||
def listToConstDestList : (l : List (index S)) →
|
||||
(f : Fin l.length → Fin 2) → List (ConstDestAlgebra.index S)
|
||||
| [], _ => []
|
||||
| i :: l, f =>
|
||||
(f ⟨0, Nat.zero_lt_succ l.length⟩, i.1, i.2) :: listToConstDestList l (f ∘ Fin.succ)
|
||||
|
||||
lemma listToConstDestList_length (l : List (index S)) (f : Fin l.length → Fin 2) :
|
||||
(listToConstDestList l f).length = l.length := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons i l ih =>
|
||||
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Prod.mk.eta, add_left_inj]
|
||||
rw [ih]
|
||||
|
||||
lemma toConstDestAlgebra_single (x : ℂ) : (l : FreeMonoid (index S)) →
|
||||
toConstDestAlgebra (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
|
||||
= ∑ (f : Fin l.length → Fin 2), FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
|
||||
(MonoidAlgebra.single (listToConstDestList l f) x)
|
||||
| [] => by
|
||||
simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_nil, Finset.univ_unique,
|
||||
listToConstDestList, Finset.sum_const, Finset.card_singleton, one_smul]
|
||||
trans x • 1
|
||||
· trans toConstDestAlgebra (x • 1)
|
||||
· congr
|
||||
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
|
||||
FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
|
||||
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rfl
|
||||
· simp only [toConstDestAlgebra, Fin.isValue, map_smul, map_one]
|
||||
· simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, FreeMonoid.lift,
|
||||
FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk, AlgEquiv.ofAlgHom_symm_apply,
|
||||
MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rfl
|
||||
| i :: l => by
|
||||
simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_cons, listToConstDestList,
|
||||
Fin.zero_eta, Prod.mk.eta]
|
||||
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single (i :: l) x) =
|
||||
(FreeAlgebra.ι ℂ i) *
|
||||
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single l x)) := by
|
||||
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
|
||||
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
|
||||
congr
|
||||
simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
|
||||
MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
change List.foldl (fun x1 x2 => x1 * x2) (FreeAlgebra.ι ℂ i) (List.map (FreeAlgebra.ι ℂ) l) = _
|
||||
match l with
|
||||
| [] =>
|
||||
simp only [List.map_nil, List.foldl_nil, ne_eq, FreeAlgebra.ι_ne_zero, not_false_eq_true,
|
||||
left_eq_mul₀]
|
||||
rfl
|
||||
| x :: l =>
|
||||
simp only [List.map_cons, List.foldl_cons]
|
||||
change _ = FreeAlgebra.ι ℂ i * List.foldl (fun x1 x2 => x1 * x2) _ _
|
||||
rw [List.foldl_assoc]
|
||||
rw [h1]
|
||||
rw [map_mul]
|
||||
trans ∑ f : Fin (l.length + 1) → Fin 2, (FreeAlgebra.ι ℂ ((f 0, i)) : ConstDestAlgebra S) *
|
||||
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
|
||||
(Finsupp.single (listToConstDestList l (f ∘ Fin.succ)) x) : ConstDestAlgebra S)
|
||||
· rw [← (Fin.consEquiv (n := l.length) (fun _ => Fin 2)).sum_comp
|
||||
(α := FreeAlgebra ℂ (ConstDestAlgebra.index S))]
|
||||
erw [Finset.sum_product]
|
||||
simp only [toConstDestAlgebra_ι, Fin.isValue, Fin.consEquiv_apply, Fin.cons_zero,
|
||||
Fin.sum_univ_two]
|
||||
rw [← Finset.mul_sum, ← Finset.mul_sum]
|
||||
erw [← toConstDestAlgebra_single]
|
||||
rw [add_mul]
|
||||
· congr
|
||||
funext f
|
||||
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
|
||||
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
|
||||
congr
|
||||
simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
|
||||
MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
match l with
|
||||
| [] =>
|
||||
simp only [listToConstDestList]
|
||||
change FreeAlgebra.ι ℂ (f 0, i) * 1 = _
|
||||
simp only [mul_one]
|
||||
rfl
|
||||
| x :: l =>
|
||||
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Function.comp_apply,
|
||||
Fin.succ_zero_eq_one, Prod.mk.eta]
|
||||
change FreeAlgebra.ι ℂ (f 0, i) * List.foldl _ _ _ = List.foldl _ _ _
|
||||
simp only [List.map_cons, List.foldl_cons]
|
||||
haveI : Std.Associative fun
|
||||
(x1 x2 : FreeAlgebra ℂ (ConstDestAlgebra.index S)) => x1 * x2 := by
|
||||
exact Semigroup.to_isAssociative
|
||||
refine Eq.symm List.foldl_assoc
|
||||
|
||||
lemma toWickAlgebra_factor_toConstDestAlgebra :
|
||||
toWickAlgebra 𝓞 = (ConstDestAlgebra.toWickAlgebra 𝓞).comp toConstDestAlgebra := by
|
||||
refine FreeAlgebra.hom_ext ?_
|
||||
funext i
|
||||
simp only [Function.comp_apply, toWickAlgebra_ι, ConstDestAlgebra.toWickAlgebra, AlgHom.coe_comp,
|
||||
toConstDestAlgebra_ι, Fin.isValue, map_add, FreeAlgebra.lift_ι_apply]
|
||||
split
|
||||
rename_i x i_1 f x_1 heq
|
||||
simp_all only [Fin.isValue, Prod.mk.injEq]
|
||||
obtain ⟨left, right⟩ := heq
|
||||
subst left right
|
||||
exact Eq.symm (𝓞.ψc_ψd f x_1)
|
||||
|
||||
/-- The time ordering relation in the field algebra. -/
|
||||
def timeOrderRel : index S → index S → Prop := fun x y => x.2 0 ≤ y.2 0
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- The time ordering relation in the field algebra is decidable. -/
|
||||
instance : DecidableRel (@timeOrderRel S) :=
|
||||
fun a b => Real.decidableLE (a.2 0) (b.2 0)
|
||||
|
||||
/-- The time ordering in the field algebra. -/
|
||||
def timeOrder (q : index S → Fin 2) : S.FieldAlgebra →ₗ[ℂ] S.FieldAlgebra :=
|
||||
koszulOrder timeOrderRel q
|
||||
|
||||
/-
|
||||
lemma timeOrder_comm_toConstDestAlgebra (q : index S → Fin 2)
|
||||
(q' : ConstDestAlgebra.index S → Fin 2) :
|
||||
(ConstDestAlgebra.timeOrder q').comp toConstDestAlgebra.toLinearMap =
|
||||
toConstDestAlgebra.toLinearMap.comp (timeOrder q) := by
|
||||
let e : S.FieldAlgebra ≃ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid (index S)) :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
|
||||
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
|
||||
apply MonoidAlgebra.lhom_ext'
|
||||
intro l
|
||||
apply LinearMap.ext
|
||||
intro x
|
||||
simp [e, toConstDestAlgebra_single, timeOrder]
|
||||
simp [FreeMonoid.length, List.length_insertionSort]
|
||||
let ew := Equiv.piCongrLeft' (fun a => Fin 2)
|
||||
(Fin.castOrderIso (List.length_insertionSort timeOrderRel l).symm).toEquiv
|
||||
rw [← ew.sum_comp
|
||||
(α := FreeAlgebra ℂ (ConstDestAlgebra.index S)) ]
|
||||
congr
|
||||
funext f
|
||||
simp [ConstDestAlgebra.timeOrder]
|
||||
congr 1
|
||||
·
|
||||
· sorry
|
||||
-/
|
||||
|
||||
end
|
||||
|
||||
end FieldAlgebra
|
||||
|
||||
end Species
|
||||
|
||||
informal_definition asymptoicContract where
|
||||
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator [φd(i), ψ(j)]."
|
||||
|
|
@ -137,41 +472,34 @@ informal_definition asymptoicContractAsymptotic where
|
|||
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator
|
||||
[φd(i), φc(j)]."
|
||||
|
||||
informal_definition contraction where
|
||||
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the element of WickAlgebra
|
||||
defined by subtracting the normal ordering of `ψ i ψ j` from the time-ordering of
|
||||
`ψ i ψ j`."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
|
||||
informal_lemma contraction_in_center where
|
||||
math :≈ "The contraction of two fields is in the center of the algebra."
|
||||
deps :≈ [``WickAlgebra, ``contraction]
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
informal_lemma contraction_non_dual_is_zero where
|
||||
math :≈ "The contraction of two fields is zero if the fields are not dual to each other."
|
||||
deps :≈ [``WickAlgebra, ``contraction]
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
informal_lemma timeOrder_single where
|
||||
math :≈ "The time ordering of a single field is the normal ordering of that field."
|
||||
proof :≈ "Follows from the definitions."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial.timeOrder, ``WickMonomial.normalOrder]
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
informal_lemma timeOrder_pair where
|
||||
math :≈ "The time ordering of two fields is the normal ordering of the fields plus the
|
||||
contraction of the fields."
|
||||
proof :≈ "Follows from the definition of contraction."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial.timeOrder, ``WickMonomial.normalOrder,
|
||||
``contraction]
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
informal_definition WickMap where
|
||||
math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
|
||||
`vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
|
||||
physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
|
||||
the necessary properties for lots of theorems to hold."
|
||||
deps :≈ [``WickAlgebra, ``WickMonomial]
|
||||
deps :≈ [``WickAlgebra]
|
||||
|
||||
informal_lemma normalOrder_wickMap where
|
||||
math :≈ "Any normal ordering maps to zero under a Wick map."
|
||||
deps :≈ [``WickMap, ``WickMonomial.normalOrder]
|
||||
deps :≈ [``WickMap]
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -20,6 +20,10 @@ import HepLean.Meta.Notes.Basic
|
|||
|
||||
namespace Wick
|
||||
variable {S : Species}
|
||||
|
||||
note r"
|
||||
<h2>Wick Contractions</h2>
|
||||
"
|
||||
/-- A Wick contraction for a Wick string is a series of pairs `i` and `j` of indices
|
||||
to be contracted, subject to ordering and subject to the condition that they can
|
||||
be contracted. -/
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import Mathlib.Logic.Function.Basic
|
||||
import HepLean.Meta.Informal.Basic
|
||||
import HepLean.Meta.Notes.Basic
|
||||
import HepLean.Lorentz.RealVector.Basic
|
||||
/-!
|
||||
|
||||
# Wick Species
|
||||
|
|
@ -56,11 +57,18 @@ structure Species where
|
|||
𝓘 : Type
|
||||
/-- The fields associated to each interaction term. -/
|
||||
𝓘Fields : 𝓘 → Σ n, Fin n → 𝓯
|
||||
/-- The map taking a field to `0` if it is a boson and `1` if it is a fermion.
|
||||
Note that this definition suffers a similar problem to Boolean Blindness. -/
|
||||
grade : 𝓯 → Fin 2
|
||||
|
||||
namespace Species
|
||||
|
||||
variable (S : Species)
|
||||
|
||||
/-- When commuting two fields `f` and `g`, in the super commuator which is sematically
|
||||
`[f, g] = f g + c * g f`, this is `c`. -/
|
||||
def commFactor (f g : S.𝓯) : ℂ := - (- 1) ^ (S.grade f * S.grade g : ℕ)
|
||||
|
||||
informal_definition 𝓕 where
|
||||
math :≈ "The orbits of the involution `ξ`.
|
||||
May have to define a multiplicative action of ℤ₂ on `𝓯`, and
|
||||
|
|
|
|||
|
|
@ -13,8 +13,11 @@ Wick's theorem is related to a result in probability theory called Isserlis' the
|
|||
-/
|
||||
|
||||
namespace Wick
|
||||
note r"
|
||||
<h2>Wick's theorem</h2>
|
||||
"
|
||||
|
||||
informal_lemma wicks_theorem where
|
||||
informal_lemma_note wicks_theorem where
|
||||
math :≈ "Wick's theorem for fields which are not normally ordered."
|
||||
|
||||
informal_lemma wicks_theorem_normal_order where
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue