diff --git a/Physlib/Mathematics/ConjModule.lean b/Physlib/Mathematics/ConjModule.lean index 3b2ce7039..0e1102274 100644 --- a/Physlib/Mathematics/ConjModule.lean +++ b/Physlib/Mathematics/ConjModule.lean @@ -9,7 +9,7 @@ public import Mathlib.Algebra.Module.Equiv.Defs public import Mathlib.Algebra.Star.Module public import Mathlib.LinearAlgebra.Basis.Defs public import Mathlib.Tactic.Ring - +public import Mathlib.RepresentationTheory.Basic /-! # The conjugate module @@ -53,6 +53,19 @@ conjugation ring endomorphism `starRingEnd k`. -/ instance instModule : Module k (ConjModule M) := Module.compHom M (starRingEnd k) +variable {A : Type*} [Ring A] + +instance : Ring (ConjModule A) := + let i1 : AddCommGroup (ConjModule A) := inferInstanceAs (AddCommGroup (ConjModule A)) + let i2 : Ring A := inferInstanceAs (Ring A) + { i1, i2 with } + +/-- The conjugate module of a `k`-algebra is a `k`-algebra: the same ring, with scalars +acting through `star`. -/ +instance instAlgebra [Algebra k A] : Algebra k (ConjModule A) := + Algebra.ofModule (fun r x y => smul_mul_assoc (β := A) (star r) x y) + (fun r x y => mul_smul_comm (β := A) (star r) x y) + end ConjModule /-- The canonical conjugate-linear equivalence `M ≃ₛₗ[starRingEnd k] ConjModule M`, the identity on @@ -65,6 +78,26 @@ def conjEquiv : M ≃ₛₗ[starRingEnd k] ConjModule M where left_inv _ := rfl right_inv _ := rfl +/-- The canonical conjugate-linear equivalence between the dual of a module `M` and + the dual of its conjugate. -/ +def conjDualEquiv : Module.Dual k M ≃ₛₗ[starRingEnd k] Module.Dual k (ConjModule M) where + toFun f := (starRingEnd k).toSemilinearMap.comp + (f.comp (conjEquiv (k := k) (M := M)).symm.toLinearMap) + invFun f := (starRingEnd k).toSemilinearMap.comp + (f.comp (conjEquiv (k := k) (M := M)).toLinearMap) + map_add' f g := by + ext x + simp + map_smul' r f := by + ext x + simp + left_inv f := by + ext x + simp + right_inv f := by + ext x + simp + namespace ConjModule /-- Conjugating twice returns the original module: the `k`-linear isomorphism @@ -89,16 +122,16 @@ noncomputable def starFinsupp : (ι →₀ k) ≃ₛₗ[starRingEnd k] (ι → /-- A basis of `M` transported to a basis of `ConjModule M`: the same basis vectors, with coordinates conjugated (`(Basis.conj b).repr v = star ∘ b.repr v`). -/ -noncomputable def _root_.Basis.conj (b : Basis ι k M) : Basis ι k (ConjModule M) := +noncomputable def _root_.Module.Basis.conj (b : Basis ι k M) : Basis ι k (ConjModule M) := Basis.ofRepr (((conjEquiv (k := k) (M := M)).symm.trans b.repr).trans starFinsupp) /-- Coordinates in `Basis.conj b` are the `star` of the coordinates in `b`. -/ -@[simp] lemma _root_.Basis.conj_repr_apply (b : Basis ι k M) (v : ConjModule M) (i : ι) : +@[simp] lemma _root_.Module.Basis.conj_repr_apply (b : Basis ι k M) (v : ConjModule M) (i : ι) : (Basis.conj b).repr v i = star (b.repr ((conjEquiv (k := k) (M := M)).symm v) i) := rfl /-- The basis vectors of `Basis.conj b` are those of `b`, viewed through `conjEquiv`. -/ -@[simp] lemma _root_.Basis.conj_apply (b : Basis ι k M) (i : ι) : +@[simp] lemma _root_.Module.Basis.conj_apply (b : Basis ι k M) (i : ι) : Basis.conj b i = conjEquiv (k := k) (M := M) (b i) := by apply (Basis.conj b).repr.injective ext j @@ -106,6 +139,29 @@ noncomputable def _root_.Basis.conj (b : Basis ι k M) : Basis ι k (ConjModule · subst h; simp [Basis.conj_repr_apply] · simp [Basis.conj_repr_apply, Finsupp.single_eq_of_ne, h] +/-! + +## The conjugate of a representation + +-/ + +/-- The conjugate of a representation `ρ` of `G` on `M`: the same maps `ρ g`, acting on +`ConjModule M` through `conjEquiv`. -/ +def _root_.Representation.conj {G} [Group G] (ρ : Representation k G M) : + Representation k G (ConjModule M) where + toFun g := { + toFun := conjEquiv (k := k) (M := M) ∘ ρ g ∘ (conjEquiv (k := k) (M := M)).symm + map_add' x y := (ρ g).map_add x y + map_smul' a m := (ρ g).map_smul (star a) m } + map_one' := LinearMap.ext fun _ => + congrArg (conjEquiv (k := k)) (LinearMap.congr_fun (map_one ρ) _) + map_mul' g h := LinearMap.ext fun _ => + congrArg (conjEquiv (k := k)) (LinearMap.congr_fun (map_mul ρ g h) _) + +lemma _root_.Representation.conj_apply {G} [Group G] (ρ : Representation k G M) (g : G) + (m : ConjModule M) : + ρ.conj g m = conjEquiv (k := k) (M := M) (ρ g ((conjEquiv (k := k) (M := M)).symm m)) := rfl + end ConjModule end diff --git a/Physlib/Mathematics/MultisetsOfMassDim.lean b/Physlib/Mathematics/MultisetsOfMassDim.lean new file mode 100644 index 000000000..993d96854 --- /dev/null +++ b/Physlib/Mathematics/MultisetsOfMassDim.lean @@ -0,0 +1,217 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith, Nathaneal Sajan, Jinzheng Li +-/ +module + +public import Mathlib.Data.Finset.Sym +public import Mathlib.Data.Finset.Lattice.Fold +public import Mathlib.Data.Rat.Floor +public import Mathlib.Algebra.Order.BigOperators.Group.Multiset +/-! + +# Computable enumeration of multisets of a given mass dimension + +## i. Overview + +Given a finite type `F` of field specifications, a map `dim : F → ℚ` assigning to each field +its mass dimension (assumed positive), and a target `m : ℚ`, this file constructs, in a +computable way, the `Finset (Multiset F)` of all multisets of fields whose overall mass +dimension is `m`. This corresponds to the possible operators (terms) of mass dimension `m` +in an EFT Lagrangian built from the fields in `F` (excluding derivatives). + +The construction proceeds by noting that if `d` is the minimal mass dimension of a field, +then a multiset of mass dimension `m` has at most `⌊m / d⌋₊` elements. We therefore +enumerate all multisets of cardinality at most this bound using `Finset.sym`, and filter +by the mass-dimension condition. + +Since the construction is computable it can be used with `#eval`. However, rational +arithmetic does not reduce in the kernel, so `multisetsOfMassDim` can not directly be +used with `decide`. For this reason we also provide a version `multisetsOfMassDimNat` +with natural-number valued mass dimensions (corresponding to clearing denominators, +e.g. working in units of half mass dimensions so that a Weyl fermion has scaled +dimension `3`), which is `decide`-friendly. The lemma `multisetsOfMassDim_eq_natCast` +allows one to rewrite the former into the latter before calling `decide`. + +## Key results + +- `multisetsOfCard` : the finset of all multisets over `F` of a given cardinality. +- `multisetsOfMassDim` : the finset of all multisets over `F` of a given mass dimension. +- `mem_multisetsOfMassDim_iff` : the defining property + `s ∈ multisetsOfMassDim dim m ↔ (s.map dim).sum = m`, valid whenever `dim` is positive. +- `multisetsOfMassDimNat`, `mem_multisetsOfMassDimNat_iff` : the analogous construction + for natural-number valued (scaled) mass dimensions, usable with `decide`. +- `multisetsOfMassDim_eq_natCast` : the two constructions agree after clearing + denominators. + +-/ + +@[expose] public section + +variable {F : Type*} [Fintype F] + +/-! + +## A. Multisets of a given cardinality + +-/ + +/-- The finset of all multisets over a finite type `F` with exactly `n` elements. -/ +def multisetsOfCard (F : Type*) [Fintype F] [DecidableEq F] (n : ℕ) : + Finset (Multiset F) := + (Finset.univ.sym n).image Sym.toMultiset + +@[simp] +lemma mem_multisetsOfCard [DecidableEq F] {n : ℕ} {s : Multiset F} : + s ∈ multisetsOfCard F n ↔ Multiset.card s = n := by + constructor + · intro h + obtain ⟨x, -, rfl⟩ := Finset.mem_image.mp h + exact x.2 + · rintro rfl + exact Finset.mem_image.mpr + ⟨⟨s, rfl⟩, Finset.mem_sym_iff.mpr fun a _ => Finset.mem_univ a, rfl⟩ + +/-! + +## B. The bound on the cardinality + +-/ + +/-- The sum of `dim` over a multiset is at least the cardinality times the minimal + value of `dim`. Shared bound underlying `card_le_massDimCardBound` and + `card_le_massDimCardBoundNat`. -/ +lemma card_nsmul_inf'_le_sum_map {M : Type*} [AddCommMonoid M] [LinearOrder M] + [AddLeftMono M] (huniv : (Finset.univ : Finset F).Nonempty) (dim : F → M) + (s : Multiset F) : + Multiset.card s • Finset.univ.inf' huniv dim ≤ (s.map dim).sum := by + have h1 : Multiset.card (s.map dim) • Finset.univ.inf' huniv dim ≤ (s.map dim).sum := by + refine Multiset.card_nsmul_le_sum fun x hx => ?_ + obtain ⟨f, -, rfl⟩ := Multiset.mem_map.mp hx + exact Finset.inf'_le dim (Finset.mem_univ f) + simpa using h1 + +/-- An upper bound on the number of fields in a multiset of overall mass dimension `m`: + `⌊m / d⌋₊` where `d` is the minimal mass dimension of a field. Equal to `0` when + `F` is empty. -/ +def massDimCardBound (dim : F → ℚ) (m : ℚ) : ℕ := + if h : (Finset.univ : Finset F).Nonempty then ⌊m / Finset.univ.inf' h dim⌋₊ else 0 + +private lemma card_le_massDimCardBound {dim : F → ℚ} (hdim : ∀ f, 0 < dim f) {m : ℚ} + {s : Multiset F} (hs : (s.map dim).sum = m) : + Multiset.card s ≤ massDimCardBound dim m := by + rcases eq_or_ne s 0 with rfl | hne + · simp + obtain ⟨f0, -⟩ := Multiset.exists_mem_of_ne_zero hne + have huniv : (Finset.univ : Finset F).Nonempty := ⟨f0, Finset.mem_univ f0⟩ + rw [massDimCardBound, dif_pos huniv] + have hdpos : 0 < Finset.univ.inf' huniv dim := + (Finset.lt_inf'_iff huniv).mpr fun i _ => hdim i + have hle := hs ▸ card_nsmul_inf'_le_sum_map huniv dim s + refine Nat.le_floor ?_ + rw [le_div_iff₀ hdpos] + simpa [nsmul_eq_mul] using hle + +/-! + +## C. Multisets of a given mass dimension + +-/ + +/-- The finset of all multisets over a finite type `F` whose overall mass dimension, + as measured by `dim : F → ℚ`, is `m`. The defining property, valid when `dim` is + positive, is `mem_multisetsOfMassDim_iff`. -/ +def multisetsOfMassDim [DecidableEq F] (dim : F → ℚ) (m : ℚ) : Finset (Multiset F) := + ((Finset.range (massDimCardBound dim m + 1)).biUnion (multisetsOfCard F)).filter + fun s => (s.map dim).sum = m + +lemma mem_multisetsOfMassDim_iff [DecidableEq F] {dim : F → ℚ} (hdim : ∀ f, 0 < dim f) {m : ℚ} + {s : Multiset F} : + s ∈ multisetsOfMassDim dim m ↔ (s.map dim).sum = m := by + constructor + · exact fun h => (Finset.mem_filter.mp h).2 + · intro h + refine Finset.mem_filter.mpr ⟨Finset.mem_biUnion.mpr ⟨Multiset.card s, ?_, by simp⟩, h⟩ + exact Finset.mem_range.mpr (Nat.lt_succ_of_le (card_le_massDimCardBound hdim h)) + +/-! + +## D. Multisets of a given scaled (natural-number) mass dimension + +Rational arithmetic does not reduce in the kernel, so `multisetsOfMassDim` is usable +with `#eval` but not with `decide`. Clearing denominators in the mass dimensions +(e.g. working in units of half mass dimensions) reduces the problem to natural-number +valued dimensions, for which the analogous construction below is `decide`-friendly. + +-/ + +/-- An upper bound on the number of fields in a multiset of overall scaled mass + dimension `m`: `m / d` (natural-number division) where `d` is the minimal scaled + mass dimension of a field. Equal to `0` when `F` is empty. -/ +def massDimCardBoundNat (dim : F → ℕ) (m : ℕ) : ℕ := + if h : (Finset.univ : Finset F).Nonempty then m / Finset.univ.inf' h dim else 0 + +private lemma card_le_massDimCardBoundNat {dim : F → ℕ} (hdim : ∀ f, 0 < dim f) {m : ℕ} + {s : Multiset F} (hs : (s.map dim).sum = m) : + Multiset.card s ≤ massDimCardBoundNat dim m := by + rcases eq_or_ne s 0 with rfl | hne + · simp + obtain ⟨f0, -⟩ := Multiset.exists_mem_of_ne_zero hne + have huniv : (Finset.univ : Finset F).Nonempty := ⟨f0, Finset.mem_univ f0⟩ + rw [massDimCardBoundNat, dif_pos huniv] + have hdpos : 0 < Finset.univ.inf' huniv dim := + (Finset.lt_inf'_iff huniv).mpr fun i _ => hdim i + rw [Nat.le_div_iff_mul_le hdpos] + simpa [hs, smul_eq_mul] using card_nsmul_inf'_le_sum_map huniv dim s + +/-- The finset of all multisets over a finite type `F` whose overall scaled mass + dimension, as measured by `dim : F → ℕ`, is `m`. The defining property, valid when + `dim` is positive, is `mem_multisetsOfMassDimNat_iff`. Unlike `multisetsOfMassDim`, + this construction reduces in the kernel and can be used with `decide`. -/ +def multisetsOfMassDimNat [DecidableEq F] (dim : F → ℕ) (m : ℕ) : Finset (Multiset F) := + ((Finset.range (massDimCardBoundNat dim m + 1)).biUnion (multisetsOfCard F)).filter + fun s => (s.map dim).sum = m + +lemma mem_multisetsOfMassDimNat_iff [DecidableEq F] {dim : F → ℕ} (hdim : ∀ f, 0 < dim f) + {m : ℕ} {s : Multiset F} : + s ∈ multisetsOfMassDimNat dim m ↔ (s.map dim).sum = m := by + constructor + · exact fun h => (Finset.mem_filter.mp h).2 + · intro h + refine Finset.mem_filter.mpr ⟨Finset.mem_biUnion.mpr ⟨Multiset.card s, ?_, by simp⟩, h⟩ + exact Finset.mem_range.mpr (Nat.lt_succ_of_le (card_le_massDimCardBoundNat hdim h)) + +/-! + +## E. Relating the two constructions + +-/ + +/-- Clearing denominators: on multiplying all mass dimensions and the target mass + dimension by a common positive scale `N` rendering them all natural numbers, the + finset of multisets of a given mass dimension can be computed through + `multisetsOfMassDimNat`, and hence through `decide`. -/ +lemma multisetsOfMassDim_eq_natCast [DecidableEq F] {dim : F → ℚ} (hdim : ∀ f, 0 < dim f) + {dimN : F → ℕ} {N : ℕ} (hN : 0 < N) (hdimN : ∀ f, (dimN f : ℚ) = dim f * N) + {m : ℚ} {mN : ℕ} (hmN : (mN : ℚ) = m * N) : + multisetsOfMassDim dim m = multisetsOfMassDimNat dimN mN := by + have hNQ : (N : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr hN.ne' + have hdimNpos : ∀ f, 0 < dimN f := fun f => by + have h1 : (0 : ℚ) < (dimN f : ℚ) := by + rw [hdimN f] + exact mul_pos (hdim f) (by exact_mod_cast hN) + exact_mod_cast h1 + ext s + rw [mem_multisetsOfMassDim_iff hdim, mem_multisetsOfMassDimNat_iff hdimNpos] + have key : ((s.map dimN).sum : ℚ) = (s.map dim).sum * N := by + induction s using Multiset.induction with + | empty => simp + | cons a t ih => simp [hdimN, ih, add_mul] + constructor + · intro h + have h1 : ((s.map dimN).sum : ℚ) = (mN : ℚ) := by rw [key, h, hmN] + exact_mod_cast h1 + · intro h + have h1 : (s.map dim).sum * (N : ℚ) = m * N := by rw [← key, h, hmN] + exact mul_right_cancel₀ hNQ h1 diff --git a/Physlib/Particles/PureFermionic/EFTLagrangianExclDeriv.lean b/Physlib/Particles/PureFermionic/EFTLagrangianExclDeriv.lean new file mode 100644 index 000000000..b5c589cf4 --- /dev/null +++ b/Physlib/Particles/PureFermionic/EFTLagrangianExclDeriv.lean @@ -0,0 +1,1965 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith, Jinzheng Li, Nathaneal Sajan +-/ +module + +public import Physlib.Relativity.Fermions.Weyl.Metric +public import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation +public import Mathlib.LinearAlgebra.ExteriorAlgebra.Basis +public import Physlib.Mathematics.ConjModule +public import Physlib.Mathematics.MultisetsOfMassDim +public import Mathlib.RingTheory.GradedAlgebra.Basic +/-! + +# The effective potential for a left-handed Weyl fermion + +## i. Overview + +In this file our primary objective is to look at the potential +of a single left-handed Weyl fermion, correctly taking account +of the anti-commuting nature of the fermion. + +Two facts about the (effective) potential, which we take as a given, are that: +1. It is written in terms of the components of the left-handed Weyl fermion and its conjugate. + (For this effective potential, we do not consider derivatives.) +2. Within the potential the components anti-commute. +The first of these, tells us that we should be working with the dual of the left-handed Weyl fermion +and its conjugate (since the duals are the linear functionals which pick +out the components of the fermion). The second of these tells us that we should be working with an +exterior algebra. + +Thus, the type in which the potential lives is +`ExteriorAlgebra ℂ (Module.Dual ℂ LeftHandedWeyl × Module.Dual ℂ (ConjModule LeftHandedWeyl))`. +We call this type `EFTLagrangianExclDeriv` and define it and its properties in this file. +Note that `Module.Dual ℂ LeftHandedWeyl` is equivalent to `DualLeftHandedWeyl` and +`Module.Dual ℂ (ConjModule LeftHandedWeyl)` is equivalent to `DualRightHandedWeyl`, +so we could equivalently define the effective potential as +`ExteriorAlgebra ℂ (DualLeftHandedWeyl × DualRightHandedWeyl)`. We have done the +former here as it generalises to other cases. + +On `EFTLagrangianExclDeriv` we define a representation of the Lorentz group, and prove that that +if the potential is invariant under the Lorentz group it must be of the form +`c + m1 * ψ 0 * ψ 1 + m2 * barψ 0 * barψ 1 + λ * ψ 0 * ψ 1 * barψ 0 * barψ 1`, +which is true to all orders. + +## References + +- https://physics.stackexchange.com/questions/506709 describes the mass term of a + Weyl fermion. + +-/ + +@[expose] public section + +namespace Fermion +noncomputable section + +open Module Matrix +open MatrixGroups +open Complex +open TensorProduct +open CategoryTheory.MonoidalCategory + +/-! + +## A. The effective potential for Weyl fermions + +-/ + +/-- The type corresponding to the effective potential of a + left-handed Weyl fermion. -/ +abbrev EFTLagrangianExclDeriv : Type := ExteriorAlgebra ℂ + (Module.Dual ℂ LeftHandedWeyl × Module.Dual ℂ (ConjModule LeftHandedWeyl)) + +namespace EFTLagrangianExclDeriv + +/-! + +### A. The representation on the effective potential + +-/ + +/-- The representation of the Lorentz group (here `SL(2, ℂ)`) on `EFTLagrangianExclDeriv`. -/ +def rep : Representation ℂ SL(2, ℂ) EFTLagrangianExclDeriv where + toFun Λ := (ExteriorAlgebra.map ((LeftHandedWeyl.rep.dual Λ).prodMap + (LeftHandedWeyl.rep.conj.dual Λ))).toLinearMap + map_one' := by + simp only [map_one, End.one_eq_id, LinearMap.prodMap_id, ExteriorAlgebra.map_id, + AlgHom.toLinearMap_id] + map_mul' Λ1 Λ2 := by + simp only [map_mul, End.mul_eq_comp, ← LinearMap.prodMap_comp, ← ExteriorAlgebra.map_comp_map, + AlgHom.comp_toLinearMap] + +lemma rep_apply (Λ : SL(2, ℂ)) (V : EFTLagrangianExclDeriv) : + rep Λ V = ExteriorAlgebra.map ((LeftHandedWeyl.rep.dual Λ).prodMap + (LeftHandedWeyl.rep.conj.dual Λ)) V := rfl + +@[simp] +lemma rep_apply_one (Λ : SL(2, ℂ)) : rep Λ 1 = 1 := by + simp [rep_apply] + +lemma rep_mul (Λ : SL(2, ℂ)) (V W : EFTLagrangianExclDeriv) : + rep Λ (V * W) = rep Λ V * rep Λ W:= by + simp [rep] + + +/-! + +## The invariance condition on + +-/ + +/-- An effective potential is Lorentz invariant if it is stable under the + action of the Lorentz group. -/ +def IsInvariant (V : EFTLagrangianExclDeriv) : Prop := ∀ Λ, rep Λ V = V + +lemma IsInvariant.eq_iff {V : EFTLagrangianExclDeriv} : + IsInvariant V ↔ ∀ Λ, rep Λ V = V := by rfl + +@[simp] +lemma IsInvariant.zero : IsInvariant 0 := by + intro Λ + simp [rep] + +lemma IsInvariant.add {V W : EFTLagrangianExclDeriv} (hV : IsInvariant V) (hW : IsInvariant W) : + IsInvariant (V + W) := by + intro Λ + simp_all [IsInvariant.eq_iff] + +lemma IsInvariant.smul {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) (c : ℂ) : + IsInvariant (c • V) := by + intro Λ + simp_all [IsInvariant.eq_iff] + +lemma IsInvariant.mul {V W : EFTLagrangianExclDeriv} (hV : IsInvariant V) (hW : IsInvariant W) : + IsInvariant (V * W) := by + intro Λ + simp_all [IsInvariant.eq_iff, rep_mul] + +lemma IsInvariant.one : IsInvariant 1 := by + intro Λ + simp [rep] + +lemma IsInvariant.sum {ι : Type} (s : Finset ι) {f : ι → EFTLagrangianExclDeriv} + (h : ∀ i ∈ s, IsInvariant (f i)) : IsInvariant (∑ i ∈ s, f i) := by + intro Λ + simp_all [IsInvariant.eq_iff] + +end EFTLagrangianExclDeriv + +/-! + +### Diagonal elements of the Lorentz group + +The diagonal elements `diag (z, z⁻¹)` of `SL(2, ℂ)` scale each of the fields by a +factor, given below by `FieldSpecification.diagScale`. These elements are useful for +deriving selection rules on the effective potential. + +-/ + +TODO "Move the diagonal `SL(2, ℂ)` material `diagSL`, `diagSL_inv`, `diagSL_neg_one` + and `twoI` to `Physlib.Relativity.SL2C.Basic`, their canonical home, when the + effective-potential development is split up." + +/-- The diagonal element `diag (z, z⁻¹)` of `SL(2, ℂ)` associated with a unit `z : ℂˣ`. -/ +def diagSL (z : ℂˣ) : SL(2, ℂ) := + ⟨!![(z : ℂ), 0; 0, ((z⁻¹ : ℂˣ) : ℂ)], by simp [Matrix.det_fin_two_of]⟩ + +@[simp] +lemma diagSL_inv (z : ℂˣ) : (diagSL z)⁻¹ = diagSL z⁻¹ := by + rw [inv_eq_iff_mul_eq_one] + ext i j + fin_cases i <;> fin_cases j <;> simp [diagSL, Matrix.mul_apply, Fin.sum_univ_two] + +/-- The diagonal element at `z = -1` is the central element `-1` of the Lorentz + group (the lift of a rotation by `2π`). -/ +@[simp] +lemma diagSL_neg_one : diagSL (-1) = -1 := by + ext i j + fin_cases i <;> fin_cases j <;> simp [diagSL] + +/-- The unit `2 * I` of `ℂ`. The associated diagonal Lorentz transformation + `diagSL twoI` detects selection rules which real diagonal elements miss, since its + scaling factors mix in a phase under conjugation. -/ +def twoI : ℂˣ := + ⟨2 * I, -I / 2, by linear_combination -Complex.I_mul_I, by linear_combination -Complex.I_mul_I⟩ + +@[simp] +lemma twoI_val : ((twoI : ℂˣ) : ℂ) = 2 * I := (rfl) + +@[simp] +lemma twoI_inv_val : ((twoI⁻¹ : ℂˣ) : ℂ) = -I / 2 := (rfl) + +/-! + +### B. Field specification for the theory + +-/ + +/-- The specification of the field components appearing in the effective potential: + the two components `ψ α` of the left-handed Weyl fermion and the two components + `barψ α` of its conjugate. -/ +inductive FieldSpecification : Type + | ψ (α : Fin 2) : FieldSpecification + | barψ (α : Fin 2) : FieldSpecification +deriving DecidableEq, Repr + +namespace FieldSpecification + +open EFTLagrangianExclDeriv + +instance : Fintype FieldSpecification where + elems := {ψ 0, ψ 1, barψ 0, barψ 1} + complete := by + intro x + match x with + | ψ 0 => simp + | ψ 1 => simp + | barψ 0 => simp + | barψ 1 => simp + +/-! + +## Ordering on FieldSpecification + +We define an ordering on `FieldSpecification`. +This ordering is a choice, and nothing physical can depend on this choice. +We however make it as it simplifies the proofs of lots of lemmas, and +makes it easy to do more calculational aspects. + +-/ + +/-- The equivalence between `FieldSpecification` and `Fin 2 ⊕ Fin 2` sending `ψ α` to + the left and `barψ α` to the right component. -/ +def toSumFin : FieldSpecification ≃ Fin 2 ⊕ Fin 2 where + toFun := fun | .ψ (α : Fin 2) => Sum.inl α | .barψ α => Sum.inr α + invFun := fun | .inl α => ψ α | .inr α => barψ α + left_inv f := by cases f <;> rfl + right_inv x := by cases x <;> rfl + + +/-- The basis of the module underlying the effective potential indexed by + `FieldSpecification`: `ψ α` corresponds to the dual basis of the left-handed Weyl + fermion and `barψ α` to the dual basis of its conjugate. -/ +def moduleBasis : Basis FieldSpecification ℂ + (Module.Dual ℂ LeftHandedWeyl × Module.Dual ℂ (ConjModule LeftHandedWeyl)) := + (LeftHandedWeyl.basis.dualBasis.prod LeftHandedWeyl.basis.conj.dualBasis).reindex toSumFin.symm + +/-- The image of a field specification in the effective potential, as the + exterior-algebra generator of the corresponding basis vector. Denoted `[ψ]ₑ`. -/ +def toEFTLagrangianExclDeriv (ψ : FieldSpecification) : EFTLagrangianExclDeriv := + ExteriorAlgebra.ι ℂ (moduleBasis ψ) + +scoped notation "[" v "]ₑ" => toEFTLagrangianExclDeriv v + +lemma toEFTLagrangianExclDeriv_eq (ψ : FieldSpecification) : + toEFTLagrangianExclDeriv ψ = ExteriorAlgebra.ι ℂ (moduleBasis ψ) := rfl + +lemma toEFTLagrangianExclDeriv_ψ_eq (α : Fin 2) : [ψ α]ₑ = + ExteriorAlgebra.ι ℂ (LinearMap.inl ℂ _ _ (LeftHandedWeyl.basis.dualBasis α)) := by + fin_cases α <;> simp [toEFTLagrangianExclDeriv_eq, moduleBasis, toSumFin] + +lemma toEFTLagrangianExclDeriv_barψ_eq (α : Fin 2) : [barψ α]ₑ = + ExteriorAlgebra.ι ℂ (LinearMap.inr ℂ _ _ (LeftHandedWeyl.basis.conj.dualBasis α)) := by + fin_cases α <;> simp [toEFTLagrangianExclDeriv_eq, moduleBasis, toSumFin] + +@[simp] +lemma toEFTLagrangianExclDeriv_mul_self (ψ : FieldSpecification) : [ψ]ₑ * [ψ]ₑ = 0 := by + simp [toEFTLagrangianExclDeriv_eq] + +lemma toEFTLagrangianExclDeriv_mul_anti_commute (ψ χ : FieldSpecification) : + [ψ]ₑ * [χ]ₑ = - [χ]ₑ * [ψ]ₑ := by + simp [toEFTLagrangianExclDeriv_eq, neg_mul, eq_neg_iff_add_eq_zero] + +lemma rep_apply_toEFTLagrangianExclDeriv_ψ_eq_sum (Λ : SL(2, ℂ)) (α : Fin 2) : + rep Λ [ψ α]ₑ = ∑ (β : Fin 2), Λ⁻¹ α β • [ψ β]ₑ := by + simp only [toEFTLagrangianExclDeriv_ψ_eq, Basis.coe_dualBasis, LinearMap.coe_inl, rep_apply, + Representation.dual_apply, ExteriorAlgebra.map_apply_ι, LinearMap.prodMap_apply, map_zero, + ← map_smul, Prod.smul_mk, smul_zero, Fin.sum_univ_two, Fin.isValue, ← map_add, Prod.mk_add_mk, + add_zero, ExteriorAlgebra.ι_inj, Prod.mk.injEq, and_true] + refine LeftHandedWeyl.basis.ext fun l => ?_ + fin_cases α <;> fin_cases l <;> + simp [Module.Dual.transpose_apply, LeftHandedWeyl.rep_apply_basis, + -SpecialLinearGroup.coe_inv] + +lemma rep_apply_toEFTLagrangianExclDeriv_barψ_eq_sum (Λ : SL(2, ℂ)) (α : Fin 2) : + rep Λ [barψ α]ₑ = ∑ β, star (Λ⁻¹ α β) • [barψ β]ₑ := by + simp only [toEFTLagrangianExclDeriv_barψ_eq, Basis.coe_dualBasis, LinearMap.coe_inr, rep_apply, + Representation.dual_apply, + ExteriorAlgebra.map_apply_ι, LinearMap.prodMap_apply, map_zero, RCLike.star_def, ← map_smul, + Prod.smul_mk, smul_zero, Fin.sum_univ_two, Fin.isValue, ← map_add, Prod.mk_add_mk, add_zero, + ExteriorAlgebra.ι_inj, Prod.mk.injEq, true_and] + refine LeftHandedWeyl.basis.conj.ext fun l => ?_ + fin_cases α <;> fin_cases l <;> + simp [Module.Dual.transpose_apply, LeftHandedWeyl.rep_apply_basis, + -SpecialLinearGroup.coe_inv, Representation.conj_apply] + +/-! + +## Scaling of the fields under diagonal Lorentz transformations + +-/ + +/-- The factor by which the field specifications scale under the action of `diagSL z`. -/ +def diagScale (z : ℂˣ) : FieldSpecification → ℂ + | .ψ α => if α = 0 then ((z⁻¹ : ℂˣ) : ℂ) else z + | .barψ α => if α = 0 then star ((z⁻¹ : ℂˣ) : ℂ) else star (z : ℂ) + +lemma rep_diagSL_apply (z : ℂˣ) (φ : FieldSpecification) : + rep (diagSL z) [φ]ₑ = diagScale z φ • [φ]ₑ := by + match φ with + | .ψ α => + rw [rep_apply_toEFTLagrangianExclDeriv_ψ_eq_sum, diagSL_inv] + fin_cases α <;> simp [diagSL, diagScale, Fin.sum_univ_two] + | .barψ α => + rw [rep_apply_toEFTLagrangianExclDeriv_barψ_eq_sum, diagSL_inv] + fin_cases α <;> simp [diagSL, diagScale, Fin.sum_univ_two] + +@[simp] +lemma diagScale_neg_one (φ : FieldSpecification) : diagScale (-1) φ = -1 := by + cases φ <;> simp [diagScale] + +lemma diagScale_twoI_ψ (α : Fin 2) : + diagScale twoI (ψ α) = if α = 0 then -I / 2 else 2 * I := by + simp only [diagScale, twoI_val, twoI_inv_val] + +lemma diagScale_twoI_barψ (α : Fin 2) : + diagScale twoI (barψ α) = if α = 0 then I / 2 else -(2 * I) := by + simp only [diagScale, twoI_val, twoI_inv_val] + split_ifs <;> simp [Complex.conj_I] + +/-- Every field scales by `-1` under the central element `-1` of the Lorentz group + (fermion parity): the special case `z = -1` of `rep_diagSL_apply`. -/ +lemma rep_neg_one_apply (φ : FieldSpecification) : + rep (-1) [φ]ₑ = (-1 : ℂ) • [φ]ₑ := by + rw [← diagSL_neg_one, rep_diagSL_apply, diagScale_neg_one] + +/-- Under `diagSL twoI` the total scaling of a mixed pair `ψ α`, `barψ β` is never `1`: + the four possible products are `1 / 4`, `-1`, `-1` and `4`. This is the numerical + input to the selection rule `irrepCoeff_ψ_barψ_eq_zero_of_isInvariant`. -/ +lemma diagScale_twoI_ψ_mul_barψ_ne_one (α β : Fin 2) : + diagScale twoI (ψ α) * diagScale twoI (barψ β) ≠ 1 := by + fin_cases α <;> fin_cases β <;> + simp only [diagScale_twoI_ψ, diagScale_twoI_barψ, Fin.zero_eta, Fin.mk_one, Fin.reduceEq, + reduceIte] + -- The four cases are the four weight products `1/4`, `-1`, `-1` and `4`. Each + -- counterfactual is routed through `linear_combination` with `I * I = -1` to a + -- rational equation, since `norm_num` alone treats `I` as an opaque atom; no uniform + -- closer exists (the modulus argument degenerates for the two `-1` cases). + · intro hcontra + have h : (1 / 4 : ℂ) = 1 := by + linear_combination hcontra + (1 / 4 : ℂ) * Complex.I_mul_I + norm_num at h + · intro hcontra + have h : (-1 : ℂ) = 1 := by linear_combination hcontra - Complex.I_mul_I + norm_num at h + · intro hcontra + have h : (-1 : ℂ) = 1 := by linear_combination hcontra - Complex.I_mul_I + norm_num at h + · intro hcontra + have h : (4 : ℂ) = 1 := by linear_combination hcontra + 4 * Complex.I_mul_I + norm_num at h + +/-! + +## The irreps + +-/ + +/-- The irreducible representations of the Lorentz group present in the effective + potential: `ψ` for the left-handed Weyl fermion and `barψ` for its conjugate. -/ +inductive Irrep + | ψ + | barψ +deriving DecidableEq, Fintype + +/-- The irrep in which a field specification sits. -/ +def toIrrep : FieldSpecification → Irrep + | .ψ _ => .ψ + | .barψ _ => .barψ + +@[simp] +lemma toIrrep_ψ (α : Fin 2) : toIrrep (ψ α) = Irrep.ψ := rfl + +@[simp] +lemma toIrrep_barψ (α : Fin 2) : toIrrep (barψ α) = Irrep.barψ := rfl + +lemma rep_apply_toEFTLagrangianExclDeriv_mem_irrep (Λ : SL(2, ℂ)) (ψ : FieldSpecification) : + ∃ n, ∃ F : Fin n → FieldSpecification, (∃ f : Fin n → ℂ, rep Λ [ψ]ₑ = ∑ x, f x • [F x]ₑ) ∧ + (∀ x, toIrrep (F x) = toIrrep ψ) := by + match ψ with + | .ψ α => + exact ⟨2, .ψ, ⟨Λ⁻¹ α, rep_apply_toEFTLagrangianExclDeriv_ψ_eq_sum Λ α⟩, by simp⟩ + | .barψ α => + exact ⟨2, .barψ, ⟨star (Λ⁻¹ α), rep_apply_toEFTLagrangianExclDeriv_barψ_eq_sum Λ α⟩, + by simp⟩ + +/-! + +## Mass dimension + +-/ + +/-- The mass dimension of each field specification; a Weyl fermion in four dimensions + has mass dimension `3 / 2`. -/ +def massDimension : FieldSpecification → ℚ + | .ψ _ => 3 / 2 + | .barψ _ => 3 / 2 + +@[simp] +lemma massDimension_eq (f : FieldSpecification) : massDimension f = 3 / 2 := by + cases f <;> rfl + +lemma massDimension_pos (f : FieldSpecification) : 0 < massDimension f := by + rw [massDimension_eq] + norm_num + +/-- In a theory whose fields all have the same mass dimension, the overall mass + dimension of an operator just counts its fields. -/ +lemma sum_map_massDimension (s : Multiset FieldSpecification) : + (s.map massDimension).sum = 3 / 2 * (Multiset.card s : ℚ) := by + induction s using Multiset.induction with + | empty => simp + | cons a t ih => + rw [Multiset.map_cons, Multiset.sum_cons, ih, Multiset.card_cons, massDimension_eq] + push_cast + ring + +/-- The mass dimension of a field specification in units of half mass dimensions, + so that a Weyl fermion has scaled mass dimension `3`. Unlike `massDimension` this + is usable with `decide`, since natural-number arithmetic reduces in the kernel. -/ +def massDimensionNat : FieldSpecification → ℕ + | .ψ _ => 3 + | .barψ _ => 3 + +@[simp] +lemma massDimensionNat_eq (f : FieldSpecification) : massDimensionNat f = 3 := by + cases f <;> rfl + +lemma massDimensionNat_cast (f : FieldSpecification) : + (massDimensionNat f : ℚ) = massDimension f * 2 := by + rw [massDimensionNat_eq, massDimension_eq] + norm_num + + +/-! + +## Conjugation + +-/ + +def conjugate (ψ : FieldSpecification) : FieldSpecification := + match ψ with + | .ψ α => .barψ α + | .barψ α => .ψ α + +end FieldSpecification + +namespace EFTLagrangianExclDeriv + +open FieldSpecification + +/-! + +## Elements from a list of FieldSpecifications +-/ + +/-- The operator in the effective potential given by the ordered product of the + fields in `l`. -/ +def termOfList (l : List FieldSpecification) : EFTLagrangianExclDeriv := + (l.map toEFTLagrangianExclDeriv).prod + +lemma termOfList_cons (ψ : FieldSpecification) (l : List FieldSpecification) : + termOfList (ψ :: l) = [ψ]ₑ * termOfList l := by simp [termOfList] + +@[simp] +lemma termOfList_nil : termOfList [] = 1 := by simp [termOfList] + +lemma termOfList_singleton (ψ : FieldSpecification) : termOfList [ψ] = [ψ]ₑ := by + simp [termOfList_cons] + +lemma termOfList_append (l1 l2 : List FieldSpecification) : + termOfList (l1 ++ l2) = termOfList l1 * termOfList l2 := by + simp [termOfList] + +lemma mul_termOfList_of_mem (ψ : FieldSpecification) (l : List FieldSpecification) + (hψ : ψ ∈ l) : [ψ]ₑ * termOfList l = 0 := by + induction l with + | nil => simp at hψ + | cons β t ih => + rcases List.mem_cons.mp hψ with rfl | ha + · simp [termOfList_cons, ← mul_assoc] + · simp [termOfList_cons, ← mul_assoc, toEFTLagrangianExclDeriv_mul_anti_commute ψ β] + simp [mul_assoc, ih ha] + +lemma termOfList_comm_fieldSpecification (ψ : FieldSpecification) (l : List FieldSpecification) : + termOfList l * [ψ]ₑ = ((-1) ^ l.length : ℂ) • ([ψ]ₑ * termOfList l) := by + induction l with + | nil => simp + | cons β t ih => + simp only [termOfList_cons, mul_assoc, ih, Algebra.mul_smul_comm, List.length_cons] + simp only [← mul_assoc, toEFTLagrangianExclDeriv_mul_anti_commute β ψ, neg_mul, smul_neg] + ring_nf + simp + +lemma termOfList_zero_of_not_nodup (l : List FieldSpecification) (h : ¬ l.Nodup) : + termOfList l = 0 := by + revert h + induction l with + | nil => intro h; exact absurd List.nodup_nil h + | cons a t ih => + intro h + rw [termOfList_cons] + by_cases hmem : a ∈ t + · exact mul_termOfList_of_mem a t hmem + · rw [ih fun hn => h (List.nodup_cons.mpr ⟨hmem, hn⟩), mul_zero] + +lemma rep_termOfList_eq_map_rep (Λ : SL(2, ℂ)) (l : List FieldSpecification) : + rep Λ (termOfList l) = ((l.map toEFTLagrangianExclDeriv).map (rep Λ)).prod := by + induction l with + | nil => simp + | cons i l ih => + simp [termOfList_cons, rep_mul, ih] + +lemma rep_termOfList_of_monomial (g : SL(2, ℂ)) (σ : Equiv.Perm FieldSpecification) + (d : FieldSpecification → ℂ) (hg : ∀ ψ, rep g [ψ]ₑ = d ψ • [σ ψ]ₑ) + (l : List FieldSpecification) : + rep g (termOfList l) = (l.map d).prod • termOfList (l.map σ):= by + induction l with + | nil => simp + | cons a l ih => + rw [termOfList_cons, rep_mul, hg, ih] + simp [termOfList_cons, smul_smul, mul_comm] + +lemma rep_scale_termOfList_of_rep_scale_toEFTLagrangianExclDeriv (Λ : SL(2, ℂ)) + (h : ∀ ψ, ∃ c : ℂ, rep Λ [ψ]ₑ = c • [ψ]ₑ) (l : List FieldSpecification) : + ∃ c : ℂ, rep Λ (termOfList l) = c • termOfList l := by + induction l with + | nil => exact ⟨1, by simp⟩ + | cons ψ t ih => + obtain ⟨cψ, hcψ⟩ := h ψ + obtain ⟨ct, hct⟩ := ih + refine ⟨cψ * ct, ?_⟩ + simp [termOfList_cons, rep_mul, hcψ, hct] + module + + +lemma rep_termOfList_eq_sum_of_toIrrep (Λ : SL(2, ℂ)) (l : List FieldSpecification) : + ∃ n, ∃ F : Fin n → List FieldSpecification, + (∃ f : Fin n → ℂ, rep Λ (termOfList l) = ∑ x, f x • termOfList (F x)) ∧ + (∀ x, (F x).map toIrrep = l.map toIrrep) := by + induction l with + | nil => + refine ⟨1, fun _ => [], ⟨fun _ => 1, by simp⟩, fun _ => rfl⟩ + | cons ψ t ih => + obtain ⟨n, F, ⟨f, hf⟩, hF⟩ := ih + obtain ⟨nψ, Fψ, ⟨fψ, hfψ⟩, hFψ⟩ := rep_apply_toEFTLagrangianExclDeriv_mem_irrep Λ ψ + use nψ * n + let F' : Fin nψ × Fin n → List FieldSpecification := fun ⟨i, j⟩ => Fψ i :: F j + use F' ∘ finProdFinEquiv.symm + refine ⟨?_, ?_⟩ + · use (fun ⟨i, j⟩ => fψ i * f j) ∘ finProdFinEquiv.symm + rw [← finProdFinEquiv.sum_comp] + simp [termOfList_cons, rep_mul, F', hfψ, hf] + rw [Fintype.sum_mul_sum, Fintype.sum_prod_type] + simp [smul_smul] + congr + funext x + congr + funext y + ring_nf + · intro x + obtain ⟨x, rfl⟩ := finProdFinEquiv.surjective x + simp [F', hF, hFψ] + +lemma mem_termOfList_span (V : EFTLagrangianExclDeriv) : + V ∈ Submodule.span ℂ (Set.range termOfList) := by + induction V using ExteriorAlgebra.induction with + | algebraMap r => + rw [Algebra.algebraMap_eq_smul_one] + exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨[], termOfList_nil⟩) + | ι v => + rw [← Basis.sum_repr moduleBasis v, map_sum] + refine Submodule.sum_mem _ fun f _ => ?_ + rw [map_smul] + exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨[f], by simp [termOfList_singleton]; rfl⟩) + | mul a b ha hb => + induction ha using Submodule.span_induction with + | mem x hx => + obtain ⟨l1, rfl⟩ := hx + induction hb using Submodule.span_induction with + | mem y hy => + obtain ⟨l2, rfl⟩ := hy + exact Submodule.subset_span ⟨l1 ++ l2, termOfList_append l1 l2⟩ + | zero => simp + | add y z _ _ hy hz => rw [mul_add]; exact add_mem hy hz + | smul c y _ hy => rw [mul_smul_comm]; exact Submodule.smul_mem _ _ hy + | zero => simp + | add x y _ _ hx hy => rw [add_mul]; exact add_mem hx hy + | smul c x _ hx => rw [smul_mul_assoc]; exact Submodule.smul_mem _ _ hx + | add a b ha hb => exact add_mem ha hb + +lemma termOfList_perm_neq_zero {l1 l2 : List FieldSpecification} (h : l1.Perm l2) : + ∃ c : ℂ, termOfList l1 = c • termOfList l2 ∧ (c = 1 ∨ c = -1) := by + induction h with + | nil => exact ⟨1, by simp⟩ + | cons x _ ih => + obtain ⟨c, hc1, hc2⟩ := ih + exact ⟨c, by rw [termOfList_cons, termOfList_cons, hc1, mul_smul_comm], hc2⟩ + | swap x y l => + refine ⟨-1, ?_⟩ + rw [termOfList_cons, termOfList_cons, termOfList_cons, termOfList_cons, ← mul_assoc, + toEFTLagrangianExclDeriv_mul_anti_commute y x] + simp [mul_assoc] + | trans _ _ ih1 ih2 => + obtain ⟨c1, hc1, hc1'⟩ := ih1 + obtain ⟨c2, hc2, hc2'⟩ := ih2 + exact ⟨c1 * c2, by rw [hc1, hc2, smul_smul], by grind⟩ + +lemma termOfList_perm {l1 l2 : List FieldSpecification} (h : l1.Perm l2) : + ∃ c : ℂ, termOfList l1 = c • termOfList l2 := by + obtain ⟨c, h1, h2⟩ := termOfList_perm_neq_zero h + exact ⟨c, h1⟩ + + +lemma termOfList_reverse_eq {l : List FieldSpecification} : + termOfList l.reverse = ((-1) ^ (l.length.choose 2) : ℂ) • termOfList l := by + induction l with + | nil => simp + | cons ψ t ih => + rw [List.reverse_cons, termOfList_append, termOfList_singleton, ih, smul_mul_assoc, + termOfList_comm_fieldSpecification, ← termOfList_cons, smul_smul, ← pow_add, + List.length_cons, Nat.choose_succ_succ, Nat.choose_one_right, Nat.add_comm] + +lemma termOfList_reverse_eq_of_eq {l1 l2 : List FieldSpecification} {c : ℂ} + (h : termOfList l1 = c • termOfList l2) : + termOfList l1.reverse = c • termOfList l2.reverse := by + have hf : ∀ l : List FieldSpecification, + CliffordAlgebra.reverse (termOfList l) = termOfList l.reverse := by + intro l + induction l with + | nil => simp + | cons ψ t ih => + rw [termOfList_cons, CliffordAlgebra.reverse.map_mul, ih, List.reverse_cons, + termOfList_append, termOfList_singleton, toEFTLagrangianExclDeriv_eq, + CliffordAlgebra.reverse_ι] + rw [← hf, ← hf, h, map_smul] + +lemma termOfList_reverse_zero_of_zero {l : List FieldSpecification} (h : termOfList l = 0) : + termOfList l.reverse = 0 := by + rw [termOfList_reverse_eq, h, smul_zero] + +lemma termOfList_conjugate_eq_of_eq {l1 l2 : List FieldSpecification} {c : ℂ} + (h : termOfList l1 = c • termOfList l2) : + termOfList (l1.map conjugate) = c • termOfList (l2.map conjugate) := by + let f := ExteriorAlgebra.map (moduleBasis.constr ℂ fun ψ => moduleBasis (conjugate ψ)) + have hf : ∀ l : List FieldSpecification, f (termOfList l) = termOfList (l.map conjugate) := by + intro l + induction l with + | nil => simp [f] + | cons ψ t ih => + rw [termOfList_cons, List.map_cons, termOfList_cons, map_mul, ih] + congr 1 + simp [f, toEFTLagrangianExclDeriv_eq, ExteriorAlgebra.map_apply_ι] + rw [← hf, ← hf, h, map_smul] + +lemma termOfList_conjugate_zero_of_zero {l : List FieldSpecification} (h : termOfList l = 0) : + termOfList (l.map conjugate) = 0 := by + let f := ExteriorAlgebra.map (moduleBasis.constr ℂ fun ψ => moduleBasis (conjugate ψ)) + have hf : ∀ l : List FieldSpecification, f (termOfList l) = termOfList (l.map conjugate) := by + intro l + induction l with + | nil => simp [f] + | cons ψ t ih => + rw [termOfList_cons, List.map_cons, termOfList_cons, map_mul, ih] + congr 1 + simp [f, toEFTLagrangianExclDeriv_eq, ExteriorAlgebra.map_apply_ι] + rw [← hf, h] + simp + +lemma termOfList_eq_ιMulti (l : List FieldSpecification) : + termOfList l = ExteriorAlgebra.ιMulti ℂ l.length (fun i => moduleBasis (l.get i)) := by + induction l with + | nil => simp + | cons ψ l h => + simp [termOfList_cons, h] + rfl + +lemma termOfList_ofFn {n : ℕ} (g : Fin n → FieldSpecification) : + termOfList (List.ofFn g) = ExteriorAlgebra.ιMulti ℂ n (fun i => moduleBasis (g i)) := by + rw [ExteriorAlgebra.ιMulti_apply, termOfList, List.map_ofFn] + rfl + +/-! + +## Construction of a term from a tuple + +-/ + +/-- The operator in the effective potential given by the ordered product of the + fields in the tuple `g`. -/ +def termOfTuple {n} (g : Fin n → FieldSpecification) : EFTLagrangianExclDeriv := + termOfList (List.ofFn g) + +lemma termOfTuple_eq_ιMulti {n} (g : Fin n → FieldSpecification) : + termOfTuple g = ExteriorAlgebra.ιMulti ℂ n (fun i => moduleBasis (g i)) := by + rw [termOfTuple, termOfList_ofFn] + +lemma termOfTuple_perm {n} (g : Fin n → FieldSpecification) {i j : Fin n} (hij : i ≠ j) : + termOfTuple (g ∘ Equiv.swap i j) = - termOfTuple g := by + rw [termOfTuple_eq_ιMulti, termOfTuple_eq_ιMulti] + exact AlternatingMap.map_swap (ExteriorAlgebra.ιMulti ℂ n) (fun k => moduleBasis (g k)) hij + +/-- The alternating map taking a tuple of vectors to their product in the + effective potential. -/ +def termOfVectTuple {n} : + AlternatingMap ℂ (Module.Dual ℂ LeftHandedWeyl × Module.Dual ℂ (ConjModule LeftHandedWeyl)) + EFTLagrangianExclDeriv (Fin n) := ExteriorAlgebra.ιMulti ℂ n + +/-- The alternating map underlying `coeff s`: a tuple of vectors is sent to + `termOfTuple g` weighted by the product of the `g`-coordinates of the vectors, + summed over the tuples `g` of fields with field content `s`. -/ +def coeffOfVectorTuple (s : Multiset FieldSpecification) (n : ℕ) : + AlternatingMap ℂ (Module.Dual ℂ LeftHandedWeyl × Module.Dual ℂ (ConjModule LeftHandedWeyl)) + EFTLagrangianExclDeriv (Fin n) where + toMultilinearMap := + ∑ g : Fin n → FieldSpecification, + if Multiset.ofList (List.ofFn g) = s then + (LinearMap.toSpanSingleton ℂ EFTLagrangianExclDeriv (termOfTuple g)).compMultilinearMap + ((MultilinearMap.mkPiAlgebra ℂ (Fin n) ℂ).compLinearMap fun i => moduleBasis.coord (g i)) + else 0 + map_eq_zero_of_eq' := by + intro v i j hv hij + have hvswap : ∀ k, v (Equiv.swap i j k) = v k := by + intro k + rcases eq_or_ne k i with rfl | hki + · rw [Equiv.swap_apply_left]; exact hv.symm + rcases eq_or_ne k j with rfl | hkj + · rw [Equiv.swap_apply_right]; exact hv + · rw [Equiv.swap_apply_of_ne_of_ne hki hkj] + simp only [MultilinearMap.toFun_eq_coe, _root_.sum_apply] + refine Finset.sum_involution (fun g _ => g ∘ Equiv.swap i j) ?_ ?_ + (fun g _ => Finset.mem_univ _) ?_ + · intro g _ + have hms : Multiset.ofList (List.ofFn (g ∘ Equiv.swap i j)) = + Multiset.ofList (List.ofFn g) := + Multiset.coe_eq_coe.mpr ((Equiv.swap i j).ofFn_comp_perm g) + rw [hms] + split_ifs with h + · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply, + MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply, + Function.comp_apply] + have hprod : ∏ k, moduleBasis.coord (g (Equiv.swap i j k)) (v k) = + ∏ k, moduleBasis.coord (g k) (v k) := + calc ∏ k, moduleBasis.coord (g (Equiv.swap i j k)) (v k) + = ∏ k, moduleBasis.coord (g (Equiv.swap i j k)) (v (Equiv.swap i j k)) := + Finset.prod_congr rfl fun k _ => by rw [hvswap k] + _ = ∏ k, moduleBasis.coord (g k) (v k) := + Equiv.prod_comp (Equiv.swap i j) fun k => moduleBasis.coord (g k) (v k) + rw [hprod, termOfTuple_perm g hij, smul_neg, add_neg_cancel] + · simp + · intro g _ hfg hcontra + apply hfg + have hgji : g j = g i := by + simpa [Equiv.swap_apply_left] using congrFun hcontra i + have hterm : termOfTuple g = 0 := by + rw [termOfTuple_eq_ιMulti] + exact AlternatingMap.map_eq_zero_of_eq _ _ (by rw [hgji]) hij + split_ifs + · simp [hterm] + · simp + · intro g _ + funext k + simp [Function.comp, Equiv.swap_apply_self] + +/-! + +## Coefficents + +We can't define a basis on effective potential without choosing and ordering on the field +specification. To get around this, we can define the coefficient of an effective potential given a +multi-set of field specifications as a linear map which projects down onto a subspace spanned by +terms which are of the correct type. It actually projects down onto a one-dimensional subspace, and +this is where you can think of it as a coefficient. + +-/ + +/-- The projection of an effective potential onto the span of the operators with + field content `s`. As described above, this plays the role of the coefficient + of the operator `s` in the effective potential. -/ +def coeff (s : Multiset FieldSpecification) : + EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv := + ExteriorAlgebra.liftAlternating (coeffOfVectorTuple s) + +lemma coeff_apply_termOfList (s : Multiset FieldSpecification) (l : List FieldSpecification) : + coeff s (termOfList l) = if Multiset.ofList l = s then termOfList l else 0 := by + have hterm : termOfTuple l.get = termOfList l := by rw [termOfTuple, List.ofFn_get] + rw [coeff, termOfList_eq_ιMulti, ExteriorAlgebra.liftAlternating_apply_ιMulti] + simp only [coeffOfVectorTuple, AlternatingMap.coe_mk, _root_.sum_apply] + refine (Finset.sum_eq_single l.get ?_ ?_).trans ?_ + · intro g _ hg + obtain ⟨i, hi⟩ := Function.ne_iff.mp hg + split_ifs with h + · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply, + MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply] + have hzero : ∏ k, moduleBasis.coord (g k) (moduleBasis (l.get k)) = 0 := + Finset.prod_eq_zero (Finset.mem_univ i) (by + rw [Basis.coord_apply, Basis.repr_self, Finsupp.single_eq_of_ne hi]) + rw [hzero, zero_smul] + · simp + · intro h + exact absurd (Finset.mem_univ _) h + · rw [List.ofFn_get] + split_ifs with h + · simp only [LinearMap.compMultilinearMap_apply, MultilinearMap.compLinearMap_apply, + MultilinearMap.mkPiAlgebra_apply, LinearMap.toSpanSingleton_apply, hterm] + have hprod : ∏ i, moduleBasis.coord (l.get i) (moduleBasis (l.get i)) = 1 := by simp + rw [hprod, one_smul] + exact termOfList_eq_ιMulti l + · simp + +lemma coeff_one (s : Multiset FieldSpecification) : coeff s 1 = if s = ∅ then 1 else 0 := by + trans coeff s (termOfList []) + · simp + · rw [coeff_apply_termOfList] + simp + grind + +@[simp] +lemma coeff_coeff_self {s : Multiset FieldSpecification} (V : EFTLagrangianExclDeriv) : + coeff s (coeff s V) = coeff s V := by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp at hV' + obtain ⟨l, rfl⟩ := hV' + simp [coeff_apply_termOfList, apply_ite] + grind + · simp + · simp [hx, hy] + · simp [hx] + +lemma coeff_coeff_eq_zero_of_diff {s1 s2 : Multiset FieldSpecification} (h : s1 ≠ s2) + (V : EFTLagrangianExclDeriv) : coeff s1 (coeff s2 V) = 0 := by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp at hV' + obtain ⟨l, rfl⟩ := hV' + simp [coeff_apply_termOfList, apply_ite] + grind + · simp + · simp [hx, hy] + · simp [hx] + +lemma coeff_sum_eq_zero_iff (V : EFTLagrangianExclDeriv) + (S : Finset (Multiset FieldSpecification)): + ∑ s ∈ S, coeff s V = 0 ↔ ∀ s ∈ S, coeff s V = 0 := by + constructor + · intro h s hs + have h1 := congrArg (coeff s) h + simp at h1 + rw [Finset.sum_eq_single s] at h1 + simpa using h1 + · intro b hb hx + exact coeff_coeff_eq_zero_of_diff (id (Ne.symm hx)) V + · simp_all + · intro h + exact Finset.sum_eq_zero h + +lemma coeff_eq_termOfList {s : Multiset FieldSpecification} + (V : EFTLagrangianExclDeriv) {l : List FieldSpecification} (hl : Multiset.ofList l = s) : + ∃ c : ℂ, coeff s V = c • termOfList l := by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp at hV' + obtain ⟨l', rfl⟩ := hV' + simp [coeff_apply_termOfList] + split_ifs + · rename_i hi + refine termOfList_perm ?_ + rw [← Multiset.coe_eq_coe] + simp_all + · use 0 + simp + · use 0 + simp + · obtain ⟨c1, hx⟩ := hx + obtain ⟨c2, hy⟩ := hy + use (c1 + c2) + simp [hx, hy] + module + · obtain ⟨c1, hx⟩ := hx + use a • c1 + simp [hx, smul_smul] + +lemma coeff_eq_exists_termOfList (s : Multiset FieldSpecification) + (V : EFTLagrangianExclDeriv) : + ∃ l, ∃ c : ℂ, (coeff s V = c • termOfList l) ∧ Multiset.ofList l = s := by + obtain ⟨c, hl⟩ := coeff_eq_termOfList V (s := s) (l := Multiset.toList s) (by simp) + use Multiset.toList s + use c + simp [hl] + +lemma coeff_monomial_selection_rule (g : SL(2, ℂ)) (σ : Equiv.Perm FieldSpecification) + (d : FieldSpecification → ℂ) (hg : ∀ ψ, rep g [ψ]ₑ = d ψ • [σ ψ]ₑ) + (s : Multiset FieldSpecification) (V : EFTLagrangianExclDeriv) (hV : IsInvariant V) : + coeff (s.map σ) V = rep g (coeff s V) := by + suffices h : ∀ W, coeff (s.map σ) (rep g W) = rep g (coeff s W) by + specialize h V + rw [hV g] at h + exact h + intro W + induction' mem_termOfList_span W using Submodule.span_induction with W' hW' x y _ _ hx hy + a x _ hx + · simp only [Set.mem_range] at hW' + obtain ⟨l, rfl⟩ := hW' + rw [rep_termOfList_of_monomial g σ d hg, map_smul, + coeff_apply_termOfList, coeff_apply_termOfList] + have hcond : Multiset.ofList (List.map σ l) = Multiset.map σ s ↔ + Multiset.ofList l = s := by + rw [← Multiset.map_coe] + exact ⟨fun hc => Multiset.map_injective σ.injective hc, fun hc => by rw [hc]⟩ + split_ifs with h1 h2 h2 + · rw [rep_termOfList_of_monomial g σ d hg] + · exact absurd (hcond.mp h1) h2 + · exact absurd (hcond.mpr h2) h1 + · simp + · simp + · simp [hx, hy] + · simp [hx] + +/-- If the action of `g` is to permute the fields, + then it defines a relation between the coefficients of the effective potential. -/ +lemma coeff_perm_selection_rule (g : SL(2, ℂ)) (σ : Equiv.Perm FieldSpecification) + (hg : ∀ ψ, rep g [ψ]ₑ = [σ ψ]ₑ) (s : Multiset FieldSpecification) + (V : EFTLagrangianExclDeriv) (hV : IsInvariant V) : + coeff (s.map σ) V = rep g (coeff s V) := by + apply coeff_monomial_selection_rule g σ (fun _ => 1) ?_ s V hV + intro ψ + simpa using hg ψ + +lemma coeff_U1_selection_rule {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) + (g : SL(2, ℂ)) (d : FieldSpecification → ℂ) (hg : ∀ ψ, rep g [ψ]ₑ = d ψ • [ψ]ₑ) + (s : Multiset FieldSpecification) (hs : (s.map d).prod ≠ 1) : + coeff s V = 0 := by + have h1 : coeff s V = rep g (coeff s V) := by + simpa using coeff_monomial_selection_rule g (Equiv.refl FieldSpecification) d + (by simpa using hg) s V hV + have hfix : rep g (coeff s V) = (s.map d).prod • coeff s V := by + obtain ⟨c, hl⟩ := coeff_eq_termOfList V (s := s) (l := Multiset.toList s) (by simp) + have hprod : ((Multiset.toList s).map d).prod = (s.map d).prod := by + rw [← Multiset.coe_toList s] + simp + rw [hl, map_smul, + rep_termOfList_of_monomial g (Equiv.refl FieldSpecification) d (by simpa using hg)] + simp [smul_smul, hprod, mul_comm] + have h2 : (1 - (s.map d).prod) • coeff s V = 0 := by + rw [sub_smul, one_smul, ← hfix, ← h1, sub_self] + rcases smul_eq_zero.mp h2 with h | h + · exact absurd (sub_eq_zero.mp h).symm hs + · exact h + +/-- The selection rule on coefficients coming from the anti-symmetry of fermionic fields. + Note that this holds for any effective potential, invariant or not. -/ +lemma coeff_fermionic_selection_rule {V : EFTLagrangianExclDeriv} + (s : Multiset FieldSpecification) (hs : ¬ s.Nodup) : + coeff s V = 0 := by + obtain ⟨c, hc⟩ := coeff_eq_termOfList V (s := s) (l := Multiset.toList s) (by simp) + have hl : ¬ (Multiset.toList s).Nodup := by + rw [← Multiset.coe_toList s] at hs + exact fun h => hs (Multiset.coe_nodup.mpr h) + rw [hc, termOfList_zero_of_not_nodup _ hl, smul_zero] + +/-- The selection rule on coefficients saying that + every term with an odd number of fermions is zero. -/ +lemma coeff_odd_selection_rule {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) + (s : Multiset FieldSpecification) (hs : Odd s.card) : coeff s V = 0 := by + refine coeff_U1_selection_rule hV (-1) (fun _ => -1) rep_neg_one_apply s ?_ + rw [Multiset.map_const', Multiset.prod_replicate, hs.neg_one_pow] + norm_num + +@[simp] +lemma coeff_ψ_barψ_selection_rule {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) + (a b : Fin 2) : coeff {.ψ a, .barψ b} V = 0 := by + refine coeff_U1_selection_rule hV (diagSL twoI) (diagScale twoI) (rep_diagSL_apply twoI) _ ?_ + simp only [Multiset.insert_eq_cons, diagScale, Fin.isValue, Units.val_inv_eq_inv_val, twoI_val, + _root_.mul_inv_rev, inv_I, neg_mul, star_neg, star_mul', RCLike.star_def, conj_I, star_inv₀, + star_ofNat, neg_neg, mul_neg, Multiset.map_cons, Multiset.map_singleton, Multiset.prod_cons, + Multiset.prod_singleton, mul_ite, ite_mul, ne_eq] + field_simp + simp only [Fin.isValue, I_sq, neg_neg, neg_mul, one_mul] + grind + +lemma coeff_empty_isInvariant {V : EFTLagrangianExclDeriv} : IsInvariant (coeff 0 V) := by + obtain ⟨c, hc⟩ := coeff_eq_termOfList V (s := 0) (l := []) (by simp) + rw [hc] + refine IsInvariant.smul (fun Λ => ?_) _ + simp + +lemma coeff_ψ_zero_ψ_one_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (coeff {.ψ 0, .ψ 1} V) := by + obtain ⟨c, hc⟩ := coeff_eq_termOfList V (s := {.ψ 0, .ψ 1}) (l := [.ψ 0, .ψ 1]) (by decide) + rw [hc] + refine IsInvariant.smul (fun Λ => ?_) _ + simp only [termOfList, Fin.isValue, List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, + mul_one, rep_mul, rep_apply_toEFTLagrangianExclDeriv_ψ_eq_sum, SpecialLinearGroup.coe_inv, + adjugate_fin_two, of_apply, cons_val', cons_val_fin_one, cons_val_zero, Fin.sum_univ_two, + cons_val_one, mul_add, Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc, + toEFTLagrangianExclDeriv_mul_self, smul_zero, + toEFTLagrangianExclDeriv_mul_anti_commute (.ψ 1) (.ψ 0), neg_mul, smul_neg, ← neg_smul, neg_neg, + zero_add, smul_smul, add_zero, ← add_smul] + trans Λ.1.det • ([.ψ 0]ₑ * [.ψ 1]ₑ) + · simp only [Matrix.det_fin_two] + ring_nf + · simp + +@[simp] +lemma coeff_ψ_ψ_isInvariant {V : EFTLagrangianExclDeriv} (a b : Fin 2) : + IsInvariant (coeff {.ψ a, .ψ b} V) := by + match a, b with + | 0, 0 => rw [coeff_fermionic_selection_rule _ (by decide)]; simp + | 1, 1 => rw [coeff_fermionic_selection_rule _ (by decide)]; simp + | 0, 1 => exact coeff_ψ_zero_ψ_one_isInvariant + | 1, 0 => convert coeff_ψ_zero_ψ_one_isInvariant using 3; decide + +lemma coeff_barψ_zero_barψ_one_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (coeff {.barψ 0, .barψ 1} V) := by + obtain ⟨c, hc⟩ := coeff_eq_termOfList V (s := {.barψ 0, .barψ 1}) (l := [.barψ 0, .barψ 1]) + (by decide) + rw [hc] + refine IsInvariant.smul (fun Λ => ?_) _ + simp only [termOfList, Fin.isValue, List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, + mul_one, rep_mul, rep_apply_toEFTLagrangianExclDeriv_barψ_eq_sum, SpecialLinearGroup.coe_inv, + adjugate_fin_two, of_apply, cons_val', cons_val_fin_one, cons_val_zero, RCLike.star_def, + Fin.sum_univ_two, cons_val_one, mul_add, Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc, + toEFTLagrangianExclDeriv_mul_self, smul_zero, + toEFTLagrangianExclDeriv_mul_anti_commute (.barψ 1) (.barψ 0), neg_mul, smul_neg, ← neg_smul, + ← map_neg, neg_neg, zero_add, smul_smul, ← map_mul, add_zero, ← add_smul, ← map_add] + trans (starRingEnd ℂ) Λ.1.det • ([.barψ 0]ₑ * [.barψ 1]ₑ) + · simp only [Matrix.det_fin_two] + ring_nf + · simp + +@[simp] +lemma coeff_barψ_barψ_isInvariant {V : EFTLagrangianExclDeriv} (a b : Fin 2) : + IsInvariant (coeff {.barψ a, .barψ b} V) := by + match a, b with + | 0, 0 => rw [coeff_fermionic_selection_rule _ (by decide)]; simp + | 1, 1 => rw [coeff_fermionic_selection_rule _ (by decide)]; simp + | 0, 1 => exact coeff_barψ_zero_barψ_one_isInvariant + | 1, 0 => convert coeff_barψ_zero_barψ_one_isInvariant using 3; decide + +lemma coeff_quartic_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (coeff {.ψ 0, .ψ 1, .barψ 0, .barψ 1} V) := by + obtain ⟨c', hc⟩ := coeff_eq_termOfList V (s := {.ψ 0, .ψ 1, .barψ 0, .barψ 1}) + (l := [.ψ 0, .ψ 1, .barψ 0, .barψ 1]) (by decide) + rw [hc] + refine IsInvariant.smul (fun Λ => ?_) _ + simp only [termOfList, Fin.isValue, List.map_cons, List.map_nil, List.prod_cons, List.prod_nil, + mul_one, rep_mul, rep_apply_toEFTLagrangianExclDeriv_barψ_eq_sum, SpecialLinearGroup.coe_inv, + adjugate_fin_two, of_apply, cons_val', cons_val_fin_one, cons_val_zero, RCLike.star_def, + Fin.sum_univ_two, cons_val_one, mul_add, Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc, + toEFTLagrangianExclDeriv_mul_self, smul_zero, + toEFTLagrangianExclDeriv_mul_anti_commute (.barψ 1) (.barψ 0), neg_mul, smul_neg, ← neg_smul, + ← map_neg, neg_neg, zero_add, smul_smul, ← map_mul, add_zero, ← add_smul, ← map_add] + trans (starRingEnd ℂ) Λ.1.det • ((rep Λ) [ψ 0]ₑ * ((rep Λ) [ψ 1]ₑ * ([barψ 0]ₑ * [barψ 1]ₑ))) + · simp only [Matrix.det_fin_two] + ring_nf + simp only [SpecialLinearGroup.det_coe, map_one, Fin.isValue, + rep_apply_toEFTLagrangianExclDeriv_ψ_eq_sum, SpecialLinearGroup.coe_inv, adjugate_fin_two, + of_apply, cons_val', cons_val_fin_one, cons_val_zero, Fin.sum_univ_two, cons_val_one, + ← mul_assoc, add_mul, Algebra.smul_mul_assoc, mul_add, Algebra.mul_smul_comm, + toEFTLagrangianExclDeriv_mul_self, smul_zero, + toEFTLagrangianExclDeriv_mul_anti_commute (.ψ 1) (.ψ 0), neg_mul, smul_neg, ← neg_smul, neg_neg, + zero_add, smul_smul, add_zero, ← add_smul, mul_neg, one_mul] + trans Λ.1.det • ([ψ 0]ₑ * [ψ 1]ₑ * [barψ 0]ₑ * [barψ 1]ₑ) + · simp only [Matrix.det_fin_two] + ring_nf + · simp + +/-- The support of an effective potential: the set of multisets of field specifications + for which the corresponding coefficient is non-zero. -/ +def support (V : EFTLagrangianExclDeriv) : Finset (Multiset FieldSpecification) := + Set.Finite.toFinset (s := {s | coeff s V ≠ 0}) <| by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp only [Set.mem_range] at hV' + obtain ⟨l, rfl⟩ := hV' + refine (Set.finite_singleton (Multiset.ofList l)).subset ?_ + intro s hs + simp at hs + rw [coeff_apply_termOfList] at hs + rw [Set.mem_singleton_iff] + by_contra hne + exact hs (if_neg fun h => hne h.symm) + · refine Set.finite_empty.subset ?_ + intro s hs + simp at hs + · refine (hx.union hy).subset ?_ + intro s hs + simp at hs + grind + · refine hx.subset ?_ + intro s hs + simp at hs + grind + +@[simp] +lemma support_zero_eq_empty : support (0 : EFTLagrangianExclDeriv) = ∅ := by + simp [support] + +lemma mem_support_iff {V : EFTLagrangianExclDeriv} {s : Multiset FieldSpecification} : + s ∈ support V ↔ coeff s V ≠ 0 := by simp [support] + +lemma coeff_eq_zero_of_not_mem_support {V : EFTLagrangianExclDeriv} + {s : Multiset FieldSpecification} (h : s ∉ support V) : coeff s V = 0 := by + simpa [support, Set.Finite.mem_toFinset] using h + +lemma support_add {V W : EFTLagrangianExclDeriv} : + support (V + W) ⊆ support V ∪ support W := by + simp [support] + grind + +lemma support_sub {V W : EFTLagrangianExclDeriv} : + support (V - W) ⊆ support V ∪ support W := by + simp [support] + grind + +lemma support_one : support 1 = {{}} := by + simp [support, coeff_one] + rfl + +lemma support_smul {V : EFTLagrangianExclDeriv} (c : ℂ) : + support (c • V) ⊆ support V := by + simp [support] + +lemma support_smul_neq_zero {V : EFTLagrangianExclDeriv} (c : ℂ) (hc : c ≠ 0) : + support (c • V) = support V := by + simp [support, hc] + +lemma mem_support_termOfList_iff {l : List FieldSpecification} (s : Multiset FieldSpecification): + s ∈ support (termOfList l) ↔ s = Multiset.ofList l ∧ termOfList l ≠ 0 := by + simp [support, coeff_apply_termOfList] + grind + +lemma support_termOfList_subset (l : List FieldSpecification) : + support (termOfList l) ⊆ {Multiset.ofList l} := by + intro s hs + simp [mem_support_termOfList_iff] at hs + simp [hs.1] + +lemma eq_sum_support_coeff (V : EFTLagrangianExclDeriv) : V = ∑ s ∈ support V, coeff s V := by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp only [Set.mem_range] at hV' + obtain ⟨l, rfl⟩ := hV' + trans ∑ s ∈ {Multiset.ofList l}, coeff s (termOfList l); swap + · symm + apply Finset.sum_subset (support_termOfList_subset l) + simp + intro hl + simp [mem_support_termOfList_iff] at hl + rw [hl] + simp + · simp [coeff_apply_termOfList] + · simp + · trans ∑ s ∈ x.support ∪ y.support, coeff s (x + y); swap + · symm + apply Finset.sum_subset + · simp [support_add] + · intro s hs hs' + exact coeff_eq_zero_of_not_mem_support hs' + · conv_lhs => rw [hx, hy] + simp [Finset.sum_add_distrib] + congr 1 + · apply Finset.sum_subset + · simp + · intro s hs hs' + exact coeff_eq_zero_of_not_mem_support hs' + · apply Finset.sum_subset + · simp + · intro s hs hs' + exact coeff_eq_zero_of_not_mem_support hs' + · trans ∑ s ∈ (support x).image (fun s => s), coeff s (a • x); swap + · symm + apply Finset.sum_subset + · simp [support_smul] + · intro s hs hs' + exact coeff_eq_zero_of_not_mem_support hs' + conv_lhs => rw [hx] + simp [Finset.smul_sum] + +lemma nodup_of_mem_support {V : EFTLagrangianExclDeriv} {s : Multiset FieldSpecification} + (hs : s ∈ support V) : s.Nodup := by + simp [support, Set.Finite.mem_toFinset] at hs + by_contra h + exact hs (coeff_fermionic_selection_rule (V := V) s h) + +/-- For a purely fermionic theory, no fermion can appear twice in the same term, + so the support is a subset of those multisets which are actually finite sets. + This does not hold in a bosonic theory. -/ +lemma support_subset_finset_univ {V : EFTLagrangianExclDeriv} : + support V ⊆ (Finset.univ : Finset (Finset FieldSpecification)).image fun V => V.val := by + intro s hs + simp only [Finset.mem_image, Finset.mem_univ, true_and] + exact ⟨Finset.mk s (nodup_of_mem_support hs), rfl⟩ + +/-- Regrouping the decomposition `eq_sum_support_coeff` along a classifying map `key` + on field contents: if `fiber k` is the finset of field contents with `key s = k`, + then an effective potential is the sum of its projections onto the fibers of the + keys appearing in its support. Specialised to irrep content in `eq_sum_irrepCoeff` + and to mass dimension in `eq_sum_massDimCoeff`. -/ +lemma eq_sum_fiber_coeff {κ : Type*} [DecidableEq κ] {key : Multiset FieldSpecification → κ} + {fiber : κ → Finset (Multiset FieldSpecification)} + (hmem : ∀ k s, s ∈ fiber k ↔ key s = k) (V : EFTLagrangianExclDeriv) : + V = ∑ k ∈ (support V).image key, ∑ s ∈ fiber k, coeff s V := by + have hdisj : (((support V).image key : Finset κ) : Set κ).PairwiseDisjoint fiber := by + intro i _ j _ hij + simp only [Function.onFun, Finset.disjoint_left] + intro s hsi hsj + exact hij (((hmem i s).mp hsi).symm.trans ((hmem j s).mp hsj)) + rw [← Finset.sum_biUnion hdisj] + conv_lhs => rw [eq_sum_support_coeff V] + refine Finset.sum_subset (fun s hs => ?_) (fun s _ hs => coeff_eq_zero_of_not_mem_support hs) + exact Finset.mem_biUnion.mpr ⟨key s, Finset.mem_image_of_mem _ hs, (hmem _ s).mpr rfl⟩ + +/-! + +## Mixing of operators under the action of the Lorentz group + +-/ + +/-- Under the action of `g` an operator with field content specified by `s` mixes + into operators with field content given by this Finset. -/ +def repSupport (s : Multiset FieldSpecification) (g : SL(2, ℂ)) : + Finset (Multiset FieldSpecification) := + support (rep g (termOfList (Multiset.toList s))) + +lemma repSupport_eq_termOfList {s : Multiset FieldSpecification} (g : SL(2, ℂ)) + (l : List FieldSpecification) (hl : Multiset.ofList l = s) : + repSupport s g = support (rep g (termOfList l)) := by + simp [repSupport] + obtain ⟨c, h1, hc⟩ := termOfList_perm_neq_zero (l1 := Multiset.toList s) (l2 := l) + (by apply Multiset.coe_eq_coe.mp; simp [hl]) + simp [h1] + apply support_smul_neq_zero + grind + +lemma repSupport_subset_self_of_singleton_subset_self {s : Multiset FieldSpecification} + (g : SL(2, ℂ)) (h : ∀ ψ : FieldSpecification, repSupport {ψ} g ⊆ {{ψ}}) : + repSupport s g ⊆ {s} := by + have hsingle : ∀ ψ : FieldSpecification, ∃ c : ℂ, + rep g (termOfList [ψ]) = c • termOfList [ψ] := by + intro ψ + have hsup := h ψ + rw [repSupport_eq_termOfList g [ψ] (by simp)] at hsup + rcases Finset.subset_singleton_iff.mp hsup with h0 | h1 + · refine ⟨0, ?_⟩ + rw [eq_sum_support_coeff (rep g (termOfList [ψ])), h0] + simp + · obtain ⟨c, hc⟩ := coeff_eq_termOfList (s := {ψ}) (rep g (termOfList [ψ])) + (l := [ψ]) (by simp) + refine ⟨c, ?_⟩ + rw [eq_sum_support_coeff (rep g (termOfList [ψ])), h1, Finset.sum_singleton, hc] + have hlist : ∀ l : List FieldSpecification, ∃ c : ℂ, + rep g (termOfList l) = c • termOfList l := by + intro l + induction l with + | nil => exact ⟨1, by simp⟩ + | cons a l ih => + obtain ⟨c, hc⟩ := ih + obtain ⟨ca, hca⟩ := hsingle a + refine ⟨ca * c, ?_⟩ + rw [show a :: l = [a] ++ l from rfl, termOfList_append, rep_mul, hca, hc, + smul_mul_smul_comm] + obtain ⟨c, hc⟩ := hlist s.toList + intro t ht + rw [repSupport, hc] at ht + have ht' := support_smul c ht + rw [mem_support_termOfList_iff] at ht' + simpa using ht'.1 + + +/-! + + +## Coefficents of irrep terms + + +-/ + +/-- The field content of a term which corresponds to a given irrep content. -/ +def allTermsWithIrrepContent (i : Multiset Irrep) : Finset (Multiset FieldSpecification) := + (multisetsOfCard FieldSpecification i.card).filter (fun s => Multiset.map toIrrep s = i) + +lemma mem_allTermsWithIrrepContent_iff (i : Multiset Irrep) (s : Multiset FieldSpecification) : + s ∈ allTermsWithIrrepContent i ↔ Multiset.map toIrrep s = i := by + simp only [allTermsWithIrrepContent, Finset.mem_filter, mem_multisetsOfCard, + and_iff_right_iff_imp] + intro h + rw [← h, Multiset.card_map] + +/-- The projection of a term of `EFTLagrangianExclDeriv` onto those operators which + have an irrep content determined by `i`. -/ +def irrepCoeff (i : Multiset Irrep) : EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv := + ∑ s ∈ allTermsWithIrrepContent i, coeff s + +lemma irrepCoeff_eq_sum (i : Multiset Irrep) (V : EFTLagrangianExclDeriv) : + irrepCoeff i V = ∑ s ∈ allTermsWithIrrepContent i, coeff s V := by + simp [irrepCoeff] + +lemma irrepCoeff_one (i : Multiset Irrep) : irrepCoeff i 1 = if i = ∅ then 1 else 0 := by + rw [irrepCoeff_eq_sum] + simp only [coeff_one] + rw [Finset.sum_ite_eq'] + refine if_congr ?_ rfl rfl + rw [mem_allTermsWithIrrepContent_iff] + simp [eq_comm] + +lemma irrepCoeff_termOfList (i : Multiset Irrep) (l : List FieldSpecification) : + irrepCoeff i (termOfList l) = if Multiset.map toIrrep (Multiset.ofList l) = i then + termOfList l else 0 := by + simp [irrepCoeff, coeff_apply_termOfList, mem_allTermsWithIrrepContent_iff] + +/-- The irrep contents of the operators appearing in an effective potential. -/ +def irrepSupport (V : EFTLagrangianExclDeriv) : Finset (Multiset Irrep) := + (support V).image (Multiset.map toIrrep) + +lemma mem_irrepSupport_iff (V : EFTLagrangianExclDeriv) (i : Multiset Irrep) : + i ∈ irrepSupport V ↔ irrepCoeff i V ≠ 0 := by + simp [irrepSupport, Finset.mem_image] + constructor + · rintro ⟨s, hs, hsi⟩ + simp [irrepCoeff_eq_sum, coeff_sum_eq_zero_iff] + refine ⟨s, ?_⟩ + simp [mem_allTermsWithIrrepContent_iff, hsi] + exact mem_support_iff.mp hs + · intro h + simp [irrepCoeff_eq_sum, coeff_sum_eq_zero_iff] at h + obtain ⟨s, hs, hsi⟩ := h + use s + simp [mem_allTermsWithIrrepContent_iff] at hs + simp [mem_support_iff, hsi, hs] + +lemma irrepSupport_subset (V : EFTLagrangianExclDeriv) : + irrepSupport V ⊆ {{}, {.ψ}, {.barψ}, {.ψ, .ψ}, {.barψ, .barψ}, {.ψ, .barψ}, + {.ψ, .barψ, .barψ}, {.ψ, .ψ, .barψ}, {.ψ, .ψ, .barψ, .barψ}} := by + trans ((Finset.univ : Finset (Finset FieldSpecification)).image fun V => + V.val).image (Multiset.map toIrrep) + · rw [irrepSupport] + exact Finset.image_subset_image support_subset_finset_univ + · apply Finset.subset_of_eq + decide + +lemma eq_sum_irrepCoeff (V : EFTLagrangianExclDeriv) : + V = ∑ i ∈ irrepSupport V, irrepCoeff i V := by + simp only [irrepSupport, irrepCoeff_eq_sum] + exact eq_sum_fiber_coeff mem_allTermsWithIrrepContent_iff V + +lemma eq_sum_irrepCoeff_subset {V : EFTLagrangianExclDeriv} {S : Finset (Multiset Irrep)} + (hS : irrepSupport V ⊆ S) : V = ∑ i ∈ S, irrepCoeff i V := by + conv_lhs => rw [eq_sum_irrepCoeff V] + apply Finset.sum_subset hS + intro s hs hsi + simpa [mem_irrepSupport_iff] using hsi + +lemma irrepCoeff_rep_termOfList (i : Multiset Irrep) (g : SL(2, ℂ)) + (l : List FieldSpecification) : + rep g (irrepCoeff i (termOfList l)) = irrepCoeff i (rep g (termOfList l)) := by + obtain ⟨n, F, ⟨f, hf⟩, hF⟩ := rep_termOfList_eq_sum_of_toIrrep g l + have hcond : ∀ x, Multiset.map toIrrep (Multiset.ofList (F x)) = + Multiset.map toIrrep (Multiset.ofList l) := by + intro x + rw [Multiset.map_coe, Multiset.map_coe, hF x] + rw [irrepCoeff_termOfList, hf, map_sum] + -- Rewriting with `hcond` transports every summand's irrep-content condition into the + -- outer one, so that `split_ifs` sees a single condition and produces two goals. + simp only [map_smul, irrepCoeff_termOfList, hcond] + split_ifs with h + · exact hf + · simp + +lemma irrepCoeff_rep_apply_fieldSpecification {i : Multiset Irrep} (g : SL(2, ℂ)) + (ψ : FieldSpecification) : + rep g (irrepCoeff i [ψ]ₑ) = irrepCoeff i (rep g [ψ]ₑ) := by + rw [← termOfList_singleton] + exact irrepCoeff_rep_termOfList i g [ψ] + +lemma irrepCoeff_rep {i : Multiset Irrep} {V : EFTLagrangianExclDeriv} (g : SL(2, ℂ)) : + rep g (irrepCoeff i V) = irrepCoeff i (rep g V) := by + induction' mem_termOfList_span V using Submodule.span_induction with V' hV' x y _ _ hx hy + a x _ hx + · simp only [Set.mem_range] at hV' + obtain ⟨l, rfl⟩ := hV' + exact irrepCoeff_rep_termOfList i g l + · simp + · simp [hx, hy] + · simp [hx] + +/-- There is no Lorentz-invariant operator with irrep content `{ψ, barψ}`: + invariance under the diagonal transformation `diagSL twoI` forces every + coefficient of a mixed `ψ`–`barψ` pair to vanish. -/ +lemma irrepCoeff_ψ_barψ_eq_zero_of_isInvariant {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) : + irrepCoeff {Irrep.ψ, Irrep.barψ} V = 0 := by + rw [irrepCoeff_eq_sum, Finset.sum_congr (g := fun s => coeff s V) + (s₂ := {{ψ 0, barψ 0}, {ψ 0, barψ 1}, {ψ 1, barψ 0}, {ψ 1, barψ 1}}) (by decide) (by simp)] + repeat rw [Finset.sum_insert (by decide)] + simp only [coeff_ψ_barψ_selection_rule hV, Finset.sum_singleton, add_zero] + +lemma irrepCoeff_odd_eq_zero_of_isInvariant {V : EFTLagrangianExclDeriv} + (hV : IsInvariant V) (s : Multiset Irrep) (hs : Odd s.card) : irrepCoeff s V = 0 := by + simp [irrepCoeff_eq_sum] + refine Finset.sum_eq_zero ?_ + intro s' hs' + simp [mem_allTermsWithIrrepContent_iff] at hs' + subst hs' + apply coeff_odd_selection_rule hV s' + simpa using hs + +lemma eq_sum_irrepCoeff_of_isInvariant {V : EFTLagrangianExclDeriv} (hV : IsInvariant V) : + V = irrepCoeff {} V + irrepCoeff {Irrep.ψ, Irrep.ψ} V + + irrepCoeff {Irrep.barψ, Irrep.barψ} V + + irrepCoeff {Irrep.ψ, Irrep.ψ, Irrep.barψ, Irrep.barψ} V := by + nth_rewrite 1 [eq_sum_irrepCoeff_subset (irrepSupport_subset V)] + simp +decide [Finset.sum_insert, Finset.sum_singleton, -Multiset.insert_eq_cons, + irrepCoeff_odd_eq_zero_of_isInvariant hV, irrepCoeff_ψ_barψ_eq_zero_of_isInvariant hV] + abel + +/-- Only the terms whose field content is `Nodup` survive in `irrepCoeff i`, since a + repeated fermionic field forces the coefficient to vanish (`coeff_fermionic_selection_rule`). + Hence if exactly one such term `s` exists, `irrepCoeff i` is just `coeff s`. -/ +lemma irrepCoeff_eq_coeff_of_filter_nodup {i : Multiset Irrep} {s : Multiset FieldSpecification} + (h : (allTermsWithIrrepContent i).filter (·.Nodup) = {s}) (V : EFTLagrangianExclDeriv) : + irrepCoeff i V = coeff s V := by + rw [irrepCoeff_eq_sum, ← Finset.sum_filter_of_ne + (fun t _ ht => by by_contra hn; exact ht (coeff_fermionic_selection_rule t hn)), + h, Finset.sum_singleton] + +lemma irrepCoeff_empty_eq {V : EFTLagrangianExclDeriv} : + irrepCoeff 0 V = coeff 0 V := + irrepCoeff_eq_coeff_of_filter_nodup (by decide) V + +lemma irrepCoeff_ψ_ψ_eq {V : EFTLagrangianExclDeriv} : + irrepCoeff {Irrep.ψ, Irrep.ψ} V = coeff {.ψ 0, .ψ 1} V := + irrepCoeff_eq_coeff_of_filter_nodup (by decide) V + +lemma irrepCoeff_barψ_barψ_eq {V : EFTLagrangianExclDeriv} : + irrepCoeff {Irrep.barψ, Irrep.barψ} V = coeff {.barψ 0, .barψ 1} V := + irrepCoeff_eq_coeff_of_filter_nodup (by decide) V + +lemma irrepCoeff_quartic_eq {V : EFTLagrangianExclDeriv} : + irrepCoeff {Irrep.ψ, Irrep.ψ, Irrep.barψ, Irrep.barψ} V = + coeff {.ψ 0, .ψ 1, .barψ 0, .barψ 1} V := + irrepCoeff_eq_coeff_of_filter_nodup (by set_option maxRecDepth 4000 in decide) V + +lemma irrepCoeff_empty_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (irrepCoeff 0 V) := by + rw [irrepCoeff_empty_eq] + exact coeff_empty_isInvariant + +lemma irrepCoeff_ψ_ψ_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (irrepCoeff {Irrep.ψ, Irrep.ψ} V) := by + rw [irrepCoeff_ψ_ψ_eq] + exact coeff_ψ_ψ_isInvariant _ _ + +lemma irrepCoeff_barψ_barψ_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (irrepCoeff {Irrep.barψ, Irrep.barψ} V) := by + rw [irrepCoeff_barψ_barψ_eq] + exact coeff_barψ_barψ_isInvariant _ _ + +lemma irrepCoeff_quadratic_isInvariant {V : EFTLagrangianExclDeriv} : + IsInvariant (irrepCoeff {Irrep.ψ, Irrep.ψ, Irrep.barψ, Irrep.barψ} V) := by + rw [irrepCoeff_quartic_eq] + exact coeff_quartic_isInvariant + +lemma isInvariant_iff_eq_sum_irrepCoeff {V : EFTLagrangianExclDeriv} : + IsInvariant V ↔ V = irrepCoeff 0 V + irrepCoeff {Irrep.ψ, Irrep.ψ} V + + irrepCoeff {Irrep.barψ, Irrep.barψ} V + + irrepCoeff {Irrep.ψ, Irrep.ψ, Irrep.barψ, Irrep.barψ} V := by + constructor + · intro hV + exact eq_sum_irrepCoeff_of_isInvariant hV + · intro h + rw [h] + apply IsInvariant.add _ irrepCoeff_quadratic_isInvariant + apply IsInvariant.add _ irrepCoeff_barψ_barψ_isInvariant + apply IsInvariant.add irrepCoeff_empty_isInvariant irrepCoeff_ψ_ψ_isInvariant + +lemma isInvariant_iff_eq_sum_coeff {V : EFTLagrangianExclDeriv} : + IsInvariant V ↔ V = coeff 0 V + coeff {.ψ 0, .ψ 1} V + + coeff {.barψ 0, .barψ 1} V + coeff {.ψ 0, .ψ 1, .barψ 0, .barψ 1} V := by + rw [isInvariant_iff_eq_sum_irrepCoeff, irrepCoeff_empty_eq, irrepCoeff_ψ_ψ_eq, + irrepCoeff_barψ_barψ_eq, irrepCoeff_quartic_eq] + +lemma isInvariant_iff_eq_exists {V : EFTLagrangianExclDeriv} : + IsInvariant V ↔ + ∃ c : ℂ, ∃ m0 : ℂ, ∃ m1 : ℂ, ∃ ρ : ℂ, V = c • 1 + m0 • ([ψ 0]ₑ * [ψ 1]ₑ) + + m1 • ([barψ 0]ₑ * [barψ 1]ₑ) + ρ • ([ψ 0]ₑ * [ψ 1]ₑ * [barψ 0]ₑ * [barψ 1]ₑ):= by + rw [isInvariant_iff_eq_sum_coeff] + obtain ⟨c, hc⟩ := coeff_eq_termOfList V (s := 0) (l := []) (by decide) + obtain ⟨m0, hm0⟩ := coeff_eq_termOfList V (s := {.ψ 0, .ψ 1}) (l := [.ψ 0, .ψ 1]) (by decide) + obtain ⟨m1, hm1⟩ := coeff_eq_termOfList V (s := {.barψ 0, .barψ 1}) + (l := [.barψ 0, .barψ 1]) (by decide) + obtain ⟨ρ, hρ⟩ := coeff_eq_termOfList V (s := {.ψ 0, .ψ 1, .barψ 0, .barψ 1}) + (l := [.ψ 0, .ψ 1, .barψ 0, .barψ 1]) (by decide) + rw [hc, hm0, hm1, hρ] + simp [termOfList] + constructor + · intro h + use c, m0, m1, ρ + rw [h] + grind + · rintro ⟨c', m0', m1', ρ', hV⟩ + simp [← mul_assoc] + rw [show [ψ 0]ₑ * [ψ 1]ₑ * [barψ 0]ₑ * [barψ 1]ₑ = + termOfList [.ψ 0, .ψ 1, .barψ 0, .barψ 1] by simp [termOfList]; grind, + show [ψ 0]ₑ * [ψ 1]ₑ = termOfList [.ψ 0, .ψ 1] by simp [termOfList], + show [barψ 0]ₑ * [barψ 1]ₑ = termOfList [.barψ 0, .barψ 1] by simp [termOfList]] at hV ⊢ + rw [hV] at hm0 hρ hm1 hc + simp +decide only [Fin.isValue, map_add, map_smul, coeff_one, ↓reduceIte, smul_zero, + coeff_apply_termOfList, add_zero, termOfList_nil, ne_eq, one_ne_zero, not_false_eq_true, + smul_left_inj] at hm0 hρ hm1 hc + simp_all + +/-! + +## Mass dimension + +-/ + +/-- The finset of all possible field contents of terms with overall mass dimension `n`. + Since every field has mass dimension at least `3 / 2`, a term of mass dimension `n` + contains a bounded number of fields, so this is a computable finset (constructed + through `multisetsOfMassDim`). The defining property is + `mem_allTermsWithMassDimension_iff`. -/ +def allTermsWithMassDimension (n : ℚ) : Finset (Multiset FieldSpecification) := + multisetsOfMassDim massDimension n + +lemma mem_allTermsWithMassDimension_iff (n : ℚ) (s : Multiset FieldSpecification) : + s ∈ allTermsWithMassDimension n ↔ (s.map massDimension).sum = n := + mem_multisetsOfMassDim_iff massDimension_pos + +/-- Clearing denominators: the terms of mass dimension `n` are those whose scaled + (`ℕ`-valued) mass dimensions sum to `2 * n`. The right-hand side reduces in the + kernel, so after rewriting by this lemma membership can be decided by `decide`. -/ +lemma allTermsWithMassDimension_eq_natCast {n : ℚ} {mN : ℕ} (hm : (mN : ℚ) = n * 2) : + allTermsWithMassDimension n = multisetsOfMassDimNat massDimensionNat mN := + multisetsOfMassDim_eq_natCast massDimension_pos (by norm_num) massDimensionNat_cast hm + +example : ({ψ 0, ψ 1} : Multiset FieldSpecification) ∈ allTermsWithMassDimension 3 := by + rw [allTermsWithMassDimension_eq_natCast (mN := 6) (by norm_num)] + decide + +example : ({ψ 0, ψ 1, barψ 0, barψ 1} : Multiset FieldSpecification) ∉ + allTermsWithMassDimension 3 := by + rw [allTermsWithMassDimension_eq_natCast (mN := 6) (by norm_num)] + decide + +/-- The projection of a term of `EFTLagrangianExclDeriv` onto those operators whose + field content has overall mass dimension `n`. -/ +def massDimCoeff (n : ℚ) : EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv := + ∑ s ∈ allTermsWithMassDimension n, coeff s + +lemma massDimCoeff_eq_sum (n : ℚ) (V : EFTLagrangianExclDeriv) : + massDimCoeff n V = ∑ s ∈ allTermsWithMassDimension n, coeff s V := by + simp [massDimCoeff] + +lemma massDimCoeff_termOfList (n : ℚ) (l : List FieldSpecification) : + massDimCoeff n (termOfList l) = + if (Multiset.map massDimension (Multiset.ofList l)).sum = n then termOfList l else 0 := by + simp [massDimCoeff_eq_sum, coeff_apply_termOfList, mem_allTermsWithMassDimension_iff] + +lemma massDimCoeff_termOfList_ofNat (n : ℕ) (l : List FieldSpecification) : + massDimCoeff (n) (termOfList l) = + if (Multiset.map massDimensionNat (Multiset.ofList l)).sum = 2 * n then termOfList l else 0 := by + rw [massDimCoeff_termOfList] + simp + congr 1 + field_simp + simp + constructor + · intro h + exact_mod_cast h + · intro h + exact_mod_cast h + +lemma massDimCoeff_one (n : ℚ) : massDimCoeff n 1 = if n = 0 then 1 else 0 := by + rw [massDimCoeff_eq_sum] + simp only [coeff_one] + rw [Finset.sum_ite_eq'] + refine if_congr ?_ rfl rfl + rw [mem_allTermsWithMassDimension_iff] + simp [eq_comm] + +/-- The mass dimensions of the operators appearing in an effective potential. -/ +def massDimSupport (V : EFTLagrangianExclDeriv) : Finset ℚ := + (support V).image (fun s => (s.map massDimension).sum) + +lemma massDimSupport_add {V W : EFTLagrangianExclDeriv} : + massDimSupport (V + W) ⊆ massDimSupport V ∪ massDimSupport W := by + simp [massDimSupport, ← Finset.image_union] + apply Finset.image_subset_image + exact support_add + +lemma massDimSupport_sub {V W : EFTLagrangianExclDeriv} : + massDimSupport (V - W) ⊆ massDimSupport V ∪ massDimSupport W := by + simp [massDimSupport, ← Finset.image_union] + apply Finset.image_subset_image + exact support_sub + +lemma massDimSupport_one : massDimSupport 1 = {0} := by + simp [support_one, massDimSupport] + +lemma massDimSupport_smul {c : ℂ} {V : EFTLagrangianExclDeriv} : + massDimSupport (c • V) ⊆ massDimSupport V := by + simp [massDimSupport, ] + apply Finset.image_subset_image + exact support_smul c + +lemma massDimSupport_termOfList (l : List FieldSpecification) : + massDimSupport (termOfList l) ⊆ {(Multiset.map massDimension (Multiset.ofList l)).sum} := by + trans ({Multiset.ofList l} : Finset (Multiset FieldSpecification)).image + (fun s => (s.map massDimension).sum) + · apply Finset.image_subset_image + exact support_termOfList_subset l + · simp + +lemma eq_sum_massDimCoeff (V : EFTLagrangianExclDeriv) : + V = ∑ n ∈ massDimSupport V, massDimCoeff n V := by + simp only [massDimSupport, massDimCoeff_eq_sum] + exact eq_sum_fiber_coeff mem_allTermsWithMassDimension_iff V + +def HasMassDimLE (n : ℚ) (V : EFTLagrangianExclDeriv): Prop := + ∀ s ∈ massDimSupport V, s ≤ n + +lemma HasMassDimLE.add {n : ℚ} {V W : EFTLagrangianExclDeriv} (hV : HasMassDimLE n V) + (hW : HasMassDimLE n W) : HasMassDimLE n (V + W) := by + intro s hs + have h1 := massDimSupport_add hs + simp at h1 + rcases h1 with h1 | h1 + · exact hV s h1 + · exact hW s h1 + +lemma HasMassDimLE.sub {n : ℚ} {V W : EFTLagrangianExclDeriv} (hV : HasMassDimLE n V) + (hW : HasMassDimLE n W) : HasMassDimLE n (V - W) := by + intro s hs + have h1 := massDimSupport_sub hs + simp at h1 + rcases h1 with h1 | h1 + · exact hV s h1 + · exact hW s h1 + +lemma HasMassDimLE.smul {n : ℚ} {c : ℂ} {V : EFTLagrangianExclDeriv} (hV : HasMassDimLE n V) : + HasMassDimLE n (c • V) := by + intro s hs + have h1 := massDimSupport_smul hs + exact hV s h1 + +lemma HasMassDimLE.one {n : ℚ} (hn : 0 ≤ n): HasMassDimLE n 1 := by + simp [HasMassDimLE, massDimSupport_one] + exact hn + +lemma HasMassDimLE.termOfList {n : ℚ} {l : List FieldSpecification} + (hl : (Multiset.map massDimension (Multiset.ofList l)).sum ≤ n) : + HasMassDimLE n (termOfList l) := by + intro s hs + have hs' := massDimSupport_termOfList l hs + simp_all + +/-- Off the mass-dimension support the projection vanishes: if no operator of `V` has + mass dimension `q`, then `massDimCoeff q V = 0`. -/ +lemma massDimCoeff_eq_zero_of_not_mem_massDimSupport {q : ℚ} {V : EFTLagrangianExclDeriv} + (h : q ∉ massDimSupport V) : massDimCoeff q V = 0 := by + rw [massDimCoeff_eq_sum] + refine Finset.sum_eq_zero fun s hs => ?_ + rw [mem_allTermsWithMassDimension_iff] at hs + refine coeff_eq_zero_of_not_mem_support fun hsupp => h ?_ + rw [massDimSupport] + exact Finset.mem_image.mpr ⟨s, hsupp, hs⟩ + +lemma eq_sum_of_hasMassDimLE {n : ℕ} {V : EFTLagrangianExclDeriv} (h : HasMassDimLE n V) : + V = ∑ m ∈ Finset.range (2 * n + 1), massDimCoeff (m / (2 : ℚ)) V := by + have hinj : ∀ x ∈ Finset.range (2 * n + 1), ∀ y ∈ Finset.range (2 * n + 1), + (x / (2 : ℚ)) = (y / (2 : ℚ)) → x = y := by + intro x _ y _ hxy + exact_mod_cast (by linarith : (x : ℚ) = y) + have hreindex : (∑ m ∈ Finset.range (2 * n + 1), massDimCoeff (m / (2 : ℚ)) V) + = ∑ q ∈ (Finset.range (2 * n + 1)).image (fun m : ℕ => (m : ℚ) / 2), massDimCoeff q V := + (Finset.sum_image (f := fun q => massDimCoeff q V) hinj).symm + rw [hreindex] + conv_lhs => rw [eq_sum_massDimCoeff V] + refine Finset.sum_subset ?_ (fun q _ hq => massDimCoeff_eq_zero_of_not_mem_massDimSupport hq) + rw [massDimSupport, Finset.image_subset_iff] + intro s hs + have hle : (s.map massDimension).sum ≤ (n : ℚ) := + h _ (by rw [massDimSupport]; exact Finset.mem_image.mpr ⟨s, hs, rfl⟩) + rw [sum_map_massDimension] at hle + refine Finset.mem_image.mpr ⟨3 * s.card, Finset.mem_range.mpr ?_, ?_⟩ + · have h2 : (3 * s.card : ℚ) ≤ 2 * n := by linarith + have : 3 * s.card ≤ 2 * n := by exact_mod_cast h2 + omega + · rw [sum_map_massDimension]; push_cast; ring + +lemma massDimCoeff_eq_zero_of_hasMassDimLE {n : ℕ} {V : EFTLagrangianExclDeriv} + (h : HasMassDimLE n V) (m : ℚ) (hm : n < m) : + massDimCoeff m V = 0 := by + apply massDimCoeff_eq_zero_of_not_mem_massDimSupport + simp [HasMassDimLE] at h + by_contra hn + have hl := h m hn + grind + + +/-- Applying `coeff s` to a mass-dimension projection: it returns `coeff s V` when the field + content `s` has mass dimension `q`, and `0` otherwise (the other coefficients are orthogonal + to `coeff s`). -/ +lemma coeff_massDimCoeff (q : ℚ) (s : Multiset FieldSpecification) (V : EFTLagrangianExclDeriv) : + coeff s (massDimCoeff q V) = if (s.map massDimension).sum = q then coeff s V else 0 := by + rw [massDimCoeff_eq_sum, map_sum] + split_ifs with h + · rw [Finset.sum_eq_single s (fun t _ htn => coeff_coeff_eq_zero_of_diff (Ne.symm htn) V) + (fun hns => absurd ((mem_allTermsWithMassDimension_iff q s).mpr h) hns)] + exact coeff_coeff_self V + · refine Finset.sum_eq_zero fun t ht => ?_ + rw [mem_allTermsWithMassDimension_iff] at ht + exact coeff_coeff_eq_zero_of_diff (by rintro rfl; exact h ht) V + +lemma hasMassDimLE_iff_eq_sum {n : ℕ} {V : EFTLagrangianExclDeriv} : + HasMassDimLE n V ↔ V = ∑ m ∈ Finset.range (2 * n + 1), massDimCoeff (m / (2 : ℚ)) V := by + refine ⟨eq_sum_of_hasMassDimLE, fun hV => ?_⟩ + intro q hq + rw [massDimSupport, Finset.mem_image] at hq + obtain ⟨s, hs, rfl⟩ := hq + rw [mem_support_iff] at hs + have hcoeff : coeff s V + = ∑ m ∈ Finset.range (2 * n + 1), + if (s.map massDimension).sum = (m : ℚ) / 2 then coeff s V else 0 := by + conv_lhs => rw [hV] + rw [map_sum] + simp_rw [coeff_massDimCoeff] + have hex : ∃ m ∈ Finset.range (2 * n + 1), (s.map massDimension).sum = (m : ℚ) / 2 := by + by_contra hcon + push Not at hcon + exact hs (by rw [hcoeff]; exact Finset.sum_eq_zero fun m hm => if_neg (hcon m hm)) + obtain ⟨m, hm, hqm⟩ := hex + rw [Finset.mem_range] at hm + rw [hqm] + have hmn : (m : ℚ) ≤ 2 * (n : ℚ) := by exact_mod_cast (show m ≤ 2 * n from by omega) + linarith + +/-! + +## Conjugation + +-/ + +/-- The conjugate of a coefficient. -/ +def conjCoeffMap (s : Multiset FieldSpecification) (V : EFTLagrangianExclDeriv) : + EFTLagrangianExclDeriv := + let c := Classical.choose (coeff_eq_termOfList V (s := s) (l := s.toList) (by simp)) + starRingEnd ℂ c • termOfList (s.toList.map conjugate).reverse + +lemma conjCoeffMap_of_eq_termOfList (s : Multiset FieldSpecification) (l : List FieldSpecification) + (V : EFTLagrangianExclDeriv) (c : ℂ) (hl : Multiset.ofList l = s) + (h : coeff s V = c • termOfList l) : + conjCoeffMap s V = starRingEnd ℂ c • termOfList (l.map conjugate).reverse := by + obtain ⟨b, hb1, hb2⟩ := termOfList_perm_neq_zero (l1 := s.toList) (l2 := l) + (by subst hl; rw [← Multiset.coe_eq_coe ]; simp) + let c' := Classical.choose (coeff_eq_termOfList V (s := s) (l := s.toList) (by simp)) + have hc' : coeff s V = c' • termOfList s.toList := + Classical.choose_spec (coeff_eq_termOfList V (s := s) (l := s.toList) (by simp)) + change starRingEnd ℂ c' • termOfList (s.toList.map conjugate).reverse = _ + rw [h] at hc' + have hx1 := termOfList_reverse_eq_of_eq (termOfList_conjugate_eq_of_eq hb1) + rw [hx1, smul_smul] + rw [hb1, smul_smul] at hc' + have hx2 : (c - c' * b) • termOfList l = 0 := by + simp [sub_smul, hc'] + simp at hx2 + rcases hx2 with (h0 | h1) + · congr + grind + · rw [termOfList_reverse_zero_of_zero (termOfList_conjugate_zero_of_zero h1)] + simp + +@[simp] +lemma conjCoeffMap_add (s : Multiset FieldSpecification) (V W : EFTLagrangianExclDeriv) : + conjCoeffMap s (V + W) = conjCoeffMap s V + conjCoeffMap s W := by + obtain ⟨l, c, hV, hl⟩ := coeff_eq_exists_termOfList s V + obtain ⟨d, hW⟩ := coeff_eq_termOfList W hl + have hVW : coeff s (V + W) = (c + d) • termOfList l := by + simp [hV, hW, add_smul] + rw [conjCoeffMap_of_eq_termOfList s l (V + W) (c + d) hl hVW, + conjCoeffMap_of_eq_termOfList s l V c hl hV, conjCoeffMap_of_eq_termOfList s l W d hl hW] + simp [add_smul] + +@[simp] +lemma conjCoeff_smul (s : Multiset FieldSpecification) (c : ℂ) (V : EFTLagrangianExclDeriv) : + conjCoeffMap s (c • V) = starRingEnd ℂ c • conjCoeffMap s V := by + obtain ⟨l, d, hV, hl⟩ := coeff_eq_exists_termOfList s V + have h : coeff s (c • V) = (c * d) • termOfList l := by + simp [hV, smul_smul] + rw [conjCoeffMap_of_eq_termOfList s l (c • V) (c * d) hl h, + conjCoeffMap_of_eq_termOfList s l V d hl hV] + simp [smul_smul] + +def conjCoeff (s : Multiset FieldSpecification) : EFTLagrangianExclDeriv →ₛₗ[starRingEnd ℂ] EFTLagrangianExclDeriv where + toFun := conjCoeffMap s + map_add' := conjCoeffMap_add s + map_smul' := conjCoeff_smul s + +lemma conjCoeff_of_eq_termOfList (s : Multiset FieldSpecification) (l : List FieldSpecification) + (V : EFTLagrangianExclDeriv) (c : ℂ) (hl : Multiset.ofList l = s) + (h : coeff s V = c • termOfList l) : + conjCoeff s V = starRingEnd ℂ c • termOfList (l.map conjugate).reverse := by + simp [conjCoeff, conjCoeffMap_of_eq_termOfList s l V c hl h] + +/-- The conjugate coefficient vanishes on field contents outside the support, since there + the coefficient itself is zero. -/ +lemma conjCoeff_eq_zero_of_not_mem_support {s : Multiset FieldSpecification} + {V : EFTLagrangianExclDeriv} (h : s ∉ support V) : conjCoeff s V = 0 := by + rw [conjCoeff_of_eq_termOfList s s.toList V 0 (by simp) + (by simp [coeff_eq_zero_of_not_mem_support h])] + simp + +lemma conjCoeff_termOfList (s : Multiset FieldSpecification) (l : List FieldSpecification) : + conjCoeff s (termOfList l) = if Multiset.ofList l = s then + termOfList (l.map conjugate).reverse else 0 := by + split_ifs with h + · have h0 : coeff s (termOfList l) = (1 : ℂ) • termOfList l := by + simp [coeff_apply_termOfList, h] + rw [conjCoeff_of_eq_termOfList s l (termOfList l) 1 h h0] + simp + · apply conjCoeff_eq_zero_of_not_mem_support + simp [mem_support_termOfList_iff] + grind + +def conjugate : EFTLagrangianExclDeriv →ₛₗ[starRingEnd ℂ] EFTLagrangianExclDeriv where + toFun := fun V => ∑ s ∈ support V, conjCoeff s V + map_add' := by + intro V W + rw [Finset.sum_subset support_add + (fun s _ hs => conjCoeff_eq_zero_of_not_mem_support hs), + Finset.sum_subset (Finset.subset_union_left (s₂ := support W)) + (fun s _ hs => conjCoeff_eq_zero_of_not_mem_support hs), + Finset.sum_subset (Finset.subset_union_right (s₁ := support V)) + (fun s _ hs => conjCoeff_eq_zero_of_not_mem_support hs)] + simp [map_add, Finset.sum_add_distrib] + map_smul' := by + intro c V + rw [Finset.sum_subset (support_smul c) + (fun s _ hs => conjCoeff_eq_zero_of_not_mem_support hs)] + simp [map_smulₛₗ, Finset.smul_sum] + +lemma conjugate_termOfList (l : List FieldSpecification) : + conjugate (termOfList l) = termOfList (l.map .conjugate).reverse := by + simp [conjugate, conjCoeff_termOfList, mem_support_termOfList_iff] + exact fun h => (termOfList_reverse_zero_of_zero (termOfList_conjugate_zero_of_zero h)).symm + +@[simp] +lemma conjugate_one : conjugate 1 = 1 := by + simp [← termOfList_nil, conjugate_termOfList] + +/-! + +## IsReal condition + +-/ + +def IsReal (V : EFTLagrangianExclDeriv) : Prop := conjugate V = V + +/-- The lemma expressing the form of an element of `EFTLagrangianExclDeriv`, if it is both + invariant under the Lorentz group and is real. + + This expresses the EFT lagrangian in terms of the Majorana mass trem. -/ +lemma isInvariant_and_isReal_iff_eq_exists {V : EFTLagrangianExclDeriv} : + IsInvariant V ∧ IsReal V ↔ ∃ c : ℝ, ∃ m0 : ℂ, ∃ ρ : ℝ, V = (c : ℂ) • 1 + m0 • ([ψ 0]ₑ * [ψ 1]ₑ) - + starRingEnd ℂ m0 • ([barψ 0]ₑ * [barψ 1]ₑ) + + (ρ : ℂ) • ([ψ 0]ₑ * [ψ 1]ₑ * [barψ 0]ₑ * [barψ 1]ₑ) := by + have h_quartic : termOfList [ψ 1, ψ 0, barψ 1, barψ 0] = termOfList [ψ 0, ψ 1, barψ 0, barψ 1] := by + simp [termOfList, toEFTLagrangianExclDeriv_mul_anti_commute (barψ 0) (barψ 1)] + simp [← mul_assoc, toEFTLagrangianExclDeriv_mul_anti_commute (ψ 0) (ψ 1)] + constructor + · rintro ⟨hi, hr⟩ + rw [isInvariant_iff_eq_exists] at hi + obtain ⟨c, m0, m1, ρ, hV⟩ := hi + simp [← termOfList_singleton, ← termOfList_append] at hV ⊢ + simp [IsReal, hV, conjugate_termOfList] at hr + have h0 := congr_arg (coeff 0) hr + have h2 := congr_arg (coeff {.barψ 0, .barψ 1}) hr + have h3 := congr_arg (coeff {.ψ 0, .ψ 1, .barψ 0, .barψ 1}) hr + simp +decide [coeff_apply_termOfList, coeff_one] at h0 h2 h3 + obtain ⟨c', rfl⟩ := Complex.conj_eq_iff_real.mp h0 + refine ⟨c', m0, ρ.re, hV.trans ?_⟩ + have hx : m1 • termOfList [barψ 0, barψ 1] = + -(starRingEnd ℂ m0 • termOfList [barψ 0, barψ 1]) := by + rw [← h2] + simp [termOfList, FieldSpecification.conjugate, + toEFTLagrangianExclDeriv_mul_anti_commute (barψ 0)] + have hρ : ρ • termOfList [ψ 0, ψ 1, barψ 0, barψ 1] = + (ρ.re : ℂ) • termOfList [ψ 0, ψ 1, barψ 0, barψ 1] := by + simp [FieldSpecification.conjugate, h_quartic] at h3 + rcases smul_eq_zero.mp (show (starRingEnd ℂ ρ - ρ) • + termOfList [ψ 0, ψ 1, barψ 0, barψ 1] = 0 by simp [sub_smul, h3]) with h | h + · obtain ⟨ρ', rfl⟩ := Complex.conj_eq_iff_real.mp (sub_eq_zero.mp h) + simp + · simp [h] + rw [hx, hρ] + simp [sub_eq_add_neg] + · rintro ⟨c, m0, ρ, hV⟩ + constructor + · rw [isInvariant_iff_eq_exists] + use (c : ℂ), m0, - starRingEnd ℂ m0, ρ + rw [hV] + simp + abel + · simp only [← termOfList_singleton, ← termOfList_append] at hV + subst hV + simp [IsReal, -coe_smul, Fin.isValue, map_add, map_sub, LinearMap.map_smulₛₗ, + RingHomCompTriple.comp_apply, RingHom.id_apply, conjugate_termOfList, + FieldSpecification.conjugate, h_quartic] + simp [termOfList, toEFTLagrangianExclDeriv_mul_anti_commute (barψ 0) (barψ 1), + toEFTLagrangianExclDeriv_mul_anti_commute (ψ 0) (ψ 1)] + abel + +/-- The lemma expressing the form of an element of `EFTLagrangianExclDeriv`, if it is + invariant under the Lorentz group and is real, and has mass dimension at most `4`. + + This expresses the EFT lagrangian in terms of the Majorana mass trem. -/ +lemma isInvariant_isReal_hasMassDimLE_four_iff_eq_exists {V : EFTLagrangianExclDeriv} : + IsInvariant V ∧ IsReal V ∧ HasMassDimLE 4 V ↔ ∃ c : ℝ, ∃ m0 : ℂ, + V = (c : ℂ) • 1 + m0 • ([ψ 0]ₑ * [ψ 1]ₑ) - starRingEnd ℂ m0 • ([barψ 0]ₑ * [barψ 1]ₑ) := by + constructor + · rintro ⟨hi, hr, hm⟩ + obtain ⟨c, m0, ρ, hV⟩ := (isInvariant_and_isReal_iff_eq_exists.mp ⟨hi, hr⟩) + use c, m0 + simp only [← termOfList_singleton, ← termOfList_append] at hV ⊢ + rw [hV] + simp only [Fin.isValue, add_eq_left, smul_eq_zero] + have hmass := massDimCoeff_eq_zero_of_hasMassDimLE hm (6 : ℕ) (by norm_num) + have h0 := massDimCoeff_termOfList_ofNat (n := 6) + simp only [Nat.cast_ofNat, massDimensionNat_eq, Multiset.map_coe, List.map_const', + Multiset.sum_coe, List.sum_replicate, smul_eq_mul, Nat.reduceMul] at h0 + simp +decide [hV, h0, massDimCoeff_one] at hmass + rcases hmass with rfl | hmass + · simp + · simp [hmass] + · rintro ⟨c, m0, hV⟩ + rw [← and_assoc] + constructor + · rw [isInvariant_and_isReal_iff_eq_exists] + use c, m0, 0 + simp [hV] + · simp only [← termOfList_singleton, ← termOfList_append] at hV + rw [hV] + refine HasMassDimLE.sub + (HasMassDimLE.add (HasMassDimLE.smul (HasMassDimLE.one ?_)) + (HasMassDimLE.smul (HasMassDimLE.termOfList ?_))) + (HasMassDimLE.smul (HasMassDimLE.termOfList ?_)) <;> norm_num + +end EFTLagrangianExclDeriv + +end +end Fermion diff --git a/Physlib/Particles/WessZumino/EFTLagrangianExclDeriv.lean b/Physlib/Particles/WessZumino/EFTLagrangianExclDeriv.lean new file mode 100644 index 000000000..2143bf8fd --- /dev/null +++ b/Physlib/Particles/WessZumino/EFTLagrangianExclDeriv.lean @@ -0,0 +1,662 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith, Jinzheng Li, Nathaneal Sajan +-/ +module + +public import Physlib.Relativity.Fermions.Weyl.Metric +public import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation +public import Mathlib.LinearAlgebra.ExteriorAlgebra.Basis +public import Physlib.Mathematics.ConjModule +public import Physlib.Mathematics.MultisetsOfMassDim +public import Mathlib.RingTheory.GradedAlgebra.Basic +public import Mathlib.LinearAlgebra.SymmetricAlgebra.Basic +public import Mathlib.RingTheory.TensorProduct.Basic +public import Mathlib.RingTheory.TensorProduct.Maps +public import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction +public import Mathlib.LinearAlgebra.SymmetricAlgebra.Basis +public import Mathlib.Algebra.MvPolynomial.PDeriv +/-! + +# The Wess-Zumino EFT Lagrangian without derivatives + +## i. Overview + +The Wess-Zumino theory is a simple field theory consisting +of a single left-handed Weyl fermion and a single complex scalar field. +Sometimes the complex scalar field is replaced by a pair of real scalar fields. + +The theory is of physical interest, because it simple example of a theory +permitting a supersymmetry. In this file we don't consider the supersymmetric nature +of the theory. + +-/ + +@[expose] public section + +namespace WessZumino +noncomputable section + +open Module Matrix +open MatrixGroups +open Complex +open TensorProduct +open CategoryTheory.MonoidalCategory +open Fermion + +/-! + +## Field specification + +-/ + +inductive ComplexScalars + | φ : ComplexScalars + | barφ : ComplexScalars +deriving DecidableEq + +inductive Fermions + | ψ (α : Fin 2) : Fermions + | barψ (α : Fin 2) : Fermions +deriving DecidableEq + +inductive FieldGenerators + | cScalar (_ : ComplexScalars) : FieldGenerators + | fermion (_ : Fermions) : FieldGenerators +deriving DecidableEq + +def FieldGenerators.IsFermion : FieldGenerators → Bool + | .cScalar _ => False + | .fermion _ => True + +@[simp] +lemma FieldGenerators.cScalar_isFermion (ϕ : ComplexScalars) : + (cScalar ϕ).IsFermion = False := by simp [IsFermion] + +@[simp] +lemma FieldGenerators.fermion_isFermion (ϕ : Fermions) : + (fermion ϕ).IsFermion = True := by simp [IsFermion] + +def FieldGenerators.IsBoson : FieldGenerators → Bool + | .cScalar _ => True + | .fermion _ => False + +@[simp] +lemma FieldGenerators.cScalar_isBoson (ϕ : ComplexScalars) : + (cScalar ϕ).IsBoson = True := by simp [IsBoson] + +@[simp] +lemma FieldGenerators.fermion_isBoson (ϕ : Fermions) : + (fermion ϕ).IsBoson = False := by simp [IsBoson] + + +/-! + +## A. The EFT lagrangian without derivatives + +-/ + +/-- The algebra corresponding to the EFT lagrangian excluding + derivative terms for the Wess-Zumino theory: the free supercommutative algebra + on the bosonic and fermionic generators, i.e. the tensor product of the symmetric + algebra on the bosonic duals with the exterior algebra on the fermionic duals. -/ +abbrev EFTLagrangianExclDeriv : Type := + -- bosonic part of the lagrangian + SymmetricAlgebra ℂ (Module.Dual ℂ (ℂ × ConjModule ℂ)) ⊗[ℂ] + -- fermionic part of the lagrangian + ExteriorAlgebra ℂ (Module.Dual ℂ (LeftHandedWeyl × ConjModule LeftHandedWeyl)) + +namespace EFTLagrangianExclDeriv + +/-! + +## The elements of the EFT generated by the field generators + +Every element of the Field generators gives an element in the +type of EFT lagragians. + +-/ +/-- The elements of `EFTLagrangianExclDeriv` associated with + the `FieldGenerators`. -/ +def ofFieldGenerators : FieldGenerators → EFTLagrangianExclDeriv + | .cScalar .φ => SymmetricAlgebra.ι ℂ _ + (((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inl 0)) + ⊗ₜ 1 + | .cScalar .barφ => SymmetricAlgebra.ι ℂ _ + (((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inr 0)) + ⊗ₜ 1 + | .fermion (.ψ α) => 1 ⊗ₜ ExteriorAlgebra.ι ℂ + ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis (Sum.inl α)) + | .fermion (.barψ α) => 1 ⊗ₜ ExteriorAlgebra.ι ℂ + ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis (Sum.inr α)) + +scoped notation "[" v "]ₐ" => ofFieldGenerators v +scoped notation "[" v "]ₛ" => ofFieldGenerators (FieldGenerators.cScalar v) +scoped notation "[" v "]ₑ" => ofFieldGenerators (FieldGenerators.fermion v) + +lemma ofFieldGenerators_cScalar_exists (ϕ : ComplexScalars) : + ∃ x, [ϕ]ₛ = SymmetricAlgebra.ι ℂ _ x ⊗ₜ 1 := by + match ϕ with + | .φ => exact + ⟨((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inl 0), rfl⟩ + | .barφ => exact + ⟨((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inr 0), rfl⟩ + +lemma ofFieldGenerators_fermion_exists (ψ : Fermions) : + ∃ x, [ψ]ₑ = 1 ⊗ₜ ExteriorAlgebra.ι ℂ x := by + match ψ with + | .ψ α => exact + ⟨((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis (Sum.inl α)), rfl⟩ + | .barψ α => exact + ⟨((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis (Sum.inr α)), rfl⟩ + +lemma cScalar_comm_cScalar (φ₁ φ₂ : ComplexScalars) : + [φ₁]ₛ * [φ₂]ₛ = [φ₂]ₛ * [φ₁]ₛ := by + obtain ⟨x₁, h1⟩ := ofFieldGenerators_cScalar_exists φ₁ + obtain ⟨x₂, h2⟩ := ofFieldGenerators_cScalar_exists φ₂ + simp [h1, h2, mul_comm] + +lemma cScalar_comm_fermion (ϕ : ComplexScalars) (ψ : Fermions) : + [ϕ]ₛ * [ψ]ₑ = [ψ]ₑ * [ϕ]ₛ := by + obtain ⟨x₁, h1⟩ := ofFieldGenerators_cScalar_exists ϕ + obtain ⟨x₂, h2⟩ := ofFieldGenerators_fermion_exists ψ + simp [h1, h2, mul_comm] + +lemma cScalar_comm (V : EFTLagrangianExclDeriv) (ϕ : ComplexScalars) : + [ϕ]ₛ * V = V * [ϕ]ₛ := by + obtain ⟨x, h⟩ := ofFieldGenerators_cScalar_exists ϕ + induction V using TensorProduct.induction_on with + | zero => simp + | tmul a b => simp [h, mul_comm] + | add x y hx hy => simp [mul_add, add_mul, hx, hy] + +lemma fermion_comm_cScalar (ψ : Fermions) (ϕ : ComplexScalars) : + [ψ]ₑ * [ϕ]ₛ = [ϕ]ₛ * [ψ]ₑ := by + obtain ⟨x₁, h1⟩ := ofFieldGenerators_fermion_exists ψ + obtain ⟨x₂, h2⟩ := ofFieldGenerators_cScalar_exists ϕ + simp [h1, h2] + +lemma fermion_anticomm_fermion (ψ₁ ψ₂ : Fermions) : + [ψ₁]ₑ * [ψ₂]ₑ = - [ψ₂]ₑ * [ψ₁]ₑ := by + obtain ⟨x₁, h1⟩ := ofFieldGenerators_fermion_exists ψ₁ + obtain ⟨x₂, h2⟩ := ofFieldGenerators_fermion_exists ψ₂ + rw [h1, h2, ← TensorProduct.tmul_neg, Algebra.TensorProduct.tmul_mul_tmul, + Algebra.TensorProduct.tmul_mul_tmul] + congr 1 + rw [neg_mul, eq_neg_iff_add_eq_zero] + exact ExteriorAlgebra.ι_add_mul_swap x₁ x₂ + +@[simp] +lemma fermion_mul_self (ψ : Fermions) : [ψ]ₑ * [ψ]ₑ = 0 := by + obtain ⟨x, h⟩ := ofFieldGenerators_fermion_exists ψ + simp [h] + +lemma ofFieldGenerators_comm (ϕ₁ ϕ₂ : FieldGenerators) : + ∃ c : ℂ, [ϕ₁]ₐ * [ϕ₂]ₐ = c • [ϕ₂]ₐ * [ϕ₁]ₐ ∧ (c = 1 ∨ c = -1) := by + match ϕ₁, ϕ₂ with + | .cScalar φ₁, .cScalar φ₂ => exact ⟨1, by simp [cScalar_comm_cScalar]⟩ + | .cScalar _, .fermion ψ => exact ⟨1, by simp [cScalar_comm_fermion]⟩ + | .fermion ψ, .cScalar _ => exact ⟨1, by simp [fermion_comm_cScalar]⟩ + |.fermion ψ₁, .fermion ψ₂ => + exact ⟨-1, by rw [fermion_anticomm_fermion]; abel, by simp⟩ + +/-! + +## The elements generated by lists of field generators + +-/ + +/-- The element of `EFTLagrangianExclDeriv` generated from a list of field generators. -/ +def termOfList (l : List FieldGenerators) : EFTLagrangianExclDeriv := + (l.map ofFieldGenerators).prod + +lemma termOfList_cons (ψ : FieldGenerators) (l : List FieldGenerators) : + termOfList (ψ :: l) = [ψ]ₐ * termOfList l := by simp [termOfList] + +lemma termOfList_nil : termOfList [] = 1 := by simp [termOfList] + +lemma termOfList_append (l1 l2 : List FieldGenerators) : + termOfList (l1 ++ l2) = termOfList l1 * termOfList l2 := by + simp [termOfList] + +lemma termOfList_perm {l1 l2 : List FieldGenerators} (h : l1.Perm l2) : + ∃ c : ℂ, termOfList l1 = c • termOfList l2 ∧ (c = 1 ∨ c = -1) := by + induction h with + | nil => exact ⟨1, by simp⟩ + | cons x _ ih => + obtain ⟨c, hc1, hc2⟩ := ih + exact ⟨c, by rw [termOfList_cons, termOfList_cons, hc1, mul_smul_comm], hc2⟩ + | swap x y l => + obtain ⟨c, hc1, hc2⟩ := ofFieldGenerators_comm y x + refine ⟨c, ?_⟩ + rw [termOfList_cons, termOfList_cons, termOfList_cons, termOfList_cons, ← mul_assoc] + simp [hc1, mul_assoc, smul_mul_assoc] + exact hc2 + | trans _ _ ih1 ih2 => + obtain ⟨c1, hc1, hc1'⟩ := ih1 + obtain ⟨c2, hc2, hc2'⟩ := ih2 + exact ⟨c1 * c2, by rw [hc1, hc2, smul_smul], by grind⟩ + +lemma fermion_mul_termOfList_of_mem (ψ : Fermions) (l : List FieldGenerators) + (hψ : .fermion ψ ∈ l) : [ψ]ₑ * termOfList l = 0 := by + induction l with + | nil => simp at hψ + | cons β t ih => + rcases List.mem_cons.mp hψ with rfl | ha + · simp [termOfList_cons, ← mul_assoc] + · obtain ⟨c, hc1, hc2⟩ := ofFieldGenerators_comm (.fermion ψ) β + simp [termOfList_cons, ← mul_assoc, hc1] + simp [mul_assoc, ih ha] + +lemma termOfList_filter_isBoson_comm (l : List FieldGenerators) (V : EFTLagrangianExclDeriv) : + termOfList (l.filter FieldGenerators.IsBoson) * V = + V * termOfList (l.filter FieldGenerators.IsBoson) := by + induction l with + | nil => simp [termOfList] + | cons ψ t ih => + match ψ with + | .cScalar ϕ => + simp [termOfList_cons, cScalar_comm, mul_assoc] + simp [← mul_assoc, ih] + | .fermion ψ => simpa using ih + +lemma termOfList_eq_isBoson_mul_isFermion (l : List FieldGenerators) : + termOfList l = termOfList (l.filter FieldGenerators.IsBoson) * + termOfList (l.filter FieldGenerators.IsFermion) := by + induction l with + | nil => simp [termOfList] + | cons ψ t ih => + match ψ with + | .cScalar ϕ => simp [termOfList_cons, ih, mul_assoc] + | .fermion ψ => + simp [termOfList_cons, ih, ← mul_assoc, termOfList_filter_isBoson_comm] + simp [mul_assoc, termOfList_filter_isBoson_comm] + +lemma termOfList_reverse_eq_of_eq {l1 l2 : List FieldGenerators} {c : ℂ} + (h : termOfList l1 = c • termOfList l2) : + termOfList l1.reverse = c • termOfList l2.reverse := by + let r : EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv := + TensorProduct.map LinearMap.id CliffordAlgebra.reverse + have hmul : ∀ x y : EFTLagrangianExclDeriv, r (x * y) = r y * r x := by + intro x y + induction x using TensorProduct.induction_on with + | zero => simp + | tmul a b => + induction y using TensorProduct.induction_on with + | zero => simp + | tmul a' b' => + simp [r, CliffordAlgebra.reverse.map_mul, mul_comm] + | add y₁ y₂ h₁ h₂ => simp [mul_add, add_mul, h₁, h₂] + | add x₁ x₂ h₁ h₂ => simp [mul_add, add_mul, h₁, h₂] + have hgen : ∀ ψ : FieldGenerators, r [ψ]ₐ = [ψ]ₐ := by + intro ψ + match ψ with + | .cScalar ϕ => + obtain ⟨x, hx⟩ := ofFieldGenerators_cScalar_exists ϕ + simp [r, hx] + | .fermion ψ => + obtain ⟨x, hx⟩ := ofFieldGenerators_fermion_exists ψ + simp [r, hx, CliffordAlgebra.reverse_ι] + have hf : ∀ l : List FieldGenerators, r (termOfList l) = termOfList l.reverse := by + intro l + induction l with + | nil => simp [r, termOfList_nil, Algebra.TensorProduct.one_def] + | cons ψ t ih => + rw [termOfList_cons, hmul, ih, hgen, List.reverse_cons, termOfList_append] + simp [termOfList] + rw [← hf, ← hf, h, map_smul] + +/-- The elements of type `termOfList` span `EFTLagrangianExclDeriv`. -/ +lemma mem_termOfList_span (V : EFTLagrangianExclDeriv) : + V ∈ Submodule.span ℂ (Set.range termOfList) := by + have hmul_mem : ∀ x y : EFTLagrangianExclDeriv, + x ∈ Submodule.span ℂ (Set.range termOfList) → + y ∈ Submodule.span ℂ (Set.range termOfList) → + x * y ∈ Submodule.span ℂ (Set.range termOfList) := fun x y hx hy => by + have h := Submodule.mul_mem_mul hx hy + rw [Submodule.span_mul_span] at h + refine Submodule.span_mono ?_ h + rintro _ ⟨_, ⟨l1, rfl⟩, _, ⟨l2, rfl⟩, rfl⟩ + exact ⟨l1 ++ l2, termOfList_append l1 l2⟩ + have hgen : ∀ g : FieldGenerators, [g]ₐ ∈ Submodule.span ℂ (Set.range termOfList) := + fun g => Submodule.subset_span ⟨[g], by simp [termOfList]⟩ + induction V using TensorProduct.induction_on with + | zero => exact Submodule.zero_mem _ + | add x y hx hy => exact Submodule.add_mem _ hx hy + | tmul a b => + -- The bosonic factor: `a ⊗ₜ 1` lies in the span. + have h1 : (a ⊗ₜ[ℂ] 1 : EFTLagrangianExclDeriv) ∈ + Submodule.span ℂ (Set.range termOfList) := by + induction a using SymmetricAlgebra.induction with + | algebraMap c => + have : (algebraMap ℂ _ c ⊗ₜ[ℂ] 1 : EFTLagrangianExclDeriv) = c • termOfList [] := by + simp [termOfList, Algebra.TensorProduct.one_def, Algebra.algebraMap_eq_smul_one, + TensorProduct.smul_tmul'] + rw [this] + exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨[], rfl⟩) + | ι x => + rw [← Basis.sum_repr + (((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis) x, + map_sum, TensorProduct.sum_tmul] + refine Submodule.sum_mem _ fun i _ => ?_ + rw [map_smul, ← TensorProduct.smul_tmul'] + refine Submodule.smul_mem _ _ ?_ + obtain (i | i) := i <;> fin_cases i + · exact hgen (.cScalar .φ) + · exact hgen (.cScalar .barφ) + | mul a₁ a₂ h₁ h₂ => simpa using hmul_mem _ _ h₁ h₂ + | add a₁ a₂ h₁ h₂ => rw [TensorProduct.add_tmul]; exact Submodule.add_mem _ h₁ h₂ + -- The fermionic factor: `1 ⊗ₜ b` lies in the span. + have h2 : (1 ⊗ₜ[ℂ] b : EFTLagrangianExclDeriv) ∈ + Submodule.span ℂ (Set.range termOfList) := by + induction b using ExteriorAlgebra.induction with + | algebraMap c => + have : (1 ⊗ₜ[ℂ] algebraMap ℂ _ c : EFTLagrangianExclDeriv) = c • termOfList [] := by + simp [termOfList, Algebra.TensorProduct.one_def, Algebra.algebraMap_eq_smul_one, + TensorProduct.tmul_smul] + rw [this] + exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨[], rfl⟩) + | ι x => + rw [← Basis.sum_repr ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis) x, + map_sum, TensorProduct.tmul_sum] + refine Submodule.sum_mem _ fun i _ => ?_ + rw [map_smul, TensorProduct.tmul_smul] + refine Submodule.smul_mem _ _ ?_ + obtain (α | α) := i + · exact hgen (.fermion (.ψ α)) + · exact hgen (.fermion (.barψ α)) + | mul b₁ b₂ h₁ h₂ => simpa using hmul_mem _ _ h₁ h₂ + | add b₁ b₂ h₁ h₂ => rw [TensorProduct.tmul_add]; exact Submodule.add_mem _ h₁ h₂ + simpa using hmul_mem _ _ h1 h2 + +/-! + +## The coefficent associated with a multiset of field generators + + + +The below is AI slop, but it shows a useful way od defining the coefficent. + +-/ + +def CoeffSubmodule (s : Multiset FieldGenerators) : Submodule ℂ EFTLagrangianExclDeriv := + Submodule.span ℂ (termOfList '' {l | Multiset.ofList l = s}) + +instance : SetLike.GradedMonoid CoeffSubmodule where + one_mem := by simp [CoeffSubmodule, termOfList_nil] + mul_mem s1 s2 V1 V2 hV1 hV2 := by + have h := Submodule.mul_mem_mul hV1 hV2 + rw [CoeffSubmodule, CoeffSubmodule, Submodule.span_mul_span] at h + refine Submodule.span_mono ?_ h + rintro _ ⟨_, ⟨l1, hl1, rfl⟩, _, ⟨l2, hl2, rfl⟩, rfl⟩ + exact ⟨l1 ++ l2, by subst hl1; subst hl2; rfl, termOfList_append l1 l2⟩ + +open DirectSum + +namespace CoeffSubmodule + + +/-- Transport `DirectSum.of` along an equality of degrees: two homogeneous components with + equal degrees and equal underlying values are equal. -/ +lemma of_eq {s t : Multiset FieldGenerators} (h : s = t) + {x : CoeffSubmodule s} {y : CoeffSubmodule t} + (hxy : (x : EFTLagrangianExclDeriv) = y) : + DirectSum.of (fun u => CoeffSubmodule u) s x = DirectSum.of (fun u => CoeffSubmodule u) t y := by + subst h + exact congrArg _ (Subtype.ext hxy) + +/-- The class of `termOfList l` in the direct sum of the coefficient submodules, placed + in degree `↑l`. Note that the membership proof is definitional. -/ +def ofList (l : List FieldGenerators) : ⨁ s, CoeffSubmodule s := + DirectSum.of (fun s => CoeffSubmodule s) ↑l + ⟨termOfList l, Submodule.subset_span ⟨l, rfl, rfl⟩⟩ + +lemma ofList_nil : ofList [] = 1 := by + simp [ofList, termOfList_nil] + rfl + +lemma ofList_append (l₁ l₂ : List FieldGenerators) : + ofList (l₁ ++ l₂) = ofList l₁ * ofList l₂ := by + rw [ofList, ofList, ofList, DirectSum.of_mul_of] + exact of_eq rfl (by rw [SetLike.coe_gMul]; exact termOfList_append l₁ l₂) + + +/-- The image of a generator in the direct sum of the coefficient submodules, + placed in degree `{g}`. -/ +def ofGenerator (g : FieldGenerators) : ⨁ s, CoeffSubmodule s := ofList [g] + +lemma ofGenerator_comm {g₁ g₂ : FieldGenerators} (h : [g₁]ₐ * [g₂]ₐ = [g₂]ₐ * [g₁]ₐ) : + ofGenerator g₁ * ofGenerator g₂ = ofGenerator g₂ * ofGenerator g₁ := by + rw [ofGenerator, ofGenerator, ← ofList_append, ← ofList_append] + exact of_eq (Multiset.cons_swap g₁ g₂ 0) (by simp [termOfList, h]) + +lemma fermion_mul_fermion_add_swap (ψ₁ ψ₂ : Fermions) : + [ψ₁]ₑ * [ψ₂]ₑ + [ψ₂]ₑ * [ψ₁]ₑ = 0 := by + obtain ⟨x₁, h1⟩ := ofFieldGenerators_fermion_exists ψ₁ + obtain ⟨x₂, h2⟩ := ofFieldGenerators_fermion_exists ψ₂ + rw [h1, h2, Algebra.TensorProduct.tmul_mul_tmul, Algebra.TensorProduct.tmul_mul_tmul, + ← TensorProduct.tmul_add] + simp + +lemma ofList_eq_zero {l : List FieldGenerators} (h : termOfList l = 0) : ofList l = 0 := by + have hx : (⟨termOfList l, Submodule.subset_span ⟨l, rfl, rfl⟩⟩ : CoeffSubmodule ↑l) = 0 := + Subtype.ext h + rw [ofList, hx, map_zero] + +/-- Two `termOfList` classes with the same field content sum to zero as soon as the + underlying terms do. -/ +lemma ofList_add_ofList {l₁ l₂ : List FieldGenerators} + (hp : (↑l₂ : Multiset FieldGenerators) = ↑l₁) + (h : termOfList l₁ + termOfList l₂ = 0) : ofList l₁ + ofList l₂ = 0 := by + have h2 : ofList l₂ = DirectSum.of (fun u => CoeffSubmodule u) ↑l₁ + ⟨termOfList l₂, Submodule.subset_span ⟨l₂, hp, rfl⟩⟩ := of_eq hp rfl + have hsum : (⟨termOfList l₁, Submodule.subset_span ⟨l₁, rfl, rfl⟩⟩ + + ⟨termOfList l₂, Submodule.subset_span ⟨l₂, hp, rfl⟩⟩ : CoeffSubmodule ↑l₁) = 0 := + Subtype.ext h + rw [ofList, h2, ← map_add, hsum, map_zero] + +lemma ofGenerator_fermion_sq (ψf : Fermions) : + ofGenerator (.fermion ψf) * ofGenerator (.fermion ψf) = 0 := by + rw [ofGenerator, ← ofList_append] + exact ofList_eq_zero (by simp [termOfList]) + +lemma ofGenerator_fermion_add_swap (ψ₁ ψ₂ : Fermions) : + ofGenerator (.fermion ψ₁) * ofGenerator (.fermion ψ₂) + + ofGenerator (.fermion ψ₂) * ofGenerator (.fermion ψ₁) = 0 := by + rw [ofGenerator, ofGenerator, ← ofList_append, ← ofList_append] + exact ofList_add_ofList + (by simpa using List.Perm.swap (FieldGenerators.fermion ψ₁) (.fermion ψ₂) []) + (by simpa [termOfList] using fermion_mul_fermion_add_swap ψ₁ ψ₂) + +/-- The decomposition map on the fermionic factor, sending each fermionic generator to + its class in degree `{ψ}`. -/ +noncomputable def decomposeExt : + ExteriorAlgebra ℂ (Module.Dual ℂ (LeftHandedWeyl × ConjModule LeftHandedWeyl)) →ₐ[ℂ] + ⨁ s, CoeffSubmodule s := + ExteriorAlgebra.lift ℂ + ⟨(LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis.constr ℂ + (fun i => ofGenerator (.fermion (Sum.elim Fermions.ψ Fermions.barψ i))), by + intro m + -- Generic ring/module lemmas restated locally so that their statements carry the + -- direct sum's own instances; `rw` can then match where the library patterns cannot. + have hexpand : ∀ f g : Fin 2 ⊕ Fin 2 → ⨁ s, CoeffSubmodule s, + (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j := fun f g => Fintype.sum_mul_sum f g + have hsmul : ∀ (a b : ℂ) (x y : ⨁ s, CoeffSubmodule s), + (a • x) * (b • y) = (a * b) • (x * y) := fun a b x y => smul_mul_smul_comm a x b y + have hcollect : ∀ (a : ℂ) (x y : ⨁ s, CoeffSubmodule s), + a • x + a • y = a • (x + y) := fun a x y => (smul_add a x y).symm + have hzero : ∀ a : ℂ, a • (0 : ⨁ s, CoeffSubmodule s) = 0 := fun a => smul_zero a + rw [Basis.constr_apply_fintype, hexpand, ← Finset.sum_product'] + refine Finset.sum_involution (fun p _ => (p.2, p.1)) ?_ ?_ + (fun p _ => Finset.mem_univ _) (fun p _ => rfl) + · intro p _ + rw [hsmul, hsmul, mul_comm + ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis.equivFun m p.2) + ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis.equivFun m p.1), + hcollect, ofGenerator_fermion_add_swap, hzero] + · intro p _ hne heq + refine hne ?_ + have h1 : p.2 = p.1 := congrArg Prod.fst heq + rw [hsmul, h1, ofGenerator_fermion_sq, hzero]⟩ + +/-- The subalgebra of the graded direct sum generated by the bosonic generator classes. + It is commutative, which lets `SymmetricAlgebra.lift` target it. -/ +noncomputable def bosonicAdjoin : Subalgebra ℂ (⨁ s, CoeffSubmodule s) := + Algebra.adjoin ℂ {ofGenerator (.cScalar .φ), ofGenerator (.cScalar .barφ)} + +instance : IsMulCommutative bosonicAdjoin := + Algebra.isMulCommutative_adjoin ℂ (by + rintro a (rfl | rfl) b (rfl | rfl) + · rfl + · exact ofGenerator_comm (cScalar_comm_cScalar .φ .barφ) + · exact ofGenerator_comm (cScalar_comm_cScalar .barφ .φ) + · rfl) + +open scoped IsMulCommutative in +/-- The decomposition map on the bosonic factor. Since `SymmetricAlgebra.lift` requires a + commutative target, we factor through `bosonicAdjoin`. -/ +noncomputable def decomposeSym : + SymmetricAlgebra ℂ (Module.Dual ℂ (ℂ × ConjModule ℂ)) →ₐ[ℂ] ⨁ s, CoeffSubmodule s := + bosonicAdjoin.val.comp <| SymmetricAlgebra.lift <| + ((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis.constr ℂ + (Sum.elim + (fun _ => ⟨ofGenerator (.cScalar .φ), Algebra.subset_adjoin (Set.mem_insert _ _)⟩) + (fun _ => ⟨ofGenerator (.cScalar .barφ), + Algebra.subset_adjoin (Set.mem_insert_of_mem _ rfl)⟩)) + +lemma decomposeSym_mem_bosonicAdjoin (x : SymmetricAlgebra ℂ (Module.Dual ℂ (ℂ × ConjModule ℂ))) : + decomposeSym x ∈ bosonicAdjoin := by + simp only [decomposeSym, AlgHom.coe_comp, Function.comp_apply, Subalgebra.coe_val] + exact SetLike.coe_mem _ + +lemma decomposeExt_ι (v : Module.Dual ℂ (LeftHandedWeyl × ConjModule LeftHandedWeyl)) : + decomposeExt (ExteriorAlgebra.ι ℂ v) = + ∑ j, (LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis.equivFun v j • + ofGenerator (.fermion (Sum.elim Fermions.ψ Fermions.barψ j)) := by + rw [decomposeExt, ExteriorAlgebra.lift_ι_apply, Basis.constr_apply_fintype] + +lemma commute_decomposeSym_decomposeExt + (x : SymmetricAlgebra ℂ (Module.Dual ℂ (ℂ × ConjModule ℂ))) + (y : ExteriorAlgebra ℂ (Module.Dual ℂ (LeftHandedWeyl × ConjModule LeftHandedWeyl))) : + Commute (decomposeSym x) (decomposeExt y) := by + -- Every element of `bosonicAdjoin` commutes with the image of the fermionic factor; + -- this avoids ever unfolding `decomposeSym`. + have hgen : ∀ g ∈ ({ofGenerator (.cScalar .φ), ofGenerator (.cScalar .barφ)} : + Set (⨁ s, CoeffSubmodule s)), Commute g (decomposeExt y) := by + intro g hg + induction y using ExteriorAlgebra.induction with + | algebraMap c => rw [AlgHom.commutes]; exact (Algebra.commutes c g).symm + | mul y₁ y₂ h₁ h₂ => + rw [map_mul] + exact Commute.mul_right (a := g) (b := decomposeExt y₁) h₁ h₂ + | add y₁ y₂ h₁ h₂ => rw [map_add]; exact h₁.add_right h₂ + | ι v => + rw [decomposeExt_ι] + refine Commute.sum_right (b := g) _ _ fun j _ => ?_ + refine Commute.smul_right (a := g) ?_ _ + rcases hg with rfl | rfl + · exact ofGenerator_comm (cScalar_comm_fermion _ _) + · exact ofGenerator_comm (cScalar_comm_fermion _ _) + have hx := decomposeSym_mem_bosonicAdjoin x + generalize decomposeSym x = a at hx ⊢ + induction hx using Algebra.adjoin_induction with + | mem a ha => exact hgen a ha + | algebraMap c => exact Algebra.commutes c _ + | add a b _ _ h₁ h₂ => exact h₁.add_left h₂ + | mul a b _ _ h₁ h₂ => exact Commute.mul_left (c := decomposeExt y) h₁ h₂ + +noncomputable def decompose' : EFTLagrangianExclDeriv →ₐ[ℂ] ⨁ s, CoeffSubmodule s := + Algebra.TensorProduct.lift decomposeSym decomposeExt commute_decomposeSym_decomposeExt + +lemma decomposeSym_ι_basis (j : Fin 1 ⊕ Fin 1) : + decomposeSym (SymmetricAlgebra.ι ℂ _ + (((Basis.singleton (Fin 1) ℂ).prod (Basis.singleton (Fin 1) ℂ).conj).dualBasis j)) = + Sum.elim (fun _ => ofGenerator (.cScalar .φ)) (fun _ => ofGenerator (.cScalar .barφ)) j := by + simp only [decomposeSym, AlgHom.coe_comp, Function.comp_apply, SymmetricAlgebra.lift_ι_apply, + Basis.constr_basis] + obtain (j | j) := j <;> rfl + +lemma decomposeExt_ι_basis (j : Fin 2 ⊕ Fin 2) : + decomposeExt (ExteriorAlgebra.ι ℂ + ((LeftHandedWeyl.basis.prod LeftHandedWeyl.basis.conj).dualBasis j)) = + ofGenerator (.fermion (Sum.elim Fermions.ψ Fermions.barψ j)) := by + rw [decomposeExt, ExteriorAlgebra.lift_ι_apply, Basis.constr_basis] + +lemma decompose'_ofFieldGenerators (g : FieldGenerators) : + decompose' [g]ₐ = ofGenerator g := by + -- Local restatements of `mul_one`/`one_mul` carrying the direct sum's own instances. + have hmul_one : ∀ x : ⨁ s, CoeffSubmodule s, x * 1 = x := fun x => mul_one x + have hone_mul : ∀ x : ⨁ s, CoeffSubmodule s, 1 * x = x := fun x => one_mul x + match g with + | .cScalar .φ => + rw [decompose', show ([ComplexScalars.φ]ₛ : EFTLagrangianExclDeriv) = + SymmetricAlgebra.ι ℂ _ (((Basis.singleton (Fin 1) ℂ).prod + (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inl 0)) ⊗ₜ 1 from rfl, + Algebra.TensorProduct.lift_tmul, map_one, hmul_one, decomposeSym_ι_basis] + rfl + | .cScalar .barφ => + rw [decompose', show ([ComplexScalars.barφ]ₛ : EFTLagrangianExclDeriv) = + SymmetricAlgebra.ι ℂ _ (((Basis.singleton (Fin 1) ℂ).prod + (Basis.singleton (Fin 1) ℂ).conj).dualBasis (Sum.inr 0)) ⊗ₜ 1 from rfl, + Algebra.TensorProduct.lift_tmul, map_one, hmul_one, decomposeSym_ι_basis] + rfl + | .fermion (.ψ α) => + rw [decompose', show ([Fermions.ψ α]ₑ : EFTLagrangianExclDeriv) = + 1 ⊗ₜ ExteriorAlgebra.ι ℂ ((LeftHandedWeyl.basis.prod + LeftHandedWeyl.basis.conj).dualBasis (Sum.inl α)) from rfl, + Algebra.TensorProduct.lift_tmul, map_one, hone_mul, decomposeExt_ι_basis] + rfl + | .fermion (.barψ α) => + rw [decompose', show ([Fermions.barψ α]ₑ : EFTLagrangianExclDeriv) = + 1 ⊗ₜ ExteriorAlgebra.ι ℂ ((LeftHandedWeyl.basis.prod + LeftHandedWeyl.basis.conj).dualBasis (Sum.inr α)) from rfl, + Algebra.TensorProduct.lift_tmul, map_one, hone_mul, decomposeExt_ι_basis] + rfl + +lemma decompose'_termOfList (l : List FieldGenerators) : + decompose' (termOfList l) = ofList l := by + induction l with + | nil => rw [termOfList_nil, map_one, ofList_nil] + | cons g t ih => + rw [termOfList_cons, map_mul, ih, decompose'_ofFieldGenerators, ofGenerator, + ← ofList_append, List.singleton_append] + +lemma coeAlgHom_ofList (l : List FieldGenerators) : + DirectSum.coeAlgHom CoeffSubmodule (ofList l) = termOfList l := by + rw [ofList] + exact DirectSum.coeAlgHom_of _ _ _ + +instance : GradedAlgebra CoeffSubmodule := by + refine GradedAlgebra.ofAlgHom CoeffSubmodule decompose' ?_ ?_ + · refine AlgHom.ext fun x => ?_ + rw [AlgHom.comp_apply, AlgHom.id_apply] + induction mem_termOfList_span x using Submodule.span_induction with + | mem a ha => + obtain ⟨l, rfl⟩ := ha + rw [decompose'_termOfList] + exact coeAlgHom_ofList l + | zero => simp + | add a b _ _ h₁ h₂ => rw [map_add, map_add, h₁, h₂] + | smul c a _ h₁ => rw [map_smul, map_smul, h₁] + · intro s x + obtain ⟨x, hx⟩ := x + induction hx using Submodule.span_induction with + | mem a ha => + obtain ⟨l, hl, rfl⟩ := ha + subst hl + rw [decompose'_termOfList] + rfl + | zero => exact (map_zero (DirectSum.of (fun i => CoeffSubmodule i) s)).symm ▸ map_zero _ + | add a b ha hb h₁ h₂ => rw [map_add, h₁, h₂, ← map_add]; rfl + | smul c a ha h₁ => + rw [map_smul, h₁, ← DirectSum.lof_eq_of ℂ, ← map_smul]; rfl + + +def coeff (s : Multiset FieldGenerators) : EFTLagrangianExclDeriv →ₗ[ℂ] EFTLagrangianExclDeriv:= + GradedAlgebra.proj CoeffSubmodule s + +end CoeffSubmodule + + +end EFTLagrangianExclDeriv diff --git a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean index 6884f71db..96025fd99 100644 --- a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean +++ b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean @@ -32,6 +32,8 @@ Although a different index convention is used there. namespace Fermion noncomputable section +TODO "Relate `DualLeftHandedWeyl` to `LeftHandedWeyl` via `Module.dual`." + /-- The module in which dual-left handed fermions live. This is equivalent to `Fin 2 → ℂ`. -/ structure DualLeftHandedWeyl where /-- The underlying value in `Fin 2 → ℂ`. -/ diff --git a/Physlib/Relativity/Fermions/Weyl/Metric.lean b/Physlib/Relativity/Fermions/Weyl/Metric.lean index 6e6ae5df8..cf6b3ea46 100644 --- a/Physlib/Relativity/Fermions/Weyl/Metric.lean +++ b/Physlib/Relativity/Fermions/Weyl/Metric.lean @@ -118,6 +118,13 @@ lemma leftMetric_apply_one : leftMetric (1 : ℂ) = leftMetricVal := by change (1 : ℂ) • leftMetricVal = leftMetricVal simp only [one_smul] +/-- The metric `εᵃᵃ` is invariant under the action of `SL(2,ℂ)`. -/ +lemma leftMetricVal_rep (M : SL(2,ℂ)) : + TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M) leftMetricVal = + leftMetricVal := by + have h := LinearMap.congr_fun (leftMetric.isIntertwining' M) (1 : ℂ) + simpa [leftMetric_apply_one, Representation.tprod_apply] using h.symm + /-- The metric `εₐₐ` as an element of `(dualLeftHanded ⊗ dualLeftHanded).V`. -/ def dualLeftMetricVal : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) := dualLeftdualLeftToMatrix.symm metricRaw