From e6f12ddae67ea81815cf30f2012c7169e04d8b88 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Apr 2024 11:42:53 -0400
Subject: [PATCH] feat: Add even and odd parameterizations

---
 HepLean.lean                                  |   2 +
 .../PureU1/Even/Parameterization.lean         | 173 ++++++++++++++++++
 .../PureU1/Odd/Parameterization.lean          | 171 +++++++++++++++++
 3 files changed, 346 insertions(+)
 create mode 100644 HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
 create mode 100644 HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean

diff --git a/HepLean.lean b/HepLean.lean
index 5913f05..3c13632 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -15,12 +15,14 @@ import HepLean.AnomalyCancellation.PureU1.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.ConstAbs
 import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Even.Parameterization
 import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
 import HepLean.AnomalyCancellation.PureU1.LowDim.One
 import HepLean.AnomalyCancellation.PureU1.LowDim.Three
 import HepLean.AnomalyCancellation.PureU1.LowDim.Two
 import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
 import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Odd.Parameterization
 import HepLean.AnomalyCancellation.PureU1.Permutations
 import HepLean.AnomalyCancellation.PureU1.Sort
 import HepLean.AnomalyCancellation.PureU1.VectorLike
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
new file mode 100644
index 0000000..4f1a24a
--- /dev/null
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import Mathlib.RepresentationTheory.Basic
+import Mathlib.Tactic.Polyrith
+/-!
+# Parameterization in even case
+
+Given maps `g : Fin n.succ → ℚ`,  `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
+equations. We show that every solution can be got in this way, up to permutation, unless it, up to
+permutaiton, lives in the plane spanned by the firt part of the basis vector.
+
+The main reference is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+
+-/
+
+namespace PureU1
+namespace Even
+
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeEvenPlane
+
+/-- Given coefficents `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
+rational `a ∈ ℚ`, we get a
+point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show extends to an anomaly
+free point. -/
+def parameterizationAsLinear (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
+    (PureU1 (2 * n.succ)).LinSols :=
+  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
+  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+
+lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
+    (parameterizationAsLinear g f a).val =
+    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
+    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+  rw [parameterizationAsLinear]
+  change a • (_ • (P' g).val + _ • (P!' f).val) = _
+  rw [P'_val, P!'_val]
+
+lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ):
+    accCube (2* n.succ) (parameterizationAsLinear g f a).val = 0 := by
+  change accCubeTriLinSymm.toCubic _ = 0
+  rw [parameterizationAsLinear_val, HomogeneousCubic.map_smul,
+    TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube, P!_accCube]
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  ring
+
+/-- The construction of a `Sol` from a `Fin n.succ → ℚ`, a `Fin n → ℚ` and  a `ℚ`. -/
+def parameterization (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
+    (PureU1 (2 * n.succ)).Sols :=
+  ⟨⟨parameterizationAsLinear g f a, by intro i; simp at i; exact Fin.elim0 i⟩,
+  parameterizationCharge_cube g f a⟩
+
+lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}
+    (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (hS : S.val = P g + P! f) :
+    accCubeTriLinSymm (P g, P g, P! f) = - accCubeTriLinSymm (P! f, P! f, P g) := by
+  have hC := S.cubicSol
+  rw [hS] at hC
+  change (accCube (2 * n.succ)) (P g + P! f) = 0 at hC
+  erw [TriLinearSymm.toCubic_add] at hC
+  erw [P_accCube] at hC
+  erw [P!_accCube] at hC
+  linear_combination hC / 3
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case our parameterization above will be able to recover this point. -/
+def genericCase (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+
+lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)
+    (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+  intro g f hS hC
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2] at hC
+  exact hC' hC
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) = 0`.-/
+def specialCase  (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) = 0
+
+lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols)
+    (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+  intro g f hS
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2]
+  exact hC'
+
+lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) :
+    genericCase S ∨ specialCase S := by
+  obtain ⟨g, f, h⟩ := span_basis S.1.1
+  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    exact ne_or_eq _ _
+  cases h1 <;> rename_i h1
+  exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
+  exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
+
+theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : genericCase S) :
+      ∃ g f a,  S = parameterization g f a := by
+  obtain ⟨g, f, hS⟩ := span_basis S.1.1
+  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  rw [parameterization]
+  apply ACCSystem.Sols.ext
+  rw [parameterizationAsLinear_val]
+  change S.val = _ • ( _ • P g + _• P! f)
+  rw [anomalyFree_param _ _ hS]
+  rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
+  exact hS
+  have h := h g f hS
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  exact h
+
+
+lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
+    (h : specialCase S) : lineInCubic S.1.1 := by
+  intro g f hS a b
+  erw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube, P!_accCube]
+  have h := h g f hS
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  rw [h]
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  erw [h]
+  simp
+
+
+lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
+    specialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) :
+    lineInCubicPerm S.1.1 := by
+  intro M
+  exact special_case_lineInCubic (h M)
+
+
+theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
+    specialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M)) :
+    ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
+    ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M).1.1
+    ∈ Submodule.span ℚ (Set.range basis) :=
+  lineInCubicPerm_in_plane S (special_case_lineInCubic_perm h)
+
+end Even
+end PureU1
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
new file mode 100644
index 0000000..5dd63eb
--- /dev/null
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+/-!
+# Parameterization in odd case
+
+Given maps `g : Fin n → ℚ`,  `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
+equations. We show that every solution can be got in this way, up to permutation, unless it is zero.
+
+The main reference is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+
+-/
+namespace PureU1
+namespace Odd
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeOddPlane
+
+/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a linear solution. We will later
+show that this can be extended to a complete solution. -/
+def parameterizationAsLinear (g f : Fin n → ℚ)  (a : ℚ) :
+  (PureU1 (2 * n + 1)).LinSols :=
+  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
+  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+
+lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
+  (parameterizationAsLinear g f a).val =
+    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
+    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+  rw [parameterizationAsLinear]
+  change a • (_ • (P' g).val + _ • (P!' f).val) = _
+  rw [P'_val, P!'_val]
+
+lemma parameterizationCharge_cube (g f : Fin n → ℚ)  (a : ℚ):
+    (accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0 := by
+  change accCubeTriLinSymm.toCubic _ = 0
+  rw [parameterizationAsLinear_val]
+  rw [HomogeneousCubic.map_smul]
+  rw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube g, P!_accCube f]
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  ring
+
+/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a solution. -/
+def parameterization (g f : Fin n → ℚ) (a : ℚ) :
+    (PureU1 (2 * n + 1)).Sols :=
+  ⟨⟨parameterizationAsLinear g f a, by intro i; simp at i; exact Fin.elim0 i⟩,
+  parameterizationCharge_cube g f a⟩
+
+lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
+    (g f : Fin n → ℚ)  (hS : S.val = P g + P! f) :
+    accCubeTriLinSymm (P g, P g, P! f) =
+    - accCubeTriLinSymm (P! f, P! f, P g) := by
+  have hC := S.cubicSol
+  rw [hS] at hC
+  change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC
+  erw [TriLinearSymm.toCubic_add] at hC
+  erw [P_accCube] at hC
+  erw [P!_accCube] at hC
+  linear_combination hC / 3
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case our parameterization above will be able to recover this point. -/
+def genericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
+  ∀ (g f : Fin n.succ → ℚ)  (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+
+lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
+    (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+  intro g f hS hC
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2] at hC
+  exact hC' hC
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case we will show that S is zero if it is true for all permutations. -/
+def specialCase  (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
+  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) = 0
+
+lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
+    (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+  intro g f hS
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2]
+  exact hC'
+
+lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
+    genericCase S ∨ specialCase S := by
+  obtain ⟨g, f, h⟩ := span_basis S.1.1
+  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    exact ne_or_eq _ _
+  cases h1 <;> rename_i h1
+  exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
+  exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
+
+theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : genericCase S) :
+      ∃ g f a,  S = parameterization g f a := by
+  obtain ⟨g, f, hS⟩ := span_basis S.1.1
+  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  rw [parameterization]
+  apply ACCSystem.Sols.ext
+  rw [parameterizationAsLinear_val]
+  change S.val = _ • ( _ • P g + _• P! f)
+  rw [anomalyFree_param _ _ hS]
+  rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
+  exact hS
+  have h := h g f hS
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  exact h
+
+
+lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
+    (h : specialCase S) :
+      lineInCubic S.1.1 := by
+  intro g f hS a b
+  erw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube]
+  erw [P!_accCube]
+  have h := h g f hS
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  rw [h]
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  erw [h]
+  simp
+
+lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ + 1)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
+    specialCase ((FamilyPermutations (2 * n.succ + 1)).solAction.toFun S M)) :
+    lineInCubicPerm S.1.1 := by
+  intro M
+  have hM := special_case_lineInCubic (h M)
+  exact hM
+
+theorem special_case {S : (PureU1 (2 * n.succ.succ + 1)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ + 1)).group),
+    specialCase ((FamilyPermutations (2 * n.succ.succ + 1)).solAction.toFun S M)) :
+    S.1.1 = 0 := by
+  have ht :=  special_case_lineInCubic_perm h
+  exact lineInCubicPerm_zero ht
+end Odd
+end PureU1