From ecf2c8f6b83a9f0022ffb0ee6fa3d1d6dc245139 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 16 Apr 2024 16:01:44 -0400 Subject: [PATCH 1/2] feat: Add basic definitions for anomaly cancellation --- HepLean.lean | 1 + HepLean/AnomalyCancellation/Basic.lean | 284 +++++++++++++++++++++++++ 2 files changed, 285 insertions(+) create mode 100644 HepLean/AnomalyCancellation/Basic.lean diff --git a/HepLean.lean b/HepLean.lean index 95854bc1..d2c0da35 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -1 +1,2 @@ +import HepLean.AnomalyCancellation.Basic import HepLean.AnomalyCancellation.LinearMaps diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean new file mode 100644 index 00000000..62d3f06d --- /dev/null +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -0,0 +1,284 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.LinearMaps +import Mathlib.Tactic.Polyrith +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.FieldSimp +import Mathlib.NumberTheory.FLT.Basic +import Mathlib.Algebra.QuadraticDiscriminant +import Mathlib.Algebra.Module.Basic +import Mathlib.Algebra.Module.LinearMap.Basic +/-! +# 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. + +## TODO + +- Derive ACC systems from gauge algebras and fermionic representations. +- Relate ACCSystems to algebraic varities. + +-/ + +/-- A system of charges, specified by the number of charges. -/ +structure ACCSystemCharges where + /-- The number of charges. -/ + numberCharges : ℕ + +/-- + Creates an `ACCSystemCharges` object with the specified number of charges. +-/ +def ACCSystemChargesMk (n : ℕ) : ACCSystemCharges where + numberCharges := n + +namespace ACCSystemCharges + +/-- The charges as functions from `Fin χ.numberCharges → ℚ`. -/ +def charges (χ : ACCSystemCharges) : Type := Fin χ.numberCharges → ℚ + +/-- + 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 _ _ _ + +/-- + An instance provides the necessary operations and properties for `charges` to form an additive + commutative group. +-/ +instance ChargesAddCommGroup (χ : ACCSystemCharges) : AddCommGroup χ.charges := + Module.addCommMonoidToAddCommGroup ℚ + +end ACCSystemCharges + +/-- The type of charges plus the linear ACCs. -/ +structure ACCSystemLinear extends ACCSystemCharges where + /-- The number of linear ACCs. -/ + numberLinear : ℕ + /-- The linear ACCs. -/ + linearACCs : Fin numberLinear → (toACCSystemCharges.charges →ₗ[ℚ] ℚ) + +namespace ACCSystemLinear + +/-- The type of solutions to the linear ACCs. -/ +structure LinSols (χ : ACCSystemLinear) where + /-- The underlying charge. -/ + val : χ.1.charges + /-- The condition that the charge satifies the linear ACCs. -/ + linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0 + +/-- 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 := by + cases' S + simp_all only + +/-- An instance providng the operations and properties for `LinSols` to form an + addative commutative monoid. -/ +@[simps!] +instance linSolsAddCommMonoid (χ : ACCSystemLinear) : + AddCommMonoid χ.LinSols where + add S T := ⟨S.val + T.val, by + intro i + rw [(χ.linearACCs i).map_add, S.linearSol i, T.linearSol i] + rfl⟩ + add_comm S T := by + apply LinSols.ext + exact χ.chargesAddCommMonoid.add_comm _ _ + add_assoc S T L := by + apply LinSols.ext + exact χ.chargesAddCommMonoid.add_assoc _ _ _ + zero := ⟨χ.chargesAddCommMonoid.zero, by + intro i + erw [(χ.linearACCs i).map_zero]⟩ + zero_add S := by + apply LinSols.ext + exact χ.chargesAddCommMonoid.zero_add _ + add_zero S := by + apply LinSols.ext + exact χ.chargesAddCommMonoid.add_zero _ + nsmul n S := ⟨n • S.val, by + intro i + rw [nsmul_eq_smul_cast ℚ] + erw [(χ.linearACCs i).map_smul, S.linearSol i] + simp⟩ + nsmul_zero n := by + rfl + nsmul_succ n S := by + apply LinSols.ext + exact χ.chargesAddCommMonoid.nsmul_succ _ _ + +/-- An instance providng the operations and properties for `LinSols` to form an + module over `ℚ`. -/ +@[simps!] +instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where + smul a S := ⟨a • S.val, by + intro i + rw [(χ.linearACCs i).map_smul, S.linearSol i] + simp⟩ + one_smul one_smul := by + apply LinSols.ext + exact χ.chargesModule.one_smul _ + mul_smul a b S := by + apply LinSols.ext + exact χ.chargesModule.mul_smul _ _ _ + smul_zero a := by + apply LinSols.ext + exact χ.chargesModule.smul_zero _ + zero_smul S := by + apply LinSols.ext + exact χ.chargesModule.zero_smul _ + smul_add a S T := by + apply LinSols.ext + exact χ.chargesModule.smul_add _ _ _ + add_smul a b T:= by + apply LinSols.ext + exact χ.chargesModule.add_smul _ _ _ + +/-- An instance providing the operations and properties for `LinSols` to form an + an addative community. -/ +instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols := + Module.addCommMonoidToAddCommGroup ℚ + +/-- The inclusion of `LinSols` into `charges`. -/ +def linSolsIncl (χ : ACCSystemLinear) : χ.LinSols →ₗ[ℚ] χ.charges where + toFun S := S.val + map_add' _ _ := rfl + map_smul' _ _ := rfl + +end ACCSystemLinear + +/-- The type of charges plus the linear ACCs plus the quadratic ACCs. -/ +structure ACCSystemQuad extends ACCSystemLinear where + /-- The number of quadratic ACCs. -/ + numberQuadratic : ℕ + /-- The quadratic ACCs. -/ + quadraticACCs : Fin numberQuadratic → HomogeneousQuadratic toACCSystemCharges.charges + +namespace ACCSystemQuad + +/-- The type of solutions to the linear and quadratic ACCs. -/ +structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where + /-- The condition that the charge satifies the quadratic ACCs. -/ + quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0 + +/-- 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 := by + have h := ACCSystemLinear.LinSols.ext h + cases' S + simp_all only + +/-- 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 , by + intro i + erw [(χ.quadraticACCs i).map_smul] + rw [S.quadSol i] + simp + ⟩ + mul_smul a b S := by + apply QuadSols.ext + exact mul_smul _ _ _ + one_smul S := by + apply QuadSols.ext + exact one_smul _ _ + +/-- The inclusion of quadratic solutions into linear solutions. -/ +def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols where + toFun := QuadSols.toLinSols + map_smul' _ _ := rfl + +/-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion + of linear solutions into quadratic solutions. -/ +def linSolsInclQuadSolsZero (χ : ACCSystemQuad) (h : χ.numberQuadratic = 0) : + χ.LinSols →[ℚ] χ.QuadSols where + toFun S := ⟨S, by intro i; rw [h] at i; exact Fin.elim0 i⟩ + map_smul' _ _ := rfl + +/-- The inclusion of quadratic solutions into all charges. -/ +def quadSolsIncl (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.charges := + MulActionHom.comp χ.linSolsIncl.toMulActionHom χ.quadSolsInclLinSols + +end ACCSystemQuad + +/-- The type of charges plus the anomaly cancellation conditions. -/ +structure ACCSystem extends ACCSystemQuad where + /-- The cubic ACC. -/ + cubicACC : HomogeneousCubic toACCSystemCharges.charges + +namespace ACCSystem + +/-- The type of solutions to the anomaly cancellation conditions. -/ +structure Sols (χ : ACCSystem) extends χ.QuadSols where + /-- The condition that the charge satifies the cubic ACC. -/ + cubicSol : χ.cubicACC val = 0 + +/-- Two solutions are equal if the underlying charges are equal. -/ +lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) : + S = T := by + have h := ACCSystemQuad.QuadSols.ext h + cases' S + simp_all only + +/-- 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 , by + erw [(χ.cubicACC).map_smul] + rw [S.cubicSol] + simp⟩ + mul_smul a b S := by + apply Sols.ext + exact mul_smul _ _ _ + one_smul S := by + apply Sols.ext + exact one_smul _ _ + +/-- The inclusion of `Sols` into `QuadSols`. -/ +def solsInclQuadSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.QuadSols where + toFun := Sols.toQuadSols + map_smul' _ _ := rfl + +/-- The inclusion of `Sols` into `LinSols`. -/ +def solsInclLinSols (χ : ACCSystem) : χ.Sols →[ℚ] χ.LinSols := + MulActionHom.comp χ.quadSolsInclLinSols χ.solsInclQuadSols + +/-- The inclusion of `Sols` into `LinSols`. -/ +def solsIncl (χ : ACCSystem) : χ.Sols →[ℚ] χ.charges := + MulActionHom.comp χ.quadSolsIncl χ.solsInclQuadSols + +/-- The structure of a map between two ACCSystems. -/ +structure Hom (χ η : ACCSystem) where + /-- The linear map between vector spaces of charges. -/ + charges : χ.charges →ₗ[ℚ] η.charges + /-- The map between solutions. -/ + anomalyFree : χ.Sols → η.Sols + /-- The condition that the map commutes with the relevent inclusions. -/ + commute : charges ∘ χ.solsIncl = η.solsIncl ∘ anomalyFree + +/-- The definition of composition between two ACCSystems. -/ +def Hom.comp {χ η ε : ACCSystem} (g : Hom η ε) (f : Hom χ η) : Hom χ ε where + charges := LinearMap.comp g.charges f.charges + anomalyFree := g.anomalyFree ∘ f.anomalyFree + commute := by + simp + rw [Function.comp.assoc] + rw [f.commute, ← Function.comp.assoc, g.commute, Function.comp.assoc] + +end ACCSystem From c7ad21ceb6bcaf1d0ee8856da3bb70e5ccd76676 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 16 Apr 2024 16:04:53 -0400 Subject: [PATCH 2/2] refactor --- HepLean/AnomalyCancellation/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 62d3f06d..4695374f 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -191,7 +191,7 @@ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols wher intro i erw [(χ.quadraticACCs i).map_smul] rw [S.quadSol i] - simp + simp only [mul_zero] ⟩ mul_smul a b S := by apply QuadSols.ext @@ -277,7 +277,7 @@ def Hom.comp {χ η ε : ACCSystem} (g : Hom η ε) (f : Hom χ η) : Hom χ ε charges := LinearMap.comp g.charges f.charges anomalyFree := g.anomalyFree ∘ f.anomalyFree commute := by - simp + simp only [LinearMap.coe_comp] rw [Function.comp.assoc] rw [f.commute, ← Function.comp.assoc, g.commute, Function.comp.assoc]