Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Mathematics.LinearMaps
public import Mathlib.LinearAlgebra.FiniteDimensional.Defs
public import Mathlib.Tactic.CasesAnomaly cancellation conditions
i. Overview
Anomaly cancellation conditions (ACCs) are consistency conditions which arise
in gauge field theories. They correspond to a set of homogeneous diophantine equations
in the rational charges assigned to fermions under u(1) contributions to the gauge group.
These formally arise from triangle Feynman diagrams, but can otherwise be got from index theorems.
ii. Key results
There are four different types related to the underlying structure of the ACCs:
ACCSystemCharges: the structure carrying the number of charges present.
ACCSystemLinear: the structure extending ACCSystemCharges with linear anomaly cancellation
conditions.
ACCSystemQuad: the structure extending ACCSystemLinear with quadratic anomaly cancellation
conditions.
ACCSystem: the structure extending ACCSystemQuad with the cubic anomaly cancellation
condition.
Related to these are the different types of spaces of charges:
Charges: the module of all possible charge allocations.
LinSols: the module of solutions to the linear ACCs.
QuadSols: the solutions to the linear and quadratic ACCs.
Sols: the solutions to the full ACCs.
iii. Table of contents
A. The module of charges
B. The module of charges
B.1. The ℚ-module structure on the type Charges
B.2. The finiteness of the ℚ-module structure on Charges
C. The linear anomaly cancellation conditions
D. The module of solutions to the linear ACCs
D.1. Extensionality of solutions to the linear ACCs
D.2. Module structure on the solutions to the linear ACCs
D.3. Embedding of the solutions to the linear ACCs into the module of charges
E. The quadratic anomaly cancellation conditions
F. The solutions to the quadratic and linear anomaly cancellation conditions
F.1. Extensionality of solutions to the quadratic and linear ACCs
F.2. MulAction of rationals on the solutions to the quadratic and linear ACCs
F.3. Embeddings of quadratic solutions into linear solutions
F.4. Embeddings of solutions to linear ACCs into quadratic solutions when no quadratics
F.5. Embeddings of quadratic solutions into all charges
G. The full anomaly cancellation conditions
H. The solutions to the full anomaly cancellation conditions
H.1. Extensionality of solutions to the ACCs
H.2. The IsSolution predicate
H.3. MulAction of ℚ on the solutions to the ACCs
H.4. Embeddings of solutions to the ACCs into quadratic solutions
H.5. Embeddings of solutions to the ACCs into linear solutions
H.6. Embeddings of solutions to the ACCs into charges
I. Morphisms between ACC systems
I.1. Composition of morphisms between ACC systems
J. Open TODO items
iv. References
Some references on anomaly cancellation conditions are:
Alvarez-Gaume, L. and Ginsparg, P. H. (1985). The Structure of Gauge and Gravitational Anomalies.
Bilal, A. (2008). Lectures on Anomalies. arXiv preprint.
Nash, C. (1991). Differential topology and quantum field theory. Elsevier.
@[expose] public sectionA. The module of charges
We define the type ACCSystemCharges, this carries the charges
of the specification of the number of charges present in a theory.
For example for the standard model without right-handed neutrinos, this is 15 charges,
whilst with right handed neutrinos it is 18 charges.
We can think of Fin χ.numberCharges as an indexing type for
the representations present in the theory where χ : ACCSystemCharges.
A system of charges, specified by the number of charges.
The number of charges.
structure ACCSystemCharges where numberCharges : ℕB. The module of charges
Given an ACCSystemCharges object χ, we define the type of charges
χ.Charges as functions from Fin χ.numberCharges → ℚ.
That is, for each representation in the theory, indexed by an element of Fin χ.numberCharges,
we assign a rational charge.
The charges as functions from Fin χ.numberCharges → ℚ.
def Charges (χ : ACCSystemCharges) : Type := Fin χ.numberCharges → ℚ
B.1. The ℚ-module structure on the type Charges
The type χ.Charges has the structure of a module over the field ℚ.
An instance to provide the necessary operations and properties for charges to form an additive
commutative monoid.
@[simps!]
instance chargesAddCommMonoid (χ : ACCSystemCharges) : AddCommMonoid χ.Charges :=
Pi.addCommMonoid
An instance to provide the necessary operations and properties for charges to form a module
over the field ℚ.
@[simps!]
instance chargesModule (χ : ACCSystemCharges) : Module ℚ χ.Charges :=
Pi.module _ _ _instance ChargesAddCommGroup (χ : ACCSystemCharges) : AddCommGroup χ.Charges :=
Module.addCommMonoidToAddCommGroup ℚ
B.2. The finiteness of the ℚ-module structure on Charges
The type χ.Charges is a finite module.
The module χ.Charges over ℚ is finite.
instance (χ : ACCSystemCharges) : Module.Finite ℚ χ.Charges :=
FiniteDimensional.finiteDimensional_pi ℚC. The linear anomaly cancellation conditions
We define the type ACCSystemLinear which extends ACCSystemCharges by adding
a finite number (determined by numberLinear) of linear equations in the rational charges.
The type of charges plus the linear ACCs.
The number of linear ACCs.
The linear ACCs.
structure ACCSystemLinear extends ACCSystemCharges where numberLinear : ℕ linearACCs : Fin numberLinear → (toACCSystemCharges.Charges →ₗ[ℚ] ℚ)D. The module of solutions to the linear ACCs
We define the type LinSols of solutions to the linear ACCs.
That is the submodule of χ.Charges which satisfy all the linear ACCs.
The type of solutions to the linear ACCs.
The underlying charge.
The condition that the charge satisfies the linear ACCs.
structure LinSols (χ : ACCSystemLinear) where val : χ.1.Charges linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0D.1. Extensionality of solutions to the linear ACCs
We prove a lemma relating to the equality of two elements of LinSols.
Two solutions are equal if the underlying charges are equal.
@[ext]
lemma LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val) : S = T := χ:ACCSystemLinearS:χ.LinSolsT:χ.LinSolsh:S.val = T.val⊢ S = T
χ:ACCSystemLinearT:χ.LinSolsval✝:χ.ChargeslinearSol✝:∀ (i : Fin χ.numberLinear), (χ.linearACCs i) val✝ = 0h:{ val := val✝, linearSol := linearSol✝ }.val = T.val⊢ { val := val✝, linearSol := linearSol✝ } = T
All goals completed! 🐙D.2. Module structure on the solutions to the linear ACCs
we now give a module structure to LinSols.
An instance providing the operations and properties for LinSols to form an
additive commutative monoid.
@[simps!]
instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
AddCommMonoid χ.LinSols where
add S T := ⟨S.val + T.val, fun _ ↦ χ:ACCSystemLinearS:χ.LinSolsT:χ.LinSolsx✝:Fin χ.numberLinear⊢ (χ.linearACCs x✝) (S.val + T.val) = 0 All goals completed! 🐙⟩
add_comm S T := LinSols.ext (χ.chargesAddCommMonoid.add_comm _ _)
add_assoc S T L := LinSols.ext (χ.chargesAddCommMonoid.add_assoc _ _ _)
zero := ⟨χ.chargesAddCommMonoid.zero, fun _ ↦ (χ.linearACCs _).map_zero⟩
zero_add S := LinSols.ext (χ.chargesAddCommMonoid.zero_add _)
add_zero S := LinSols.ext (χ.chargesAddCommMonoid.add_zero _)
nsmul n S := ⟨n • S.val, fun _ ↦ χ:ACCSystemLinearn:ℕS:χ.LinSolsx✝:Fin χ.numberLinear⊢ (χ.linearACCs x✝) (n • S.val) = 0 All goals completed! 🐙⟩
nsmul_zero n := LinSols.ext (χ.chargesAddCommMonoid.nsmul_zero _)
nsmul_succ n S := LinSols.ext (χ.chargesAddCommMonoid.nsmul_succ _ _)
An instance providing the operations and properties for LinSols to form a
module over ℚ.
@[simps!]
instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
smul a S := ⟨a • S.val, fun _ ↦ χ:ACCSystemLineara:ℚS:χ.LinSolsx✝:Fin χ.numberLinear⊢ (χ.linearACCs x✝) (a • S.val) = 0 All goals completed! 🐙⟩
one_smul one_smul := LinSols.ext (χ.chargesModule.one_smul _)
mul_smul a b S := LinSols.ext (χ.chargesModule.mul_smul _ _ _)
smul_zero a := LinSols.ext (χ.chargesModule.smul_zero _)
zero_smul S := LinSols.ext (χ.chargesModule.zero_smul _)
smul_add a S T := LinSols.ext (χ.chargesModule.smul_add _ _ _)
add_smul a b T:= LinSols.ext (χ.chargesModule.add_smul _ _ _)instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols :=
Module.addCommMonoidToAddCommGroup ℚD.3. Embedding of the solutions to the linear ACCs into the module of charges
We give the linear embedding of solutions to the linear ACCs LinSols into
the module of all charges.
The inclusion of LinSols into charges.
def linSolsIncl (χ : ACCSystemLinear) : χ.LinSols →ₗ[ℚ] χ.Charges where
toFun S := S.val
map_add' _ _ := rfl
map_smul' _ _ := rfllemma linSolsIncl_injective (χ : ACCSystemLinear) :
Function.Injective χ.linSolsIncl := fun _ _ h => LinSols.ext hE. The quadratic anomaly cancellation conditions
We extend ACCSystemLinear to ACCSystemQuad by adding a finite number
(determined by numberQuadratic) of quadratic equations in the rational charges.
These quadratic anomaly cancellation conditions correspond to the interaction
of the u(1) part of the gauge group of interest with another abelian part.
The type of charges plus the linear ACCs plus the quadratic ACCs.
The number of quadratic ACCs.
The quadratic ACCs.
structure ACCSystemQuad extends ACCSystemLinear where numberQuadratic : ℕ quadraticACCs : Fin numberQuadratic → HomogeneousQuadratic toACCSystemCharges.ChargesF. The solutions to the quadratic and linear anomaly cancellation conditions
We define the type QuadSols of solutions to the linear and quadratic ACCs.
The type of solutions to the linear and quadratic ACCs.
The condition that the charge satisfies the quadratic ACCs.
structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0F.1. Extensionality of solutions to the quadratic and linear ACCs
We prove a lemma relating to the equality of two elements of QuadSols.
Two QuadSols are equal if the underlying charges are equal.
@[ext]
lemma QuadSols.ext {χ : ACCSystemQuad} {S T : χ.QuadSols} (h : S.val = T.val) :
S = T := χ:ACCSystemQuadS:χ.QuadSolsT:χ.QuadSolsh:S.val = T.val⊢ S = T
χ:ACCSystemQuadS:χ.QuadSolsT:χ.QuadSolsh✝:S.val = T.valh:S.toLinSols = T.toLinSols⊢ S = T
χ:ACCSystemQuadT:χ.QuadSolstoLinSols✝:χ.LinSolsquadSol✝:∀ (i : Fin χ.numberQuadratic), (χ.quadraticACCs i) toLinSols✝.val = 0h✝:{ toLinSols := toLinSols✝, quadSol := quadSol✝ }.val = T.valh:{ toLinSols := toLinSols✝, quadSol := quadSol✝ }.toLinSols = T.toLinSols⊢ { toLinSols := toLinSols✝, quadSol := quadSol✝ } = T
All goals completed! 🐙F.2. MulAction of rationals on the solutions to the quadratic and linear ACCs
The type QuadSols does not carry the structure of a module over ℚ as
the quadratic ACCs are not linear. However it does carry the structure of
a MulAction of ℚ.
An instance giving the properties and structures to define an action of ℚ on QuadSols.
instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols where
smul a S := ⟨a • S.toLinSols, fun _ ↦ χ:ACCSystemQuada:ℚS:χ.QuadSolsx✝:Fin χ.numberQuadratic⊢ (χ.quadraticACCs x✝) (a • S.toLinSols).val = 0 erw [χ:ACCSystemQuada:ℚS:χ.QuadSolsx✝:Fin χ.numberQuadratic⊢ a ^ 2 * (χ.quadraticACCs x✝) S.val = 0 χ:ACCSystemQuada:ℚS:χ.QuadSolsx✝:Fin χ.numberQuadratic⊢ a ^ 2 * 0 = 0
χ:ACCSystemQuada:ℚS:χ.QuadSolsx✝:Fin χ.numberQuadratic⊢ 0 = 0All goals completed! 🐙⟩
mul_smul a b S := QuadSols.ext (mul_smul _ _ _)
one_smul S := QuadSols.ext (one_smul _ _)F.3. Embeddings of quadratic solutions into linear solutions
We give the equivariant of solutions to the quadratic and linear ACCs QuadSols into
the solutions to the linear ACCs LinSols.
The inclusion of quadratic solutions into linear solutions.
def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols where
toFun := QuadSols.toLinSols
map_smul' _ _ := rfllemma quadSolsInclLinSols_injective (χ : ACCSystemQuad) :
Function.Injective χ.quadSolsInclLinSols :=
fun _ _ h => QuadSols.ext (congrArg (fun X => X.val) h)F.4. Embeddings of solutions to linear ACCs into quadratic solutions when no quadratics
When there are no quadratic ACCs, the solutions to the linear ACCs embed into the solutions to the quadratic and linear ACCs.
The inclusion of the linear solutions into the quadratic solutions, where there is no quadratic equations (i.e. no U(1)'s in the underlying gauge group).
χ:ACCSystemQuadh:χ.numberQuadratic = 0S:χ.LinSolsi✝:Fin χ.numberQuadratici:Fin 0⊢ (χ.quadraticACCs i) S.val = 0; All goals completed! 🐙⟩
map_smul' _ _ := rflF.5. Embeddings of quadratic solutions into all charges
We give the equivariant embedding of solutions to the quadratic and linear ACCs QuadSols into
the module of all charges Charges.
The inclusion of quadratic solutions into all charges.
def quadSolsIncl (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.Charges :=
MulActionHom.comp χ.linSolsIncl.toMulActionHom χ.quadSolsInclLinSolslemma quadSolsIncl_injective (χ : ACCSystemQuad) :
Function.Injective χ.quadSolsIncl :=
fun _ _ h => quadSolsInclLinSols_injective χ
(ACCSystemLinear.linSolsIncl_injective χ.toACCSystemLinear h)G. The full anomaly cancellation conditions
We extend ACCSystemQuad to ACCSystem by adding the single cubic equation
in the rational charges. This corresponds to the u(1)^3 anomaly.
The type of charges plus the anomaly cancellation conditions.
In many physical settings these conditions are derived formally from the gauge group and the fermionic representations. They arise from triangle Feynman diagrams, and can also be obtained using index-theoretic or characteristic-class constructions.
In this file, we take the resulting conditions as input data: linear, quadratic and cubic homogeneous forms on the space of rational charges.
The cubic ACC.
structure ACCSystem extends ACCSystemQuad where cubicACC : HomogeneousCubic toACCSystemCharges.ChargesH. The solutions to the full anomaly cancellation conditions
We define the type Sols of solutions to the full ACCs.
The type of solutions to the anomaly cancellation conditions.
The condition that the charge satisfies the cubic ACC.
H.1. Extensionality of solutions to the ACCs
We prove a lemma relating to the equality of two elements of Sols.
Two solutions are equal if the underlying charges are equal.
lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) :
S = T := χ:ACCSystemS:χ.SolsT:χ.Solsh:S.val = T.val⊢ S = T
χ:ACCSystemS:χ.SolsT:χ.Solsh✝:S.val = T.valh:S.toQuadSols = T.toQuadSols⊢ S = T
χ:ACCSystemT:χ.SolstoQuadSols✝:χ.QuadSolscubicSol✝:χ.cubicACC toQuadSols✝.val = 0h✝:{ toQuadSols := toQuadSols✝, cubicSol := cubicSol✝ }.val = T.valh:{ toQuadSols := toQuadSols✝, cubicSol := cubicSol✝ }.toQuadSols = T.toQuadSols⊢ { toQuadSols := toQuadSols✝, cubicSol := cubicSol✝ } = T
All goals completed! 🐙
H.2. The IsSolution predicate
we define a predicate on charges which is true if they correspond to a solution.
A charge S is a solution if it extends to a solution.
H.3. MulAction of ℚ on the solutions to the ACCs
Like with QuadSols, the type Sols does not carry the structure of a module over ℚ
as the cubic nor quadratic ACC is not linear. However it does carry the structure of
a MulAction of ℚ.
An instance giving the properties and structures to define an action of ℚ on Sols.
instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where
smul a S := ⟨a • S.toQuadSols, χ:ACCSystema:ℚS:χ.Sols⊢ χ.cubicACC (a • S.toQuadSols).val = 0
erw [χ:ACCSystema:ℚS:χ.Sols⊢ a ^ 3 * χ.cubicACC S.val = 0 χ:ACCSystema:ℚS:χ.Sols⊢ a ^ 3 * 0 = 0χ:ACCSystema:ℚS:χ.Sols⊢ a ^ 3 * 0 = 0
All goals completed! 🐙⟩
mul_smul a b S := Sols.ext (mul_smul _ _ _)
one_smul S := Sols.ext (one_smul _ _)H.4. Embeddings of solutions to the ACCs into quadratic solutions
The inclusion of Sols into QuadSols.
def solsInclQuadSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.QuadSols where
toFun := Sols.toQuadSols
map_smul' _ _ := rfllemma solsInclQuadSols_injective (χ : ACCSystem) :
Function.Injective χ.solsInclQuadSols :=
fun _ _ h => Sols.ext (congrArg (fun X => X.val) h)H.5. Embeddings of solutions to the ACCs into linear solutions
The inclusion of Sols into LinSols.
def solsInclLinSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.LinSols :=
MulActionHom.comp χ.quadSolsInclLinSols χ.solsInclQuadSolslemma solsInclLinSols_injective (χ : ACCSystem) :
Function.Injective χ.solsInclLinSols :=
fun _ _ h => solsInclQuadSols_injective χ
(ACCSystemQuad.quadSolsInclLinSols_injective χ.toACCSystemQuad h)H.6. Embeddings of solutions to the ACCs into charges
The inclusion of Sols into LinSols.
def solsIncl (χ : ACCSystem) : χ.Sols →[ℚ] χ.Charges :=
MulActionHom.comp χ.quadSolsIncl χ.solsInclQuadSolslemma solsIncl_injective (χ : ACCSystem) :
Function.Injective χ.solsIncl :=
fun _ _ h => solsInclQuadSols_injective χ
(ACCSystemQuad.quadSolsIncl_injective χ.toACCSystemQuad h)I. Morphisms between ACC systems
We define a morphisms between two ACCSystem objects.
as a linear map between their spaces of charges and a map between their spaces of solutions
such that mapping solutions and then including in the module of charges
is the same as including in the module of charges and then mapping charges.
The structure of a map between two ACCSystems.
The linear map between vector spaces of charges.
The map between solutions.
The condition that the map commutes with the relevant inclusions.
structure Hom (χ η : ACCSystem) where charges : χ.Charges →ₗ[ℚ] η.Charges anomalyFree : χ.Sols → η.Sols commute : charges ∘ χ.solsIncl = η.solsIncl ∘ anomalyFreeI.1. Composition of morphisms between ACC systems
The definition of composition between two ACCSystems.
All goals completed! 🐙J. Open TODO items
We give some open TODO items for future work.
One natural direction is to formalize how the anomaly cancellation conditions defining an
ACCSystem arise from gauge-theoretic data (a gauge group together with fermionic representations).
Physically these arise from triangle Feynman diagrams, and can also be described via index-theoretic
or characteristic-class constructions (e.g. through an anomaly polynomial). At present we do not
formalize this derivation in Lean, and instead take the resulting homogeneous forms as data.
(To view these you may need to go to the GitHub source code for the file.)
TODO "Anomaly cancellation conditions can be derived formally from the gauge group
and fermionic representations using e.g. topological invariants. Include such a
definition."TODO "Anomaly cancellation conditions can be defined using algebraic varieties.
Link such an approach to the approach here."