feat: Add low dim U(1)

HepLean/AnomalyCancellation/PureU1/LowDim/One.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 1 fermion
+
+We show that in this case the charge must be zero.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+
+namespace One
+
+theorem solEqZero (S : (PureU1 1).LinSols) : S = 0 := by
+  apply ACCSystemLinear.LinSols.ext
+  have hLin := pureU1_linear S
+  simp at hLin
+  funext i
+  simp at i
+  rw [show i = (0 : Fin 1) by omega]
+  exact hLin
+
+end One
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 3 fermion
+
+We show that S is a solution only if one of its charges is zero.
+We define a surjective map from `LinSols` with a charge equal to zero to `Sols`.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+namespace Three
+
+lemma cube_for_linSol' (S : (PureU1 3).LinSols) :
+    3 * S.val (0 : Fin 3) * S.val (1 : Fin 3) * S.val (2 : Fin 3) = 0 ↔
+    (PureU1 3).cubicACC S.val = 0 := by
+  have hL := pureU1_linear S
+  simp at hL
+  rw [Fin.sum_univ_three] at hL
+  change _ ↔ accCube _ _ = _
+  rw [accCube_explicit, Fin.sum_univ_three]
+  rw [show S.val (0 : Fin 3) = - (S.val (1 : Fin 3) + S.val (2 : Fin 3)) by
+      linear_combination hL]
+  ring_nf
+
+lemma cube_for_linSol (S : (PureU1 3).LinSols) :
+    (S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) ↔
+    (PureU1 3).cubicACC S.val = 0 := by
+  rw [← cube_for_linSol']
+  simp only [Fin.isValue, _root_.mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
+  rw [@or_assoc]
+
+lemma three_sol_zero (S : (PureU1 3).Sols) : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0
+    ∨ S.val (2 : Fin 3) = 0 := (cube_for_linSol S.1.1).mpr S.cubicSol
+
+/-- Given a `LinSol` with a charge equal to zero a `Sol`.-/
+def solOfLinear (S : (PureU1 3).LinSols)
+    (hS : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) :
+    (PureU1 3).Sols :=
+  ⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩,
+    (cube_for_linSol S).mp hS⟩
+
+
+theorem solOfLinear_surjects (S : (PureU1 3).Sols) :
+    ∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0
+    ∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S := by
+  use S.1.1
+  use (three_sol_zero S)
+  rfl
+
+end Three
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 2 fermions
+
+We define an equivalence between `LinSols` and `Sols`.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+
+namespace Two
+
+/-- An equivalence between `LinSols` and `Sols`. -/
+def equiv : (PureU1 2).LinSols ≃ (PureU1 2).Sols where
+  toFun S := ⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩, by
+    have hLin := pureU1_linear S
+    simp at hLin
+    erw [accCube_explicit]
+    simp
+    rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) by linear_combination hLin]
+    ring⟩
+  invFun S := S.1.1
+  left_inv S := rfl
+  right_inv S := rfl
+
+end Two
+
+end PureU1