Anomaly 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
  • A.1. A constructor for ACCSystemCharges
• 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.

A. 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.

structure ACCSystemCharges : Type

A system of charges, specified by the number of charges.

• numberCharges : ℕ

  The number of charges.

A.1. A constructor for ACCSystemCharges

We provide a constructor ACCSystemChargesMk for ACCSystemCharges given the number of charges.

def ACCSystemChargesMk (n : ℕ) : ACCSystemCharges

Creates an ACCSystemCharges object with the specified number of charges.

Equations

• ACCSystemChargesMk n = { numberCharges := n }

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.

def ACCSystemCharges.Charges (χ : ACCSystemCharges) : Type

The charges as functions from Fin χ.numberCharges → ℚ.

Equations

• χ.Charges = (Fin χ.numberCharges → ℚ)

B.1. The ℚ-module structure on the type Charges

The type χ.Charges has the structure of a module over the field ℚ.

instance ACCSystemCharges.chargesAddCommMonoid (χ : ACCSystemCharges) : AddCommMonoid χ.Charges

An instance to provide the necessary operations and properties for charges to form an additive commutative monoid.

Equations

• χ.chargesAddCommMonoid = Pi.addCommMonoid

@[simp]

theorem ACCSystemCharges.chargesAddCommMonoid_add (χ : ACCSystemCharges) (f g : (i : Fin χ.numberCharges) → (fun (a : Fin χ.numberCharges) => ℚ) i) (i : Fin χ.numberCharges) : (f + g) i = f i + g i

@[simp]

theorem ACCSystemCharges.chargesAddCommMonoid_zero_num (χ : ACCSystemCharges) (x✝ : Fin χ.numberCharges) : (0 x✝).num = 0

@[simp]

theorem ACCSystemCharges.chargesAddCommMonoid_nsmul (χ : ACCSystemCharges) (n : ℕ) (x : (i : Fin χ.numberCharges) → (fun (a : Fin χ.numberCharges) => ℚ) i) (i : Fin χ.numberCharges) : (n • x) i = ↑n * x i

@[simp]

theorem ACCSystemCharges.chargesAddCommMonoid_zero_den (χ : ACCSystemCharges) (x✝ : Fin χ.numberCharges) : (0 x✝).den = 1

instance ACCSystemCharges.chargesModule (χ : ACCSystemCharges) : Module ℚ χ.Charges

An instance to provide the necessary operations and properties for charges to form a module over the field ℚ.

Equations

• χ.chargesModule = Pi.module (Fin χ.numberCharges) (fun (a : Fin χ.numberCharges) => ℚ) ℚ

@[simp]

theorem ACCSystemCharges.chargesModule_smul (χ : ACCSystemCharges) (x1✝ : ℚ) (x2✝ : (i : Fin χ.numberCharges) → (fun (a : Fin χ.numberCharges) => ℚ) i) (i : Fin χ.numberCharges) : SMul.smul x1✝ x2✝ i = x1✝ * x2✝ i

instance ACCSystemCharges.ChargesAddCommGroup (χ : ACCSystemCharges) : AddCommGroup χ.Charges

Equations

• χ.ChargesAddCommGroup = Module.addCommMonoidToAddCommGroup ℚ

B.2. The finiteness of the ℚ-module structure on Charges

The type χ.Charges is a finite module.

instance ACCSystemCharges.instFiniteRatCharges (χ : ACCSystemCharges) : Module.Finite ℚ χ.Charges

The module χ.Charges over ℚ is finite.

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.

structure ACCSystemLinearextends ACCSystemCharges : Type

The type of charges plus the linear ACCs.

• numberCharges : ℕ
• numberLinear : ℕ

  The number of linear ACCs.

• linearACCs : Fin self.numberLinear → self.Charges →ₗ[ℚ] ℚ

  The linear ACCs.

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.

structure ACCSystemLinear.LinSols (χ : ACCSystemLinear) : Type

The type of solutions to the linear ACCs.

• val : χ.Charges

  The underlying charge.

• linearSol (i : Fin χ.numberLinear) : (χ.linearACCs i) self.val = 0

  The condition that the charge satisfies the linear ACCs.

D.1. Extensionality of solutions to the linear ACCs

We prove a lemma relating to the equality of two elements of LinSols.

theorem ACCSystemLinear.LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val) : S = T

Two solutions are equal if the underlying charges are equal.

theorem ACCSystemLinear.LinSols.ext_iff {χ : ACCSystemLinear} {S T : χ.LinSols} : S = T ↔ S.val = T.val

D.2. Module structure on the solutions to the linear ACCs

we now give a module structure to LinSols.

