Anomaly cancellation of a theory with a pure U(1)-gauge group

In a pure U(1) gauge theory with n Weyl fermions carrying charges xᵢ the anomaly cancellation conditions (ACCs) which must be satisfied for a consistent gauge theory correspond to:

• The linear ACC: ∑ xᵢ = 0
• The cubic ACC: ∑ xᵢ³ = 0

The charges xᵢ have rational fractions with one another, here they are specified as rational numbers.

def PureU1.PureU1Charges (n : ℕ) : ACCSystemCharges

The vector space of charges.

Equations

• PureU1.PureU1Charges n = ACCSystemChargesMk n

@[simp]

theorem PureU1.PureU1Charges_numberCharges (n : ℕ) : (PureU1Charges n).numberCharges = n

def PureU1.accGrav (n : ℕ) : (PureU1Charges n).Charges →ₗ[ℚ] ℚ

The gravitational anomaly.

Equations

• PureU1.accGrav n = { toFun := fun (S : (PureU1.PureU1Charges n).Charges) => ∑ i : Fin n, S i, map_add' := ⋯, map_smul' := ⋯ }

def PureU1.accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges

The symmetric trilinear form used to define the cubic anomaly.

Equations

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

@[simp]

theorem PureU1.accCubeTriLinSymm_toFun_apply_apply {n : ℕ} (S S✝ T : (PureU1Charges n).Charges) : ((accCubeTriLinSymm S) S✝) T = ∑ i : Fin n, S i * S✝ i * T i

def PureU1.accCube (n : ℕ) : HomogeneousCubic (PureU1Charges n).Charges

The cubic anomaly equation.

Equations

• PureU1.accCube n = PureU1.accCubeTriLinSymm.toCubic

theorem PureU1.accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) : (accCube n) S = ∑ i : Fin n, S i ^ 3

The cubic ACC for the pure-U(1) anomaly equations is equal to the sum of the cubed charges.

def PureU1 (n : ℕ) : ACCSystem

The ACC system for a pure $U(1)$ gauge theory with $n$ fermions.

Equations

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

@[simp]

theorem PureU1_numberLinear (n : ℕ) : (PureU1 n).numberLinear = 1

@[simp]

theorem PureU1_numberQuadratic (n : ℕ) : (PureU1 n).numberQuadratic = 0

@[simp]

theorem PureU1_cubicACC_apply (n : ℕ) (S : (PureU1.PureU1Charges n).Charges) : (PureU1 n).cubicACC S = ∑ i : Fin n, S i * S i * S i

@[simp]

theorem PureU1_numberCharges (n : ℕ) : (PureU1 n).numberCharges = n

@[simp]

theorem PureU1_linearACCs (n : ℕ) (i : Fin 1) : (PureU1 n).linearACCs i = match i with | 0 => PureU1.accGrav n

@[simp]

theorem PureU1_quadraticACCs (n : ℕ) (a✝ : Fin 0) : (PureU1 n).quadraticACCs a✝ = a✝.elim0

def pureU1EqCharges {n m : ℕ} (h : n = m) : (PureU1 n).Charges ≃ₗ[ℚ] (PureU1 m).Charges

An equivalence of vector spaces of charges when the number of fermions is equal.

Equations

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

theorem pureU1_linear {n : ℕ} (S : (PureU1 n).LinSols) : ∑ i : Fin n, S.val i = 0

A solution to the pure U(1) accs satisfies the linear ACCs.

theorem pureU1_cube {n : ℕ} (S : (PureU1 n).Sols) : ∑ i : Fin (PureU1 n).numberCharges, S.val i ^ 3 = 0

A solution to the pure U(1) accs satisfies the cubic ACCs.

theorem pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) : S.val (Fin.last n) = -∑ i : Fin n, S.val i.castSucc

The last charge of a solution to the linear ACCs is equal to the negation of the sum of the other charges.

theorem pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols} (h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T

Two solutions to the Linear ACCs for n.succ are equal if their first n charges are equal.

theorem PureU1.sum_of_charges {k n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) : (∑ i : Fin k, f i) j = ∑ i : Fin k, f i j

The jth charge of a sum of pure-U(1) charges is equal to the sum of their jth charges.

theorem PureU1.sum_of_anomaly_free_linear {k n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : (∑ i : Fin k, f i).val j = ∑ i : Fin k, (f i).val j

The jth charge of a sum of solutions to the linear ACC is equal to the sum of their jth charges.