Basic set up for anomaly cancellation conditions

This file defines the basic structures for the anomaly cancellation conditions.

It defines a module structure on the charges, and the solutions to the linear ACCs.

structure ACCSystemCharges : Type

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

• numberCharges : ℕ

  The number of charges.

def ACCSystemChargesMk (n : ℕ) : ACCSystemCharges

Creates an ACCSystemCharges object with the specified number of charges.

Equations

• ACCSystemChargesMk n = { numberCharges := n }

def ACCSystemCharges.Charges (χ : ACCSystemCharges) : Type

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

Equations

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

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_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

@[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

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

An instance provides the necessary operations and properties for charges to form an additive commutative group.

Equations

• χ.ChargesAddCommGroup = Module.addCommMonoidToAddCommGroup ℚ

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

The module χ.Charges over ℚ is finite.

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.

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.

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.

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

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

Equations

• χ.linSolsAddCommMonoid = AddCommMonoid.mk ⋯

@[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 = Module.mk ⋯ ⋯

@[simp]

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

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

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

Equations

• χ.linSolsAddCommGroup = Module.addCommMonoidToAddCommGroup ℚ

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

The inclusion of LinSols into charges.

Equations

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

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.

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.

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.

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

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

Equations

• χ.quadSolsMulAction = MulAction.mk ⋯ ⋯

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

The inclusion of quadratic solutions into linear solutions.

Equations

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

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' := ⋯ }

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

The inclusion of quadratic solutions into all charges.

Equations

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

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.

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.

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.

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

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

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

Equations

• χ.solsMulAction = MulAction.mk ⋯ ⋯

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

The inclusion of Sols into QuadSols.

Equations

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

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

The inclusion of Sols into LinSols.

Equations

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

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

The inclusion of Sols into LinSols.

Equations

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

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.

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 := ⋯ }