instance ACCSystemLinear.linSolsAddCommMonoid (χ : ACCSystemLinear) : AddCommMonoid χ.LinSols

An instance providing the operations and properties for LinSols to form an additive commutative monoid.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ACCSystemLinear.linSolsAddCommMonoid_add_val (χ : ACCSystemLinear) (S T : χ.LinSols) : (S + T).val = S.val + T.val

@[simp]

theorem ACCSystemLinear.linSolsAddCommMonoid_nsmul_val (χ : ACCSystemLinear) (n : ℕ) (S : χ.LinSols) : (n • S).val = n • S.val

@[simp]

theorem ACCSystemLinear.linSolsAddCommMonoid_zero_val (χ : ACCSystemLinear) : LinSols.val 0 = Zero.zero

instance ACCSystemLinear.linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols

An instance providing the operations and properties for LinSols to form a module over ℚ.

Equations

• χ.linSolsModule = { smul := fun (a : ℚ) (S : χ.LinSols) => { val := a • S.val, linearSol := ⋯ }, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem ACCSystemLinear.linSolsModule_smul_val (χ : ACCSystemLinear) (a : ℚ) (S : χ.LinSols) : (SMul.smul a S).val = a • S.val

instance ACCSystemLinear.linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols

Equations

• χ.linSolsAddCommGroup = 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.

def ACCSystemLinear.linSolsIncl (χ : ACCSystemLinear) : χ.LinSols →ₗ[ℚ] χ.Charges

The inclusion of LinSols into charges.

Equations

• χ.linSolsIncl = { toFun := fun (S : χ.LinSols) => S.val, map_add' := ⋯, map_smul' := ⋯ }

theorem ACCSystemLinear.linSolsIncl_injective (χ : ACCSystemLinear) : Function.Injective ⇑χ.linSolsIncl

E. 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.

structure ACCSystemQuadextends ACCSystemLinear : Type

The type of charges plus the linear ACCs plus the quadratic ACCs.

• numberCharges : ℕ
• numberLinear : ℕ
• linearACCs : Fin self.numberLinear → self.Charges →ₗ[ℚ] ℚ
• numberQuadratic : ℕ

  The number of quadratic ACCs.

• quadraticACCs : Fin self.numberQuadratic → HomogeneousQuadratic self.Charges

  The quadratic ACCs.

F. The solutions to the quadratic and linear anomaly cancellation conditions

We define the type QuadSols of solutions to the linear and quadratic ACCs.

structure ACCSystemQuad.QuadSols (χ : ACCSystemQuad) extends χ.LinSols : Type

The type of solutions to the linear and quadratic ACCs.

• val : χ.Charges
• linearSol (i : Fin χ.numberLinear) : (χ.linearACCs i) self.val = 0
• quadSol (i : Fin χ.numberQuadratic) : (χ.quadraticACCs i) self.val = 0

  The condition that the charge satisfies the quadratic ACCs.

F.1. Extensionality of solutions to the quadratic and linear ACCs

We prove a lemma relating to the equality of two elements of QuadSols.

theorem ACCSystemQuad.QuadSols.ext {χ : ACCSystemQuad} {S T : χ.QuadSols} (h : S.val = T.val) : S = T

Two QuadSols are equal if the underlying charges are equal.

theorem ACCSystemQuad.QuadSols.ext_iff {χ : ACCSystemQuad} {S T : χ.QuadSols} : S = T ↔ S.val = T.val

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 ℚ.

instance ACCSystemQuad.quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols

An instance giving the properties and structures to define an action of ℚ on QuadSols.

Equations

• χ.quadSolsMulAction = { smul := fun (a : ℚ) (S : χ.QuadSols) => { toLinSols := a • S.toLinSols, quadSol := ⋯ }, one_smul := ⋯, mul_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.

def ACCSystemQuad.quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →ₑ[id] χ.LinSols

The inclusion of quadratic solutions into linear solutions.

Equations

• χ.quadSolsInclLinSols = { toFun := ACCSystemQuad.QuadSols.toLinSols, map_smul' := ⋯ }

theorem ACCSystemQuad.quadSolsInclLinSols_injective (χ : ACCSystemQuad) : Function.Injective ⇑χ.quadSolsInclLinSols

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.

def ACCSystemQuad.linSolsInclQuadSolsZero (χ : ACCSystemQuad) (h : χ.numberQuadratic = 0) : χ.LinSols →ₑ[id] χ.QuadSols

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).

Equations

• χ.linSolsInclQuadSolsZero h = { toFun := fun (S : χ.LinSols) => { toLinSols := S, quadSol := ⋯ }, map_smul' := ⋯ }

F.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.

def ACCSystemQuad.quadSolsIncl (χ : ACCSystemQuad) : χ.QuadSols →ₑ[id] χ.Charges

The inclusion of quadratic solutions into all charges.

Equations

• χ.quadSolsIncl = χ.linSolsIncl.toMulActionHom.comp χ.quadSolsInclLinSols

theorem ACCSystemQuad.quadSolsIncl_injective (χ : ACCSystemQuad) : Function.Injective ⇑χ.quadSolsIncl

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.

structure ACCSystemextends ACCSystemQuad : Type

The type of charges plus the anomaly cancellation conditions.

• numberCharges : ℕ
• numberLinear : ℕ
• linearACCs : Fin self.numberLinear → self.Charges →ₗ[ℚ] ℚ
• numberQuadratic : ℕ
• quadraticACCs : Fin self.numberQuadratic → HomogeneousQuadratic self.Charges
• cubicACC : HomogeneousCubic self.Charges

  The cubic ACC.

H. The solutions to the full anomaly cancellation conditions

We define the type Sols of solutions to the full ACCs.

structure ACCSystem.Sols (χ : ACCSystem) extends χ.QuadSols : Type

The type of solutions to the anomaly cancellation conditions.

• val : χ.Charges
• linearSol (i : Fin χ.numberLinear) : (χ.linearACCs i) self.val = 0
• quadSol (i : Fin χ.numberQuadratic) : (χ.quadraticACCs i) self.val = 0
• cubicSol : χ.cubicACC self.val = 0

  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.

theorem ACCSystem.Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) : S = T

Two solutions are equal if the underlying charges are equal.

H.2. The IsSolution predicate

we define a predicate on charges which is true if they correspond to a solution.

def ACCSystem.IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop

A charge S is a solution if it extends to a solution.

Equations

• χ.IsSolution S = ∃ (sol : χ.Sols), sol.val = S

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 ℚ.

instance ACCSystem.solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols

An instance giving the properties and structures to define an action of ℚ on Sols.

Equations

• χ.solsMulAction = { smul := fun (a : ℚ) (S : χ.Sols) => { toQuadSols := a • S.toQuadSols, cubicSol := ⋯ }, one_smul := ⋯, mul_smul := ⋯ }

H.4. Embeddings of solutions to the ACCs into quadratic solutions

def ACCSystem.solsInclQuadSols (χ : ACCSystem) : χ.Sols →ₑ[id] χ.QuadSols

The inclusion of Sols into QuadSols.

Equations

• χ.solsInclQuadSols = { toFun := ACCSystem.Sols.toQuadSols, map_smul' := ⋯ }

theorem ACCSystem.solsInclQuadSols_injective (χ : ACCSystem) : Function.Injective ⇑χ.solsInclQuadSols

H.5. Embeddings of solutions to the ACCs into linear solutions

def ACCSystem.solsInclLinSols (χ : ACCSystem) : χ.Sols →ₑ[id] χ.LinSols

The inclusion of Sols into LinSols.

Equations

• χ.solsInclLinSols = χ.quadSolsInclLinSols.comp χ.solsInclQuadSols

theorem ACCSystem.solsInclLinSols_injective (χ : ACCSystem) : Function.Injective ⇑χ.solsInclLinSols

H.6. Embeddings of solutions to the ACCs into charges

def ACCSystem.solsIncl (χ : ACCSystem) : χ.Sols →ₑ[id] χ.Charges

The inclusion of Sols into LinSols.

Equations

• χ.solsIncl = χ.quadSolsIncl.comp χ.solsInclQuadSols

theorem ACCSystem.solsIncl_injective (χ : ACCSystem) : Function.Injective ⇑χ.solsIncl

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.

structure ACCSystem.Hom (χ η : ACCSystem) : Type

The structure of a map between two ACCSystems.

• charges : χ.Charges →ₗ[ℚ] η.Charges

  The linear map between vector spaces of charges.

• anomalyFree : χ.Sols → η.Sols

  The map between solutions.

• commute : ⇑self.charges ∘ ⇑χ.solsIncl = ⇑η.solsIncl ∘ self.anomalyFree

  The condition that the map commutes with the relevant inclusions.

I.1. Composition of morphisms between ACC systems

def ACCSystem.Hom.comp {χ η ε : ACCSystem} (g : η.Hom ε) (f : χ.Hom η) : χ.Hom ε

The definition of composition between two ACCSystems.

Equations

• g.comp f = { charges := g.charges ∘ₗ f.charges, anomalyFree := g.anomalyFree ∘ f.anomalyFree, commute := ⋯ }

J. Open TODO items

We give some open TODO items for future work.

(To view these you may need to go to the GitHub source code for the file.)