diff --git a/HepLean.lean b/HepLean.lean index e6c9326..9b65669 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -10,6 +10,22 @@ import HepLean.AnomalyCancellation.MSSMNu.Permutations import HepLean.AnomalyCancellation.MSSMNu.PlaneY3B3Orthog import HepLean.AnomalyCancellation.MSSMNu.SolsParameterization import HepLean.AnomalyCancellation.MSSMNu.Y3 +import HepLean.AnomalyCancellation.PureU1.Basic +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 import HepLean.AnomalyCancellation.SM.Basic import HepLean.AnomalyCancellation.SM.FamilyMaps import HepLean.AnomalyCancellation.SM.NoGrav.Basic diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean new file mode 100644 index 0000000..1482a39 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.Basic +import Mathlib.Algebra.Module.Equiv +import Mathlib.Algebra.BigOperators.Ring +import Mathlib.Algebra.BigOperators.Fin +/-! +# Pure U(1) ACC system. + +We define the anomaly cancellation conditions for a pure U(1) gague theory with `n` fermions. + +-/ +universe v u +open Nat + + +open Finset + +namespace PureU1 +open BigOperators + +/-- The vector space of charges. -/ +@[simps!] +def PureU1Charges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk n + +open BigOperators in +/-- The gravitational anomaly. -/ +def accGrav (n : ℕ) : ((PureU1Charges n).charges →ₗ[ℚ] ℚ) where + toFun S := ∑ i : Fin n, S i + map_add' S T := Finset.sum_add_distrib + map_smul' a S := by + simp [HSMul.hSMul, SMul.smul] + rw [← Finset.mul_sum] + + +/-- The symmetric trilinear form used to define the cubic anomaly. -/ +@[simps!] +def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges where + toFun S := ∑ i, S.1 i * S.2.1 i * S.2.2 i + map_smul₁' a S L T := by + simp [HSMul.hSMul] + rw [Finset.mul_sum] + apply Fintype.sum_congr + intro i + ring + map_add₁' S L T R := by + simp only [PureU1Charges_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add] + rw [← Finset.sum_add_distrib] + apply Fintype.sum_congr + intro i + ring + swap₁' S L T := by + simp only [PureU1Charges_numberCharges] + apply Fintype.sum_congr + intro i + ring + swap₂' S L T := by + simp only [PureU1Charges_numberCharges] + apply Fintype.sum_congr + intro i + ring + +lemma accCubeTriLinSymm_cast {n m : ℕ} (h : m = n) + (S : (PureU1Charges n).charges × (PureU1Charges n).charges × (PureU1Charges n).charges) : + accCubeTriLinSymm S = ∑ i : Fin m, + S.1 (Fin.cast h i) * S.2.1 (Fin.cast h i) * S.2.2 (Fin.cast h i) := by + rw [← accCubeTriLinSymm.toFun_eq_coe, accCubeTriLinSymm] + simp only [PureU1Charges_numberCharges] + rw [Finset.sum_equiv (Fin.castIso h).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + +/-- The cubic anomaly equation. -/ +@[simp] +def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).charges) := + (accCubeTriLinSymm).toCubic + + +lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).charges) : + accCube n S = ∑ i : Fin n, S i ^ 3:= by + rw [accCube, TriLinearSymm.toCubic] + change accCubeTriLinSymm.toFun (S, S, S) = _ + rw [accCubeTriLinSymm] + simp only [PureU1Charges_numberCharges] + apply Finset.sum_congr + simp only + ring_nf + simp + +end PureU1 + +/-- The ACC system for a pure $U(1)$ gauge theory with $n$ fermions. -/ +@[simps!] +def PureU1 (n : ℕ) : ACCSystem where + numberLinear := 1 + linearACCs := fun i => + match i with + | 0 => PureU1.accGrav n + numberQuadratic := 0 + quadraticACCs := Fin.elim0 + cubicACC := PureU1.accCube n + +/-- An equivalence of vector spaces of charges when the number of fermions is equal. -/ +def pureU1EqCharges {n m : ℕ} (h : n = m): + (PureU1 n).charges ≃ₗ[ℚ] (PureU1 m).charges where + toFun f := f ∘ Fin.cast h.symm + invFun f := f ∘ Fin.cast h + map_add' _ _ := rfl + map_smul' _ _:= rfl + left_inv _ := rfl + right_inv _ := rfl + +open BigOperators + +lemma pureU1_linear {n : ℕ} (S : (PureU1 n.succ).LinSols) : + ∑ i, S.val i = 0 := by + have hS := S.linearSol + simp at hS + exact hS 0 + +lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) : + ∑ i, (S.val i) ^ 3 = 0 := by + have hS := S.cubicSol + erw [PureU1.accCube_explicit] at hS + exact hS + +lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) : + S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := by + have hS := pureU1_linear S + simp at hS + rw [Fin.sum_univ_castSucc] at hS + linear_combination hS + +lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols} + (h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by + apply ACCSystemLinear.LinSols.ext + funext i + by_cases hi : i ≠ Fin.last n + have hiCast : ∃ j : Fin n, j.castSucc = i := by + exact Fin.exists_castSucc_eq.mpr hi + obtain ⟨j, hj⟩ := hiCast + rw [← hj] + exact h j + simp at hi + rw [hi] + rw [pureU1_last, pureU1_last] + simp only [neg_inj] + apply Finset.sum_congr + simp only + intro j _ + exact h j + +namespace PureU1 + +lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).charges) (j : Fin n) : + (∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := by + induction k + simp + rfl + rename_i k hl + rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc] + have hlt := hl (f ∘ Fin.castSucc) + erw [← hlt] + simp + + +lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : + (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by + induction k + simp + rfl + rename_i k hl + rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc] + have hlt := hl (f ∘ Fin.castSucc) + erw [← hlt] + simp + + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean new file mode 100644 index 0000000..19dbd6f --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean @@ -0,0 +1,163 @@ +/- +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 Mathlib.Tactic.Polyrith +import Mathlib.RepresentationTheory.Basic +/-! +# Basis of `LinSols` + +We give a basis of vector space `LinSols`, and find the rank thereof. + +-/ + +namespace PureU1 + +open BigOperators + +variable {n : ℕ} +namespace BasisLinear + +/-- The basis elements as charges, defined to have a `1` in the `j`th position and a `-1` in the +last position. -/ +@[simp] +def asCharges (j : Fin n) : (PureU1 n.succ).charges := + (fun i => + if i = j.castSucc then + 1 + else + if i = Fin.last n then + - 1 + else + 0) + +lemma asCharges_eq_castSucc (j : Fin n) : + asCharges j (Fin.castSucc j) = 1 := by + simp [asCharges] + +lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) : + asCharges k (Fin.castSucc j) = 0 := by + simp [asCharges] + split + rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + split + rename_i h1 h2 + rw [Fin.ext_iff] at h1 h2 + simp at h1 h2 + have hj : j.val < n := by + exact j.prop + simp_all + rfl + +/-- The basis elements as `LinSols`. -/ +@[simps!] +def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols := + ⟨asCharges j, by + intro i + simp at i + match i with + | 0 => + simp only [ Fin.isValue, PureU1_linearACCs, accGrav, + LinearMap.coe_mk, AddHom.coe_mk, Fin.coe_eq_castSucc] + rw [Fin.sum_univ_castSucc] + rw [Finset.sum_eq_single j] + simp only [asCharges, PureU1_numberCharges, ↓reduceIte] + have hn : ¬ (Fin.last n = Fin.castSucc j) := by + have hj := j.prop + rw [Fin.ext_iff] + simp only [Fin.val_last, Fin.coe_castSucc, ne_eq] + omega + split + rename_i ht + exact (hn ht).elim + rfl + intro k _ hkj + exact asCharges_ne_castSucc hkj.symm + intro hk + simp at hk⟩ + + +lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : + (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by + induction k + simp + rfl + rename_i k l hl + rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc] + have hlt := hl (f ∘ Fin.castSucc) + erw [← hlt] + simp + +/-- The coordinate map for the basis. -/ +noncomputable +def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where + toFun S := Finsupp.equivFunOnFinite.invFun (S.1 ∘ Fin.castSucc) + map_add' S T := by + simp only [PureU1_numberCharges, ACCSystemLinear.linSolsAddCommMonoid_add_val, + Equiv.invFun_as_coe] + ext + simp + map_smul' a S := by + simp only [PureU1_numberCharges, Equiv.invFun_as_coe, eq_ratCast, Rat.cast_eq_id, id_eq] + ext + simp + rfl + invFun f := ∑ i : Fin n, f i • asLinSols i + left_inv S := by + simp only [PureU1_numberCharges, Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_toFun, + Function.comp_apply] + apply pureU1_anomalyFree_ext + intro j + rw [sum_of_vectors] + simp only [HSMul.hSMul, SMul.smul, PureU1_numberCharges, + asLinSols_val, Equiv.toFun_as_coe, + Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe] + rw [Finset.sum_eq_single j] + simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one] + intro k _ hkj + rw [asCharges_ne_castSucc hkj] + simp only [mul_zero] + simp + right_inv f := by + simp only [PureU1_numberCharges, Equiv.invFun_as_coe] + ext + rename_i j + simp only [Finsupp.equivFunOnFinite_symm_apply_toFun, Function.comp_apply] + rw [sum_of_vectors] + simp only [HSMul.hSMul, SMul.smul, PureU1_numberCharges, + asLinSols_val, Equiv.toFun_as_coe, + Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe] + rw [Finset.sum_eq_single j] + simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one] + intro k _ hkj + rw [asCharges_ne_castSucc hkj] + simp only [mul_zero] + simp + +/-- The basis of `LinSols`.-/ +noncomputable +def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where + repr := coordinateMap + +instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) := + Module.Finite.of_basis asBasis + +lemma finrank_AnomalyFreeLinear : + FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by + have h := Module.mk_finrank_eq_card_basis (@asBasis n) + simp_all + simp [FiniteDimensional.finrank] + rw [h] + simp_all only [Cardinal.toNat_natCast] + + +end BasisLinear + + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean new file mode 100644 index 0000000..1acdccc --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -0,0 +1,282 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.VectorLike +/-! +# Charges assignments with constant abs + +We look at charge assignments in which all charges have the same absolute value. + +-/ +universe v u + +open Nat +open Finset +open BigOperators + +namespace PureU1 + +variable {n : ℕ} + +/-- The condition for two rationals to have the same square (equivalent to same abs). -/ +def constAbsProp : ℚ × ℚ → Prop := fun s => s.1^2 = s.2^2 + +/-- The condition on a charge assigment `S` to have constant absolute value among charges. -/ +@[simp] +def constAbs (S : (PureU1 n).charges) : Prop := ∀ i j, (S i) ^ 2 = (S j) ^ 2 + +lemma constAbs_perm (S : (PureU1 n).charges) (M :(FamilyPermutations n).group) : + constAbs ((FamilyPermutations n).rep M S) ↔ constAbs S := by + simp only [constAbs, PureU1_numberCharges, FamilyPermutations, permGroup, permCharges, + MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply] + apply Iff.intro + intro h i j + have h2 := h (M.toFun i) (M.toFun j) + simp at h2 + exact h2 + intro h i j + exact h (M.invFun i) (M.invFun j) + +lemma constAbs_sort {S : (PureU1 n).charges} (CA : constAbs S) : constAbs (sort S) := by + rw [sort] + exact (constAbs_perm S _).mpr CA + +/-- The condition for a set of charges to be `sorted`, and have `constAbs`-/ +def constAbsSorted (S : (PureU1 n).charges) : Prop := constAbs S ∧ sorted S + +namespace constAbsSorted +section charges + +variable {S : (PureU1 n.succ).charges} {A : (PureU1 n.succ).LinSols} +variable (hS : constAbsSorted S) (hA : constAbsSorted A.val) + +lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := by + have hSS := hS.2 i k hik + have ht := hS.1 i k + rw [sq_eq_sq_iff_eq_or_eq_neg] at ht + cases ht <;> rename_i h + exact h + linarith + +lemma val_le_zero {i : Fin n.succ} (hi : S i ≤ 0) : S i = S (0 : Fin n.succ) := by + symm + apply lt_eq hS hi + simp + +lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by + have hSS := hS.2 k i hik + have ht := hS.1 i k + rw [sq_eq_sq_iff_eq_or_eq_neg] at ht + cases ht <;> rename_i h + exact h + linarith + +lemma zero_gt (h0 : 0 ≤ S (0 : Fin n.succ)) (i : Fin n.succ) : S (0 : Fin n.succ) = S i := by + symm + refine gt_eq hS h0 ?_ + simp + +lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = - S j := by + have hSS := hS.1 i j + rw [sq_eq_sq_iff_eq_or_eq_neg] at hSS + cases' hSS with h h + simp_all + linarith + exact h + +lemma is_zero (h0 : S (0 : Fin n.succ) = 0) : S = 0 := by + funext i + have ht := hS.1 i (0 : Fin n.succ) + rw [h0] at ht + simp at ht + exact ht + +/-- A boundary of `S : (PureU1 n.succ).charges` (assumed sorted, constAbs and non-zero) +is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ` are different signs. + -/ +@[simp] +def boundary (S : (PureU1 n.succ).charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ + +lemma boundary_castSucc {k : Fin n} (hk : boundary S k) : S k.castSucc = S (0 : Fin n.succ) := + (lt_eq hS (le_of_lt hk.left) (by simp : 0 ≤ k.castSucc)).symm + +lemma boundary_succ {k : Fin n} (hk : boundary S k) : S k.succ = - S (0 : Fin n.succ) := by + have hn := boundary_castSucc hS hk + rw [opposite_signs_eq_neg hS (le_of_lt hk.left) (le_of_lt hk.right)] at hn + linear_combination -(1 * hn) + +lemma boundary_split (k : Fin n) : k.succ.val + (n.succ - k.succ.val) = n.succ := by + omega + +lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S = + ∑ i : Fin (k.succ.val + (n.succ - k.succ.val)), S (Fin.cast (boundary_split k) i) := by + simp [accGrav] + erw [Finset.sum_equiv (Fin.castIso (boundary_split k)).toEquiv] + intro i + simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv] + intro i + simp + rfl + +lemma boundary_accGrav'' (k : Fin n) (hk : boundary S k) : + accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by + rw [boundary_accGrav' k] + rw [Fin.sum_univ_add] + have hfst (i : Fin k.succ.val) : + S (Fin.cast (boundary_split k) (Fin.castAdd (n.succ - k.succ.val) i)) = S k.castSucc := by + apply lt_eq hS (le_of_lt hk.left) (by rw [Fin.le_def]; simp; omega) + have hsnd (i : Fin (n.succ - k.succ.val)) : + S (Fin.cast (boundary_split k) (Fin.natAdd (k.succ.val) i)) = S k.succ := by + apply gt_eq hS (le_of_lt hk.right) (by rw [Fin.le_def]; simp) + simp only [hfst, hsnd] + simp only [Fin.val_succ, sum_const, card_fin, nsmul_eq_mul, cast_add, cast_one, + succ_sub_succ_eq_sub, Fin.is_le', cast_sub] + rw [boundary_castSucc hS hk, boundary_succ hS hk] + ring + +/-- We say a `S ∈ charges` has a boundry if there exists a `k ∈ Fin n` which is a boundary. -/ +@[simp] +def hasBoundary (S : (PureU1 n.succ).charges) : Prop := + ∃ (k : Fin n), boundary S k + +lemma not_hasBoundary_zero_le (hnot : ¬ (hasBoundary S)) (h0 : S (0 : Fin n.succ) < 0) : + ∀ i, S (0 : Fin n.succ) = S i := by + intro ⟨i, hi⟩ + simp at hnot + induction i + rfl + rename_i i hii + have hnott := hnot ⟨i, by {simp at hi; linarith} ⟩ + have hii := hii (by omega) + erw [← hii] at hnott + exact (val_le_zero hS (hnott h0)).symm + +lemma not_hasBoundry_zero (hnot : ¬ (hasBoundary S)) (i : Fin n.succ) : + S (0 : Fin n.succ) = S i := by + by_cases hi : S (0 : Fin n.succ) < 0 + exact not_hasBoundary_zero_le hS hnot hi i + simp at hi + exact zero_gt hS hi i + +lemma not_hasBoundary_grav (hnot : ¬ (hasBoundary S)) : + accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by + simp [accGrav, ← not_hasBoundry_zero hS hnot] + + +lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : hasBoundary A.val := by + by_contra hn + have h0 := not_hasBoundary_grav hA hn + simp [accGrav] at h0 + erw [pureU1_linear A] at h0 + simp at h0 + cases' h0 + linarith + simp_all + +lemma AFL_odd_noBoundary {A : (PureU1 (2 * n + 1)).LinSols} (h : constAbsSorted A.val) + (hA : A.val (0 : Fin (2*n +1)) ≠ 0) : ¬ hasBoundary A.val := by + by_contra hn + obtain ⟨k, hk⟩ := hn + have h0 := boundary_accGrav'' h k hk + simp [accGrav] at h0 + erw [pureU1_linear A] at h0 + simp [hA] at h0 + have h1 : 2 * n = 2 * k.val + 1 := by + rw [← @Nat.cast_inj ℚ] + simp only [cast_mul, cast_ofNat, cast_add, cast_one] + linear_combination - h0 + omega + +lemma AFL_odd_zero {A : (PureU1 (2 * n + 1)).LinSols} (h : constAbsSorted A.val) : + A.val (0 : Fin (2 * n + 1)) = 0 := by + by_contra hn + exact (AFL_odd_noBoundary h hn ) (AFL_hasBoundary h hn) + +theorem AFL_odd (A : (PureU1 (2 * n + 1)).LinSols) (h : constAbsSorted A.val) : + A = 0 := by + apply ACCSystemLinear.LinSols.ext + exact is_zero h (AFL_odd_zero h) + +lemma AFL_even_Boundary {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val) + (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) {k : Fin (2 * n + 1)} (hk : boundary A.val k) : + k.val = n := by + have h0 := boundary_accGrav'' h k hk + change ∑ i : Fin (succ (Nat.mul 2 n + 1)), A.val i = _ at h0 + erw [pureU1_linear A] at h0 + simp [hA] at h0 + rw [← @Nat.cast_inj ℚ] + linear_combination h0 / 2 + +lemma AFL_even_below' {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val) + (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) (i : Fin n.succ) : + A.val (Fin.cast (split_equal n.succ) (Fin.castAdd n.succ i)) = A.val (0 : Fin (2*n.succ)) := by + obtain ⟨k, hk⟩ := AFL_hasBoundary h hA + rw [← boundary_castSucc h hk] + apply lt_eq h (le_of_lt hk.left) + rw [Fin.le_def] + simp only [PureU1_numberCharges, Fin.coe_cast, Fin.coe_castAdd, mul_eq, Fin.coe_castSucc] + rw [AFL_even_Boundary h hA hk] + omega + +lemma AFL_even_below (A : (PureU1 (2 * n.succ)).LinSols) (h : constAbsSorted A.val) + (i : Fin n.succ) : + A.val (Fin.cast (split_equal n.succ) (Fin.castAdd n.succ i)) + = A.val (0 : Fin (2*n.succ)) := by + by_cases hA : A.val (0 : Fin (2*n.succ)) = 0 + rw [is_zero h hA] + simp + rfl + exact AFL_even_below' h hA i + +lemma AFL_even_above' {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val) + (hA : A.val (0 : Fin (2*n.succ)) ≠ 0) (i : Fin n.succ) : + A.val (Fin.cast (split_equal n.succ) (Fin.natAdd n.succ i)) = + - A.val (0 : Fin (2*n.succ)) := by + obtain ⟨k, hk⟩ := AFL_hasBoundary h hA + rw [← boundary_succ h hk] + apply gt_eq h (le_of_lt hk.right) + rw [Fin.le_def] + simp only [mul_eq, Fin.val_succ, PureU1_numberCharges, Fin.coe_cast, Fin.coe_natAdd] + rw [AFL_even_Boundary h hA hk] + omega + +lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : constAbsSorted A.val) + (i : Fin n.succ) : + A.val (Fin.cast (split_equal n.succ) (Fin.natAdd n.succ i)) = + - A.val (0 : Fin (2*n.succ)) := by + by_cases hA : A.val (0 : Fin (2*n.succ)) = 0 + rw [is_zero h hA] + simp + rfl + exact AFL_even_above' h hA i + + +end charges + +end constAbsSorted + + +namespace ConstAbs + +theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : constAbs S.val) : + S = 0 := + have hS := And.intro (constAbs_sort hs) (sort_sorted S.val) + sortAFL_zero S (constAbsSorted.AFL_odd (sortAFL S) hS) + + +theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : constAbs S.val) : + vectorLikeEven S.val := by + have hS := And.intro (constAbs_sort hs) (sort_sorted S.val) + intro i + have h1 := constAbsSorted.AFL_even_below (sortAFL S) hS + have h2 := constAbsSorted.AFL_even_above (sortAFL S) hS + rw [sortAFL_val] at h1 h2 + rw [h1, h2] + simp + +end ConstAbs + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean new file mode 100644 index 0000000..1963a5f --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean @@ -0,0 +1,759 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.BasisLinear +import HepLean.AnomalyCancellation.PureU1.VectorLike +import Mathlib.Logic.Equiv.Fin +/-! +# Basis of `LinSols` in the even case + +We give a basis of `LinSols` in the even case. This basis has the special propoerty +that splits into two planes on which every point is a solution to the ACCs. +-/ +universe v u + +open Nat +open Finset +open BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeEvenPlane + +lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by + linarith + +section theδs + +/-- A helper function for what follows. -/ +def δ₁ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j) + +/-- A helper function for what follows. -/ +def δ₂ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j) + +/-- A helper function for what follows. -/ +def δ!₁ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n) + (Fin.natAdd 1 (Fin.castAdd 1 (Fin.castAdd n j))) + +/-- A helper function for what follows. -/ +def δ!₂ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n) + (Fin.natAdd 1 (Fin.castAdd 1 (Fin.natAdd n j))) + +/-- A helper function for what follows. -/ +def δ!₃ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0)) + +/-- A helper function for what follows. -/ +def δ!₄ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0))) + +lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ₁ i)) + (h2 : ∀ i, S (δ₂ i) = T (δ₂ i)) : S = T := by + funext i + by_cases hi : i.val < n.succ + let j : Fin n.succ := ⟨i, hi⟩ + have h2 := h1 j + have h3 : δ₁ j = i := by + simp [δ₁, Fin.ext_iff] + rw [h3] at h2 + exact h2 + let j : Fin n.succ := ⟨i - n.succ, by omega⟩ + have h2 := h2 j + have h3 : δ₂ j = i := by + simp [δ₂, Fin.ext_iff] + omega + rw [h3] at h2 + exact h2 + +lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) : + ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by + have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by + rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + rw [h1] + rw [Fin.sum_univ_add, Finset.sum_add_distrib] + rfl + +lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) : + ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by + have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by + rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + rw [h1] + rw [Fin.sum_univ_add, Finset.sum_add_distrib] + rfl + +lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) : + ∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by + have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by + rw [Finset.sum_equiv (Fin.castIso (n_cond₂ n)).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + rw [h1] + rw [Fin.sum_univ_add, Fin.sum_univ_add, Fin.sum_univ_add, Finset.sum_add_distrib] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + repeat rw [Rat.add_assoc] + apply congrArg + rw [Rat.add_comm] + rw [← Rat.add_assoc] + nth_rewrite 2 [Rat.add_comm] + repeat rw [Rat.add_assoc] + nth_rewrite 2 [Rat.add_comm] + rfl + +lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := by + rfl + +lemma δ!₄_δ₂Last: @δ!₄ n = δ₂ (Fin.last n) := by + rw [Fin.ext_iff] + simp [δ!₄, δ₂] + omega + +lemma δ!₁_δ₁ (j : Fin n) : δ!₁ j = δ₁ j.succ := by + rw [Fin.ext_iff, δ₁, δ!₁] + simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_succ] + ring + +lemma δ!₂_δ₂ (j : Fin n) : δ!₂ j = δ₂ j.castSucc := by + rw [Fin.ext_iff, δ₂, δ!₂] + simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.coe_castSucc] + ring_nf + rw [Nat.succ_eq_add_one] + ring + +end theδs + +/-- The first part of the basis as charges. -/ +def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).charges := + fun i => + if i = δ₁ j then + 1 + else + if i = δ₂ j then + - 1 + else + 0 + +/-- The second part of the basis as charges. -/ +def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).charges := + fun i => + if i = δ!₁ j then + 1 + else + if i = δ!₂ j then + - 1 + else + 0 + +lemma basis_on_δ₁_self (j : Fin n.succ) : basisAsCharges j (δ₁ j) = 1 := by + simp [basisAsCharges] + +lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by + simp [basis!AsCharges] + +lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) : + basisAsCharges k (δ₁ j) = 0 := by + simp [basisAsCharges] + simp [δ₁, δ₂] + split + rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + split + rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp at h2 + omega + rfl + +lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) : + basisAsCharges k j = 0 := by + simp [basisAsCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) : + basis!AsCharges k j = 0 := by + simp [basis!AsCharges] + simp_all only [ne_eq, ↓reduceIte] + + +lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) : + basis!AsCharges k (δ!₁ j) = 0 := by + simp [basis!AsCharges] + simp [δ!₁, δ!₂] + split + rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + split + rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp at h2 + omega + rfl + +lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) : + basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by + simp [basisAsCharges, δ₂, δ₁] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals rename_i h1 h2 + all_goals rw [Fin.ext_iff] at h1 h2 + all_goals simp_all + all_goals rename_i h3 + all_goals rw [Fin.ext_iff] at h3 + all_goals simp_all + all_goals omega + +lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) : + basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by + simp [basis!AsCharges, δ!₂, δ!₁] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals rename_i h1 h2 + all_goals rw [Fin.ext_iff] at h1 h2 + all_goals simp_all + subst h1 + exact Fin.elim0 i + all_goals rename_i h3 + all_goals rw [Fin.ext_iff] at h3 + all_goals simp_all + all_goals omega + +lemma basis_on_δ₂_self (j : Fin n.succ) : basisAsCharges j (δ₂ j) = - 1 := by + rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self] + +lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by + rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self] + +lemma basis_on_δ₂_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by + rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h] + rfl + +lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by + rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h] + rfl + +lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by + simp [basis!AsCharges] + split <;> rename_i h + rw [Fin.ext_iff] at h + simp [δ!₃, δ!₁] at h + omega + split <;> rename_i h2 + rw [Fin.ext_iff] at h2 + simp [δ!₃, δ!₂] at h2 + omega + rfl + +lemma basis!_on_δ!₄ (j : Fin n) : basis!AsCharges j δ!₄ = 0 := by + simp [basis!AsCharges] + split <;> rename_i h + rw [Fin.ext_iff] at h + simp [δ!₄, δ!₁] at h + omega + split <;> rename_i h2 + rw [Fin.ext_iff] at h2 + simp [δ!₄, δ!₂] at h2 + omega + rfl + +lemma basis_linearACC (j : Fin n.succ) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ₁_δ₂] + simp [basis_δ₂_eq_minus_δ₁] + +lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄] + simp [basis!_δ!₂_eq_minus_δ!₁] + +lemma basis_accCube (j : Fin n.succ) : + accCube (2 * n.succ) (basisAsCharges j) = 0 := by + rw [accCube_explicit, sum_δ₁_δ₂] + apply Finset.sum_eq_zero + intro i _ + simp [basis_δ₂_eq_minus_δ₁] + ring + +lemma basis!_accCube (j : Fin n) : + accCube (2 * n.succ) (basis!AsCharges j) = 0 := by + rw [accCube_explicit, sum_δ!₁_δ!₂] + rw [basis!_on_δ!₄, basis!_on_δ!₃] + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply, + zero_add] + apply Finset.sum_eq_zero + intro i _ + simp [basis!_δ!₂_eq_minus_δ!₁] + ring + + +/-- The first part of the basis as `LinSols`. -/ +@[simps!] +def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := + ⟨basisAsCharges j, by + intro i + simp at i + match i with + | 0 => + exact basis_linearACC j⟩ + +/-- The second part of the basis as `LinSols`. -/ +@[simps!] +def basis! (j : Fin n) : (PureU1 (2 * n.succ)).LinSols := + ⟨basis!AsCharges j, by + intro i + simp at i + match i with + | 0 => + exact basis!_linearACC j⟩ + +/-- The whole basis as `LinSols`. -/ +def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i => + match i with + | .inl i => basis i + | .inr i => basis! i + +/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/ +lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) + (hS : ((FamilyPermutations (2 * n.succ)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j))) S = S') : + S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by + funext i + rw [← hS, FamilyPermutations_anomalyFreeLinear_apply] + by_cases hi : i = δ!₁ j + subst hi + simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst] + by_cases hi2 : i = δ!₂ j + subst hi2 + simp [HSMul.hSMul, basis!_on_δ!₂_self, pairSwap_inv_snd] + simp [HSMul.hSMul] + rw [basis!_on_other hi hi2] + change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_ + erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)] + simp + +/-- A point in the span of the first part of the basis as a charge. -/ +def P (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).charges := ∑ i, f i • basisAsCharges i + +/-- A point in the span of the second part of the basis as a charge. -/ +def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).charges := ∑ i, f i • basis!AsCharges i + +/-- A point in the span of the basis as a charge. -/ +def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).charges := P f + P! g + +lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j := by + rw [P, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis_on_δ₁_self] + simp only [mul_one] + intro k _ hkj + rw [basis_on_δ₁_other hkj] + simp only [mul_zero] + simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff] + +lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis!_on_δ!₁_self] + simp only [mul_one] + intro k _ hkj + rw [basis!_on_δ!₁_other hkj] + simp only [mul_zero] + simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff] + +lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : + Pa f g (δ!₁ j) = f j.succ + g j := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [P!_δ!₁, δ!₁_δ₁, P_δ₁] + +lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j := by + rw [P, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis_on_δ₂_self] + simp only [mul_neg, mul_one] + intro k _ hkj + rw [basis_on_δ₂_other hkj] + simp only [mul_zero] + simp + +lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis!_on_δ!₂_self] + simp only [mul_neg, mul_one] + intro k _ hkj + rw [basis!_on_δ!₂_other hkj] + simp only [mul_zero] + simp + +lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : + Pa f g (δ!₂ j) = - f j.castSucc - g j := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [P!_δ!₂, δ!₂_δ₂, P_δ₂] + ring + +lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃] + +lemma Pa_δ!₃ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₃) = f 0 := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁] + simp + +lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₄] + +lemma Pa_δ!₄ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₄) = - f (Fin.last n) := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂] + simp + +lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ) : P f ∘ δ₂ = - P f ∘ δ₁ := by + funext j + simp only [PureU1_numberCharges, Function.comp_apply, Pi.neg_apply] + rw [P_δ₁, P_δ₂] + +lemma P_linearACC (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ₁_δ₂] + simp [P_δ₂, P_δ₁] + +lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by + rw [accCube_explicit, sum_δ₁_δ₂] + apply Finset.sum_eq_zero + intro i _ + simp [P_δ₁, P_δ₂] + ring + +lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by + rw [accCube_explicit, sum_δ!₁_δ!₂, P!_δ!₃, P!_δ!₄] + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply, + zero_add] + apply Finset.sum_eq_zero + intro i _ + simp [P!_δ!₁, P!_δ!₂] + ring + +lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) : + accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) + = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by + simp [accCubeTriLinSymm] + rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄] + simp only [mul_zero, add_zero, Function.comp_apply, zero_add] + rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self] + simp [δ!₁_δ₁, δ!₂_δ₂] + rw [P_δ₁, P_δ₂] + ring + intro k _ hkj + erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm] + simp only [mul_zero, add_zero] + simp + +lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) : + accCubeTriLinSymm.toFun (P! g, P! g, basisAsCharges j) + = (P! g (δ₁ j))^2 - (P! g (δ₂ j))^2 := by + simp [accCubeTriLinSymm] + rw [sum_δ₁_δ₂] + simp only [Function.comp_apply] + rw [Finset.sum_eq_single j, basis_on_δ₁_self, basis_on_δ₂_self] + simp [δ!₁_δ₁, δ!₂_δ₂] + ring + intro k _ hkj + erw [basis_on_δ₁_other hkj.symm, basis_on_δ₂_other hkj.symm] + simp only [mul_zero, add_zero] + simp + +lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by + intro i + erw [← P_δ₁ f] + rw [h] + rfl + +lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by + intro i + rw [← P!_δ!₁ f] + rw [h] + rfl + +lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) : + ∀ i, f i = 0 := by + have h₃ := Pa_δ!₃ f g + rw [h] at h₃ + change 0 = f 0 at h₃ + intro i + have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by + induction iv + exact h₃.symm + rename_i iv hi + have hivi : iv < n.succ := by omega + have hi2 := hi hivi + have h1 := Pa_δ!₁ f g ⟨iv, by omega⟩ + have h2 := Pa_δ!₂ f g ⟨iv, by omega⟩ + rw [h] at h1 h2 + simp at h1 h2 + erw [hi2] at h2 + change 0 = _ at h2 + simp at h2 + rw [h2] at h1 + simp at h1 + exact h1.symm + exact hinduc i.val i.prop + +lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) : + ∀ i, g i = 0 := by + have hf := Pa_zero f g h + rw [Pa, P] at h + simp [hf] at h + exact P!_zero g h + +/-- A point in the span of the first part of the basis. -/ +def P' (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis i + +/-- A point in the span of the second part of the basis. -/ +def P!' (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis! i + +/-- A point in the span of the whole basis. -/ +def Pa' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n.succ)).LinSols := + ∑ i, f i • basisa i + +lemma Pa'_P'_P!' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : + Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by + exact Fintype.sum_sum_type _ + +lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by + simp [P', P] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + simp [HSMul.hSMul] + +lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by + simp [P!', P!] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + simp [HSMul.hSMul] + +theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change P' f = 0 at h + have h1 : (P' f).val = 0 := by + simp [h] + rfl + rw [P'_val] at h1 + exact P_zero f h1 + +theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change P!' f = 0 at h + have h1 : (P!' f).val = 0 := by + simp [h] + rfl + rw [P!'_val] at h1 + exact P!_zero f h1 + + +theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change Pa' f = 0 at h + have h1 : (Pa' f).val = 0 := by + simp [h] + rfl + rw [Pa'_P'_P!'] at h1 + change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1 + rw [P!'_val, P'_val] at h1 + change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 + have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + intro i + simp_all + cases i + simp_all + simp_all + +lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by + apply Iff.intro + intro h + funext i + rw [Pa', Pa'] at h + have h1 : ∑ i : Fin (succ n) ⊕ Fin n, (f i + (- f' i)) • basisa i = 0 := by + simp only [add_smul, neg_smul] + rw [Finset.sum_add_distrib] + rw [h] + rw [← Finset.sum_add_distrib] + simp + have h2 : ∀ i, (f i + (- f' i)) = 0 := by + exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n)) + (fun i => f i + -f' i) h1 + have h2i := h2 i + linarith + intro h + rw [h] + +/-- A helper function for what follows. TODO: replace this with mathlib functions. -/ +def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : (Fin n.succ) ⊕ (Fin n) → ℚ := fun i => + match i with + | .inl i => g i + | .inr i => f i + +lemma join_ext (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : + join g f = join g' f' ↔ g = g' ∧ f = f' := by + apply Iff.intro + intro h + apply And.intro + funext i + exact congr_fun h (Sum.inl i) + funext i + exact congr_fun h (Sum.inr i) + intro h + rw [h.left, h.right] + +lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : + Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by + apply Iff.intro + intro h + rw [Pa'_eq] at h + rw [join_ext] at h + rw [h.left, h.right] + intro h + apply ACCSystemLinear.LinSols.ext + rw [Pa'_P'_P!', Pa'_P'_P!'] + simp [P'_val, P!'_val] + exact h + +lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : + Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by + rw [← join_Pa] + rw [← join_ext] + exact Pa'_eq _ _ + + +lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) = + FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by + erw [BasisLinear.finrank_AnomalyFreeLinear] + simp only [Fintype.card_sum, Fintype.card_fin, mul_eq] + omega + +/-- The basis formed out of our basisa vectors. -/ +noncomputable def basisaAsBasis : + Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols := + basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card + + +lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : + ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f := by + have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S) + obtain ⟨f, hf⟩ := h + simp [basisaAsBasis] at hf + change P' _ + P!' _ = S at hf + use f ∘ Sum.inl + use f ∘ Sum.inr + rw [← hf] + simp [P'_val, P!'_val] + rfl + +lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by + rw [(mem_span_range_iff_exists_fun ℚ)] + use f + rfl + +lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ )).LinSols) (j : Fin n) : + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈ + Submodule.span ℚ (Set.range basis!AsCharges) := by + apply Submodule.smul_mem + apply SetLike.mem_of_subset + apply Submodule.subset_span + simp_all only [Set.mem_range, exists_apply_eq_apply] + +lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) + (hS : ((FamilyPermutations (2 * n.succ)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ) + (h : S.val = P g + P! f): + ∃ + (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ) , + S'.val = P g' + P! f' ∧ P! f' = P! f + + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by + let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j + have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by + apply Submodule.add_mem + exact (P!_in_span f) + exact (smul_basis!AsCharges_in_span S j) + have hXsum := (mem_span_range_iff_exists_fun ℚ).mp hX + obtain ⟨f', hf'⟩ := hXsum + use g + use f' + change P! f' = _ at hf' + erw [hf'] + simp only [and_self, and_true] + change S'.val = P g + (P! f + _) + rw [← add_assoc, ← h] + apply swap!_as_add at hS + exact hS + +lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) + (hS : vectorLikeEven S.val) : + ∃ (M : (FamilyPermutations (2 * n.succ)).group), + (FamilyPermutations (2 * n.succ)).linSolRep M S + ∈ Submodule.span ℚ (Set.range basis) := by + use (Tuple.sort S.val).symm + change sortAFL S ∈ Submodule.span ℚ (Set.range basis) + rw [mem_span_range_iff_exists_fun ℚ] + let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (δ₁ i) + use f + apply ACCSystemLinear.LinSols.ext + rw [sortAFL_val] + erw [P'_val] + apply ext_δ + intro i + rw [P_δ₁] + rfl + intro i + rw [P_δ₂] + have ht := hS i + change sort S.val (δ₁ i) = - sort S.val (δ₂ i) at ht + have h : sort S.val (δ₂ i) = - sort S.val (δ₁ i) := by + rw [ht] + ring + rw [h] + simp + rfl + +end VectorLikeEvenPlane + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean new file mode 100644 index 0000000..d439440 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean @@ -0,0 +1,174 @@ +/- +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.Even.BasisLinear +import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond +import HepLean.AnomalyCancellation.PureU1.Permutations +import Mathlib.RepresentationTheory.Basic +import Mathlib.Tactic.Polyrith +/-! + +# Line In Cubic Even case + +We say that a linear solution satisfies the `lineInCubic` property +if the line through that point and through the two different planes formed by the baisis of +`LinSols` lies in the cubic. + +We show that for a solution all its permutations satsfiy this property, then there exists +a permutation for which it lies in the plane spanned by the first part of the basis. + +The main reference for this file is: + +- https://arxiv.org/pdf/1912.04804.pdf +-/ + +namespace PureU1 +namespace Even + +open BigOperators + +variable {n : ℕ} +open VectorLikeEvenPlane + +/-- A property on `LinSols`, statified if every point on the line between the two planes +in the basis through that point is in the cubic. -/ +def lineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop := + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) , + accCube (2 * n.succ) (a • P g + b • P! f) = 0 + +lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) : + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) , + 3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f) + + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by + intro g f hS a b + have h1 := h g f hS a b + change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1 + simp only [TriLinearSymm.toCubic_add] at h1 + simp only [HomogeneousCubic.map_smul, + accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 + erw [P_accCube, P!_accCube] at h1 + rw [← h1] + ring + +/-- + This lemma states that for a given `S` of type `(PureU1 (2 * n.succ)).AnomalyFreeLinear` and + a proof `h` that the line through `S` lies on a cubic curve, + for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if `S.val = P g + P! f`, + then `accCubeTriLinSymm.toFun (P g, P g, P! f) = 0`. +-/ +lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) : + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), + accCubeTriLinSymm (P g, P g, P! f) = 0 := by + intro g f hS + linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) - + (lineInCubic_expand h g f hS 1 2) / 6 + +/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/ +def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop := + ∀ (M : (FamilyPermutations (2 * n.succ)).group ), + lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S) + +/-- If `lineInCubicPerm S` then `lineInCubic S`. -/ +lemma lineInCubicPerm_self {S : (PureU1 (2 * n.succ)).LinSols} + (hS : lineInCubicPerm S) : lineInCubic S := hS 1 + +/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/ +lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols} + (hS : lineInCubicPerm S) (M' : (FamilyPermutations (2 * n.succ)).group) : + lineInCubicPerm ((FamilyPermutations (2 * n.succ)).linSolRep M' S) := by + rw [lineInCubicPerm] + intro M + change lineInCubic + (((FamilyPermutations (2 * n.succ)).linSolRep M * + (FamilyPermutations (2 * n.succ)).linSolRep M') S) + erw [← (FamilyPermutations (2 * n.succ)).linSolRep.map_mul M M'] + exact hS (M * M') + +lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols} + (LIC : lineInCubicPerm S) : + ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) , + (S.val (δ!₂ j) - S.val (δ!₁ j)) + * accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by + intro j g f h + let S' := (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S + have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl + obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h + have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h + have h2 := line_in_cubic_P_P_P! + (lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1 + rw [hall.2.1, hall.2.2] at h2 + rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2 + simpa using h2 + +lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ )).LinSols} + (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) : + accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges (Fin.last n)) = + - (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ + + S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) := by + rw [P_P_P!_accCube f (Fin.last n)] + have h1 := Pa_δ!₄ f g + have h2 := Pa_δ!₁ f g (Fin.last n) + have h3 := Pa_δ!₂ f g (Fin.last n) + simp at h1 h2 h3 + have hl : f (Fin.succ (Fin.last (n ))) = - Pa f g δ!₄ := by + simp_all only [Fin.succ_last, neg_neg] + erw [hl] at h2 + have hg : g (Fin.last n) = Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄ := by + linear_combination -(1 * h2) + have hll : f (Fin.castSucc (Fin.last (n ))) = + - (Pa f g (δ!₂ (Fin.last n)) + Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄) := by + linear_combination h3 - 1 * hg + rw [← hS] at hl hll + rw [hl, hll] + ring + +lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols} + (LIC : lineInCubicPerm S) : + lineInPlaneProp + ((S.val (δ!₂ (Fin.last n))), ((S.val (δ!₁ (Fin.last n))), (S.val δ!₄))) := by + obtain ⟨g, f, hfg⟩ := span_basis S + have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg + rw [P_P_P!_accCube' g f hfg] at h1 + simp at h1 + cases h1 <;> rename_i h1 + apply Or.inl + linear_combination h1 + cases h1 <;> rename_i h1 + apply Or.inr + apply Or.inl + linear_combination -(1 * h1) + apply Or.inr + apply Or.inr + exact h1 + +lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols} + (LIC : lineInCubicPerm S) : lineInPlaneCond S := by + refine @Prop_three (2 * n.succ.succ) lineInPlaneProp S (δ!₂ (Fin.last n)) (δ!₁ (Fin.last n)) + δ!₄ ?_ ?_ ?_ ?_ + simp [Fin.ext_iff, δ!₂, δ!₁] + simp [Fin.ext_iff, δ!₂, δ!₄] + simp [Fin.ext_iff, δ!₁, δ!₄] + omega + intro M + exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M) + +lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ)).Sols} + (LIC : lineInCubicPerm S.1.1) : constAbs S.val := + linesInPlane_constAbs_AF S (lineInCubicPerm_last_perm LIC) + +theorem lineInCubicPerm_vectorLike {S : (PureU1 (2 * n.succ.succ)).Sols} + (LIC : lineInCubicPerm S.1.1) : vectorLikeEven S.val := + ConstAbs.boundary_value_even S.1.1 (lineInCubicPerm_constAbs LIC) + +theorem lineInCubicPerm_in_plane (S : (PureU1 (2 * n.succ.succ)).Sols) + (LIC : lineInCubicPerm S.1.1) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group), + (FamilyPermutations (2 * n.succ.succ)).linSolRep M S.1.1 + ∈ Submodule.span ℚ (Set.range basis) := + vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC) + +end Even +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean new file mode 100644 index 0000000..359465a --- /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/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean new file mode 100644 index 0000000..a977a64 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean @@ -0,0 +1,187 @@ +/- +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 Mathlib.Tactic.Polyrith +import Mathlib.RepresentationTheory.Basic +/-! +# Line in plane condition + +We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in +`Fin n`, we have +`S i1 = S i2` or `S i1 = - S i2` or `2 S i3 + S i1 + S i2 = 0`. + +We look at various consequences of this. +The main reference for this material is + +- https://arxiv.org/pdf/1912.04804.pdf + +We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the +`constAbs` condition. + +-/ + + +namespace PureU1 + +open BigOperators + +variable {n : ℕ} + +/-- The proposition on three rationals to satisfy the `linInPlane` condition. -/ +def lineInPlaneProp : ℚ × ℚ × ℚ → Prop := fun s => + s.1 = s.2.1 ∨ s.1 = - s.2.1 ∨ 2 * s.2.2 + s.1 + s.2.1 = 0 + +/-- The proposition on a `LinSol` to satisfy the `linInPlane` condition. -/ +def lineInPlaneCond (S : (PureU1 (n)).LinSols) : Prop := + ∀ (i1 i2 i3 : Fin (n)) (_ : i1 ≠ i2) (_ : i2 ≠ i3) (_ : i1 ≠ i3), + lineInPlaneProp (S.val i1, (S.val i2, S.val i3)) + +lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : lineInPlaneCond S) + (M : (FamilyPermutations n).group) : + lineInPlaneCond ((FamilyPermutations n).linSolRep M S) := by + intro i1 i2 i3 h1 h2 h3 + rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply, + FamilyPermutations_anomalyFreeLinear_apply] + refine hS (M.invFun i1) (M.invFun i2) (M.invFun i3) ?_ ?_ ?_ + all_goals simp_all only [ne_eq, Equiv.invFun_as_coe, EmbeddingLike.apply_eq_iff_eq, + not_false_eq_true] + + +lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : lineInPlaneCond S) + (h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) : + (2 - n) * S.val (Fin.last (n + 1)) = + - (2 - n)* S.val (Fin.castSucc (Fin.last n)) := by + erw [sq_eq_sq_iff_eq_or_eq_neg] at h + rw [lineInPlaneCond] at hS + simp only [lineInPlaneProp] at hS + simp [not_or] at h + have h1 (i : Fin n) : S.val i.castSucc.castSucc = + - (S.val ((Fin.last n).castSucc) + (S.val ((Fin.last n).succ))) / 2 := by + have h1S := hS (Fin.last n).castSucc ((Fin.last n).succ) i.castSucc.castSucc + (by simp; rw [Fin.ext_iff]; simp; omega) + (by simp; rw [Fin.ext_iff]; simp; omega) + (by simp; rw [Fin.ext_iff]; simp; omega) + simp_all + field_simp + linear_combination h1S + have h2 := pureU1_last S + rw [Fin.sum_univ_castSucc] at h2 + simp [h1] at h2 + field_simp at h2 + linear_combination h2 + +lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols} + (hS : lineInPlaneCond S) : constAbsProp ((S.val ((Fin.last n.succ.succ.succ).castSucc)), + (S.val ((Fin.last n.succ.succ.succ).succ))) := by + rw [constAbsProp] + by_contra hn + have h := lineInPlaneCond_eq_last' hS hn + rw [sq_eq_sq_iff_eq_or_eq_neg] at hn + simp [or_not] at hn + have hx : ((2 : ℚ) - ↑(n + 3)) ≠ 0 := by + rw [Nat.cast_add] + simp only [Nat.cast_ofNat, ne_eq] + apply Not.intro + intro a + linarith + have ht : S.val ((Fin.last n.succ.succ.succ).succ) = + - S.val ((Fin.last n.succ.succ.succ).castSucc) := by + rw [← mul_right_inj' hx] + simp [Nat.succ_eq_add_one] + simp at h + rw [h] + ring + simp_all + +lemma linesInPlane_eq_sq {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols} + (hS : lineInPlaneCond S) : ∀ (i j : Fin n.succ.succ.succ.succ.succ) (_ : i ≠ j), + constAbsProp (S.val i, S.val j) := by + have hneq : ((Fin.last n.succ.succ.succ).castSucc) ≠ ((Fin.last n.succ.succ.succ).succ) := by + simp [Fin.ext_iff] + refine Prop_two constAbsProp hneq ?_ + intro M + exact lineInPlaneCond_eq_last (lineInPlaneCond_perm hS M) + +theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols} + (hS : lineInPlaneCond S) : constAbs S.val := by + intro i j + by_cases hij : i ≠ j + exact linesInPlane_eq_sq hS i j hij + simp at hij + rw [hij] + +lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : lineInPlaneCond S.1.1) : + constAbsProp (S.val (0 : Fin 4), S.val (1 : Fin 4)) := by + simp [constAbsProp] + by_contra hn + have hLin := pureU1_linear S.1.1 + have hcube := pureU1_cube S + simp at hLin hcube + rw [Fin.sum_univ_four] at hLin hcube + rw [sq_eq_sq_iff_eq_or_eq_neg] at hn + simp [not_or] at hn + have l012 := hS 0 1 2 (by simp) (by simp) (by simp) + have l013 := hS 0 1 3 (by simp) (by simp) (by simp) + have l023 := hS 0 2 3 (by simp) (by simp) (by simp) + simp_all [lineInPlaneProp] + have h1 : S.val (2 : Fin 4) = S.val (3 : Fin 4) := by + linear_combination l012 / 2 + -1 * l013 / 2 + by_cases h2 : S.val (0 : Fin 4) = S.val (2 : Fin 4) + simp_all + have h3 : S.val (1 : Fin 4) = - 3 * S.val (2 : Fin 4) := by + linear_combination l012 + 3 * h1 + rw [← h1, h3] at hcube + have h4 : S.val (2 : Fin 4) ^ 3 = 0 := by + linear_combination -1 * hcube / 24 + simp at h4 + simp_all + by_cases h3 : S.val (0 : Fin 4) = - S.val (2 : Fin 4) + simp_all + have h4 : S.val (1 : Fin 4) = - S.val (2 : Fin 4) := by + linear_combination l012 + h1 + simp_all + simp_all + have h4 : S.val (0 : Fin 4) = - 3 * S.val (3 : Fin 4) := by + linear_combination l023 + have h5 : S.val (1 : Fin 4) = S.val (3 : Fin 4) := by + linear_combination l013 - 1 * h4 + rw [h4, h5] at hcube + have h6 : S.val (3 : Fin 4) ^ 3 = 0 := by + linear_combination -1 * hcube / 24 + simp at h6 + simp_all + + +lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols} + (hS : lineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j), + constAbsProp (S.val i, S.val j) := by + refine Prop_two constAbsProp (by simp : (0 : Fin 4) ≠ 1) ?_ + intro M + let S' := (FamilyPermutations 4).solAction.toFun S M + have hS' : lineInPlaneCond S'.1.1 := + (lineInPlaneCond_perm hS M) + exact linesInPlane_four S' hS' + + +lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols) + (hS : lineInPlaneCond S.1.1) : constAbs S.val := by + intro i j + by_cases hij : i ≠ j + exact linesInPlane_eq_sq_four hS i j hij + simp at hij + rw [hij] + +theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols) + (hS : lineInPlaneCond S.1.1) : constAbs S.val := by + induction n + exact linesInPlane_constAbs_four S hS + exact linesInPlane_constAbs hS + + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/One.lean new file mode 100644 index 0000000..4dc949c --- /dev/null +++ b/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 diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean new file mode 100644 index 0000000..ecfc210 --- /dev/null +++ b/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 diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean new file mode 100644 index 0000000..2516212 --- /dev/null +++ b/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 only [Fin.sum_univ_two, Fin.isValue] + 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 diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean new file mode 100644 index 0000000..903d788 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -0,0 +1,713 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.BasisLinear +import HepLean.AnomalyCancellation.PureU1.VectorLike +import Mathlib.Logic.Equiv.Fin +/-! +# Basis of `LinSols` in the odd case + +We give a basis of `LinSols` in the odd case. This basis has the special propoerty +that splits into two planes on which every point is a solution to the ACCs. +-/ +universe v u + +open Nat +open Finset +open BigOperators + +namespace PureU1 + +variable {n : ℕ} + + +namespace VectorLikeOddPlane + +lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by + omega + +lemma split_adda (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by + omega + +section theDeltas + +/-- A helper function for what follows. -/ +def δ₁ (j : Fin n) : Fin (2 * n + 1) := + Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j)) + +/-- A helper function for what follows. -/ +def δ₂ (j : Fin n) : Fin (2 * n + 1) := + Fin.cast (split_odd n) (Fin.natAdd (n+1) j) + +/-- A helper function for what follows. -/ +def δ₃ : Fin (2 * n + 1) := + Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1)) + +/-- A helper function for what follows. -/ +def δ!₁ (j : Fin n) : Fin (2 * n + 1) := + Fin.cast (split_odd! n) (Fin.castAdd n (Fin.natAdd 1 j)) + +/-- A helper function for what follows. -/ +def δ!₂ (j : Fin n) : Fin (2 * n + 1) := + Fin.cast (split_odd! n) (Fin.natAdd (1 + n) j) + +/-- A helper function for what follows. -/ +def δ!₃ : Fin (2 * n + 1) := + Fin.cast (split_odd! n) (Fin.castAdd n (Fin.castAdd n 1)) + +/-- A helper function for what follows. -/ +def δa₁ : Fin (2 * n.succ + 1) := + Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1))) + +/-- A helper function for what follows. -/ +def δa₂ (j : Fin n) : Fin (2 * n.succ + 1) := + Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j))) + +/-- A helper function for what follows. -/ +def δa₃ : Fin (2 * n.succ + 1) := + Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1)) + +/-- A helper function for what follows. -/ +def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) := + Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j) + +lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by + rfl + +lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by + rfl + +lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by + rw [Fin.ext_iff] + simp [δa₂, δ₁] + omega + +lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by + rw [Fin.ext_iff] + simp [δa₂, δ!₁] + +lemma δa₃_δ₃ : @δa₃ n = δ₃ := by + rw [Fin.ext_iff] + simp [δa₃, δ₃] + omega + +lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by + rfl + +lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by + rw [Fin.ext_iff] + simp [δa₄, δ₂] + omega + +lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by + rw [Fin.ext_iff] + simp [δa₄, δ!₂] + omega + +lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by + rw [Fin.ext_iff] + simp [δ₂, δ!₂] + omega + +lemma sum_δ (S : Fin (2 * n + 1) → ℚ) : + ∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by + have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by + rw [Finset.sum_equiv (Fin.castIso (split_odd n)).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + rw [h1] + rw [Fin.sum_univ_add, Fin.sum_univ_add] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + nth_rewrite 2 [add_comm] + rw [add_assoc] + rw [Finset.sum_add_distrib] + rfl + +lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) : + ∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by + have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by + rw [Finset.sum_equiv (Fin.castIso (split_odd! n)).symm.toEquiv] + intro i + simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply] + intro i + simp + rw [h1] + rw [Fin.sum_univ_add, Fin.sum_univ_add] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + rw [add_assoc] + rw [Finset.sum_add_distrib] + rfl + +end theDeltas + +section theBasisVectors + +/-- The first part of the basis as charge assignments. -/ +def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).charges := + fun i => + if i = δ₁ j then + 1 + else + if i = δ₂ j then + - 1 + else + 0 + +/-- The second part of the basis as charge assignments. -/ +def basis!AsCharges (j : Fin n) : (PureU1 (2 * n + 1)).charges := + fun i => + if i = δ!₁ j then + 1 + else + if i = δ!₂ j then + - 1 + else + 0 + +lemma basis_on_δ₁_self (j : Fin n) : basisAsCharges j (δ₁ j) = 1 := by + simp [basisAsCharges] + +lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by + simp [basis!AsCharges] + +lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) : + basisAsCharges k (δ₁ j) = 0 := by + simp [basisAsCharges] + simp [δ₁, δ₂] + split + rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + split + rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp at h2 + omega + rfl + +lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) : + basis!AsCharges k (δ!₁ j) = 0 := by + simp [basis!AsCharges] + simp [δ!₁, δ!₂] + split + rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + split + rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp at h2 + omega + rfl + +lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) : + basisAsCharges k j = 0 := by + simp [basisAsCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) : + basis!AsCharges k j = 0 := by + simp [basis!AsCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) : + basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by + simp [basisAsCharges, δ₂, δ₁] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals rename_i h1 h2 + all_goals rw [Fin.ext_iff] at h1 h2 + all_goals simp_all + all_goals rename_i h3 + all_goals rw [Fin.ext_iff] at h3 + all_goals simp_all + all_goals omega + +lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) : + basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by + simp [basis!AsCharges, δ!₂, δ!₁] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals rename_i h1 h2 + all_goals rw [Fin.ext_iff] at h1 h2 + all_goals simp_all + subst h1 + exact Fin.elim0 i + all_goals rename_i h3 + all_goals rw [Fin.ext_iff] at h3 + all_goals simp_all + all_goals omega + +lemma basis_on_δ₂_self (j : Fin n) : basisAsCharges j (δ₂ j) = - 1 := by + rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self] + +lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by + rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self] + +lemma basis_on_δ₂_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by + rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h] + rfl + +lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by + rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h] + rfl + +lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by + simp [basisAsCharges] + split <;> rename_i h + rw [Fin.ext_iff] at h + simp [δ₃, δ₁] at h + omega + split <;> rename_i h2 + rw [Fin.ext_iff] at h2 + simp [δ₃, δ₂] at h2 + omega + rfl + +lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by + simp [basis!AsCharges] + split <;> rename_i h + rw [Fin.ext_iff] at h + simp [δ!₃, δ!₁] at h + omega + split <;> rename_i h2 + rw [Fin.ext_iff] at h2 + simp [δ!₃, δ!₂] at h2 + omega + rfl + +lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + erw [sum_δ] + simp [basis_δ₂_eq_minus_δ₁, basis_on_δ₃] + +lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ!, basis!_on_δ!₃] + simp [basis!_δ!₂_eq_minus_δ!₁] + +/-- The first part of the basis as `LinSols`. -/ +@[simps!] +def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := + ⟨basisAsCharges j, by + intro i + simp at i + match i with + | 0 => + exact basis_linearACC j⟩ + +/-- The second part of the basis as `LinSols`. -/ +@[simps!] +def basis! (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := + ⟨basis!AsCharges j, by + intro i + simp at i + match i with + | 0 => + exact basis!_linearACC j⟩ + +/-- The whole basis as `LinSols`. -/ +def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i => + match i with + | .inl i => basis i + | .inr i => basis! i + +end theBasisVectors + +/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/ +lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n) + (hS : ((FamilyPermutations (2 * n + 1)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j))) S = S') : + S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by + funext i + rw [← hS, FamilyPermutations_anomalyFreeLinear_apply] + by_cases hi : i = δ!₁ j + subst hi + simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst] + by_cases hi2 : i = δ!₂ j + subst hi2 + simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd] + simp [HSMul.hSMul] + rw [basis!_on_other hi hi2] + change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_ + erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)] + simp + +/-- A point in the span of the first part of the basis as a charge. -/ +def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := ∑ i, f i • basisAsCharges i + +/-- A point in the span of the second part of the basis as a charge. -/ +def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := ∑ i, f i • basis!AsCharges i + +/-- A point in the span of the basis as a charge. -/ +def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := P f + P! g + +lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by + rw [P, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis_on_δ₁_self] + simp only [mul_one] + intro k _ hkj + rw [basis_on_δ₁_other hkj] + simp only [mul_zero] + simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff] + +lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis!_on_δ!₁_self] + simp only [mul_one] + intro k _ hkj + rw [basis!_on_δ!₁_other hkj] + simp only [mul_zero] + simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff] + +lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by + rw [P, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis_on_δ₂_self] + simp only [mul_neg, mul_one] + intro k _ hkj + rw [basis_on_δ₂_other hkj] + simp only [mul_zero] + simp + +lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + rw [basis!_on_δ!₂_self] + simp only [mul_neg, mul_one] + intro k _ hkj + rw [basis!_on_δ!₂_other hkj] + simp only [mul_zero] + simp + +lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by + rw [P, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, basis_on_δ₃] + +lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by + rw [P!, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃] + +lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [δa₁_δ₁] + rw [δa₁_δ!₃] + rw [P_δ₁, P!_δ!₃] + simp + +lemma Pa_δa₂ (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (δa₂ j) = f j.succ + g j.castSucc := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [δa₂_δ₁] + rw [δa₂_δ!₁] + rw [P_δ₁, P!_δ!₁] + +lemma Pa_δa₃ (f g : Fin n.succ → ℚ) : Pa f g (δa₃) = g (Fin.last n) := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [δa₃_δ₃] + rw [δa₃_δ!₁] + rw [P_δ₃, P!_δ!₁] + simp + +lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by + rw [Pa] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [δa₄_δ₂] + rw [δa₄_δ!₂] + rw [P_δ₂, P!_δ!₂] + ring + +lemma P_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ] + simp [P_δ₂, P_δ₁, P_δ₃] + +lemma P!_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_δ!] + simp [P!_δ!₂, P!_δ!₁, P!_δ!₃] + +lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by + rw [accCube_explicit, sum_δ, P_δ₃] + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add] + apply Finset.sum_eq_zero + intro i _ + simp [P_δ₁, P_δ₂] + ring + +lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by + rw [accCube_explicit, sum_δ!, P!_δ!₃] + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add] + apply Finset.sum_eq_zero + intro i _ + simp [P!_δ!₁, P!_δ!₂] + ring + +lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) : + accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) + = (P g (δ!₁ j))^2 - (g j)^2 := by + simp [accCubeTriLinSymm] + rw [sum_δ!, basis!_on_δ!₃] + simp only [mul_zero, Function.comp_apply, zero_add] + rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self] + rw [← δ₂_δ!₂, P_δ₂] + ring + intro k _ hkj + erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm] + simp only [mul_zero, add_zero] + simp + + +lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by + intro i + erw [← P_δ₁ f] + rw [h] + rfl + +lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by + intro i + rw [← P!_δ!₁ f] + rw [h] + rfl + +lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) : + ∀ i, f i = 0 := by + have h₃ := Pa_δa₁ f g + rw [h] at h₃ + change 0 = _ at h₃ + simp at h₃ + intro i + have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by + induction iv + exact h₃.symm + rename_i iv hi + have hivi : iv < n.succ := by omega + have hi2 := hi hivi + have h1 := Pa_δa₄ f g ⟨iv, hivi⟩ + rw [h, hi2] at h1 + change 0 = _ at h1 + simp at h1 + have h2 := Pa_δa₂ f g ⟨iv, by omega⟩ + simp [h, h1] at h2 + exact h2.symm + exact hinduc i.val i.prop + +lemma Pa_zero! (f g : Fin n.succ → ℚ) (h : Pa f g = 0) : + ∀ i, g i = 0 := by + have hf := Pa_zero f g h + rw [Pa, P] at h + simp [hf] at h + exact P!_zero g h + +/-- A point in the span of the first part of the basis. -/ +def P' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis i + +/-- A point in the span of the second part of the basis. -/ +def P!' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis! i + +/-- A point in the span of the whole basis. -/ +def Pa' (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols := + ∑ i, f i • basisa i + +lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) : + Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by + exact Fintype.sum_sum_type _ + +lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by + simp [P', P] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + simp [HSMul.hSMul] + +lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by + simp [P!', P!] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + simp [HSMul.hSMul] + +theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change P' f = 0 at h + have h1 : (P' f).val = 0 := by + simp [h] + rfl + rw [P'_val] at h1 + exact P_zero f h1 + +theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change P!' f = 0 at h + have h1 : (P!' f).val = 0 := by + simp [h] + rfl + rw [P!'_val] at h1 + exact P!_zero f h1 + + +theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change Pa' f = 0 at h + have h1 : (Pa' f).val = 0 := by + simp [h] + rfl + rw [Pa'_P'_P!'] at h1 + change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1 + rw [P!'_val, P'_val] at h1 + change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 + have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + intro i + simp_all + cases i + simp_all + simp_all + +lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by + apply Iff.intro + intro h + funext i + rw [Pa', Pa'] at h + have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by + simp only [add_smul, neg_smul] + rw [Finset.sum_add_distrib] + rw [h] + rw [← Finset.sum_add_distrib] + simp + have h2 : ∀ i, (f i + (- f' i)) = 0 := by + exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n)) + (fun i => f i + -f' i) h1 + have h2i := h2 i + linarith + intro h + rw [h] + +/-- A helper function for what follows. TODO: replace this with mathlib functions. -/ +def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i => + match i with + | .inl i => g i + | .inr i => f i + +lemma join_ext (g g' : Fin n → ℚ) (f f' : Fin n → ℚ) : + join g f = join g' f' ↔ g = g' ∧ f = f' := by + apply Iff.intro + intro h + apply And.intro + funext i + exact congr_fun h (Sum.inl i) + funext i + exact congr_fun h (Sum.inr i) + intro h + rw [h.left, h.right] + +lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : + Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by + apply Iff.intro + intro h + rw [Pa'_eq] at h + rw [join_ext] at h + rw [h.left, h.right] + intro h + apply ACCSystemLinear.LinSols.ext + rw [Pa'_P'_P!', Pa'_P'_P!'] + simp [P'_val, P!'_val] + exact h + +lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : + Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by + rw [← join_Pa] + rw [← join_ext] + exact Pa'_eq _ _ + + + +lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) = + FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by + erw [BasisLinear.finrank_AnomalyFreeLinear] + simp only [Fintype.card_sum, Fintype.card_fin] + omega + +/-- The basis formed out of our basisa vectors. -/ +noncomputable def basisaAsBasis : + Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols := + basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card + +lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) : + ∃ (g f : Fin n.succ → ℚ) , S.val = P g + P! f := by + have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S) + obtain ⟨f, hf⟩ := h + simp [basisaAsBasis] at hf + change P' _ + P!' _ = S at hf + use f ∘ Sum.inl + use f ∘ Sum.inr + rw [← hf] + simp [P'_val, P!'_val] + rfl + +lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ) + (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f): + ∃ (g' f' : Fin n.succ → ℚ), + S'.val = P g' + P! f' ∧ P! f' = P! f + + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by + let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j + have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by + rw [(mem_span_range_iff_exists_fun ℚ)] + use f + rfl + have hP : (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈ + Submodule.span ℚ (Set.range basis!AsCharges) := by + apply Submodule.smul_mem + apply SetLike.mem_of_subset + apply Submodule.subset_span + simp_all only [Set.mem_range, exists_apply_eq_apply] + have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by + apply Submodule.add_mem + exact hf + exact hP + have hXsum := (mem_span_range_iff_exists_fun ℚ).mp hX + obtain ⟨f', hf'⟩ := hXsum + use g + use f' + change P! f' = _ at hf' + erw [hf'] + simp only [and_self, and_true] + change S'.val = P g + (P! f + _) + rw [← add_assoc, ← hS1] + apply swap!_as_add at hS + exact hS + + +end VectorLikeOddPlane + + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean new file mode 100644 index 0000000..8ee978e --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.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.Permutations +import HepLean.AnomalyCancellation.PureU1.VectorLike +import HepLean.AnomalyCancellation.PureU1.ConstAbs +import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond +import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear +import Mathlib.Tactic.Polyrith +import Mathlib.RepresentationTheory.Basic +/-! + +# Line In Cubic Odd case + +We say that a linear solution satisfies the `lineInCubic` property +if the line through that point and through the two different planes formed by the baisis of +`LinSols` lies in the cubic. + +We show that for a solution all its permutations satsfiy this property, +then the charge must be zero. + +The main reference for this file is: + +- https://arxiv.org/pdf/1912.04804.pdf +-/ +namespace PureU1 +namespace Odd + +open BigOperators + +variable {n : ℕ} +open VectorLikeOddPlane + +/-- A property on `LinSols`, statified if every point on the line between the two planes +in the basis through that point is in the cubic. -/ +def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop := + ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) , + accCube (2 * n + 1) (a • P g + b • P! f) = 0 + +lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) : + ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ) , + 3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f) + + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by + intro g f hS a b + have h1 := h g f hS a b + change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1 + simp only [TriLinearSymm.toCubic_add] at h1 + simp only [HomogeneousCubic.map_smul, + accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 + erw [P_accCube, P!_accCube] at h1 + rw [← h1] + ring + + +lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) : + ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), + accCubeTriLinSymm (P g, P g, P! f) = 0 := by + intro g f hS + linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) - + (lineInCubic_expand h g f hS 1 2 ) / 6 + + + +/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/ +def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop := + ∀ (M : (FamilyPermutations (2 * n + 1)).group ), + lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S) + +/-- If `lineInCubicPerm S` then `lineInCubic S`. -/ +lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : lineInCubicPerm S) : + lineInCubic S := hS 1 + +/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/ +lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols} + (hS : lineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) : + lineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by + rw [lineInCubicPerm] + intro M + have ht : ((FamilyPermutations (2 * n + 1)).linSolRep M) + ((FamilyPermutations (2 * n + 1)).linSolRep M' S) + = (FamilyPermutations (2 * n + 1)).linSolRep (M * M') S := by + simp [(FamilyPermutations (2 * n.succ)).linSolRep.map_mul'] + rw [ht] + exact hS (M * M') + + +lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols} + (LIC : lineInCubicPerm S) : + ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) , + (S.val (δ!₂ j) - S.val (δ!₁ j)) + * accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by + intro j g f h + let S' := (FamilyPermutations (2 * n.succ + 1)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j)) S + have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep + (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl + obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h + have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h + have h2 := line_in_cubic_P_P_P! + (lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1 + rw [hall.2.1, hall.2.2] at h2 + rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2 + simpa using h2 + +lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} + (f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) : + accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges 0) = + (S.val (δ!₁ 0) + S.val (δ!₂ 0)) * (2 * S.val δ!₃ + S.val (δ!₁ 0) + S.val (δ!₂ 0)) := by + rw [P_P_P!_accCube f 0] + rw [← Pa_δa₁ f g] + rw [← hS] + have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := by + simp [δ!₁, δ₁] + rw [Fin.ext_iff] + simp + nth_rewrite 1 [ht] + rw [P_δ₁] + have h1 := Pa_δa₁ f g + have h4 := Pa_δa₄ f g 0 + have h2 := Pa_δa₂ f g 0 + rw [← hS] at h1 h2 h4 + simp at h2 + have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0):= by + linear_combination -(1 * h1) - 1 * h4 - 1 * h2 + rw [h5] + rw [δa₄_δ!₂] + have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by + rw [δa₂_δ!₁] + simp + rw [h0, δa₁_δ!₃] + ring + +lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols} + (LIC : lineInCubicPerm S) : + lineInPlaneProp ((S.val (δ!₂ 0)), ((S.val (δ!₁ 0)), (S.val δ!₃))) := by + obtain ⟨g, f, hfg⟩ := span_basis S + have h1 := lineInCubicPerm_swap LIC 0 g f hfg + rw [P_P_P!_accCube' g f hfg] at h1 + simp at h1 + cases h1 <;> rename_i h1 + apply Or.inl + linear_combination h1 + cases h1 <;> rename_i h1 + apply Or.inr + apply Or.inl + linear_combination h1 + apply Or.inr + apply Or.inr + linear_combination h1 + +lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} + (LIC : lineInCubicPerm S) : lineInPlaneCond S := by + refine @Prop_three (2 * n.succ.succ + 1) lineInPlaneProp S (δ!₂ 0) (δ!₁ 0) + δ!₃ ?_ ?_ ?_ ?_ + simp [Fin.ext_iff, δ!₂, δ!₁] + simp [Fin.ext_iff, δ!₂, δ!₃] + simp [Fin.ext_iff, δ!₁, δ!₃] + intro M + exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M) + +lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} + (LIC : lineInCubicPerm S) : constAbs S.val := + linesInPlane_constAbs (lineInCubicPerm_last_perm LIC) + +theorem lineInCubicPerm_zero {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} + (LIC : lineInCubicPerm S) : S = 0 := + ConstAbs.boundary_value_odd S (lineInCubicPerm_constAbs LIC) + +end Odd +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean new file mode 100644 index 0000000..02d2d18 --- /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 diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean new file mode 100644 index 0000000..ff237b7 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean @@ -0,0 +1,343 @@ +/- +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.GroupActions +import Mathlib.Tactic.Polyrith +import Mathlib.RepresentationTheory.Basic +import Mathlib.Data.Fin.Tuple.Sort +/-! +# Permutations of Pure U(1) ACC + +We define the permutation group action on the charges of the Pure U(1) ACC system. +We further define the action on the ACC System. + +-/ + +universe v u + +open Nat +open Finset + +namespace PureU1 + +/-- The permutation group of the n-fermions. -/ +@[simp] +def permGroup (n : ℕ) := Equiv.Perm (Fin n) + +instance {n : ℕ} : Group (permGroup n) := by + simp [permGroup] + infer_instance + +section Charges + +/-- The image of an element of `permGroup` under the representation on charges. -/ +@[simps!] +def chargeMap {n : ℕ} (f : permGroup n) : + (PureU1 n).charges →ₗ[ℚ] (PureU1 n).charges where + toFun S := S ∘ f.toFun + map_add' S T := by + funext i + simp + map_smul' a S := by + funext i + simp [HSMul.hSMul] + -- rw [show Rat.cast a = a from rfl] + +open PureU1Charges in + +/-- The representation of `permGroup` acting on the vector space of charges. -/ +@[simp] +def permCharges {n : ℕ} : Representation ℚ (permGroup n) (PureU1 n).charges where + toFun f := chargeMap f⁻¹ + map_mul' f g :=by + simp only [permGroup, mul_inv_rev] + apply LinearMap.ext + intro S + funext i + rfl + map_one' := by + apply LinearMap.ext + intro S + funext i + rfl + +lemma accGrav_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) : + PureU1.accGrav n (permCharges f S) = accGrav n S := by + simp [accGrav, permCharges] + apply (Equiv.Perm.sum_comp _ _ _ ?_) + simp + +open BigOperators +lemma accCube_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) : + accCube n (permCharges f S) = accCube n S := by + rw [accCube_explicit, accCube_explicit] + change ∑ i : Fin n, ((((fun a => a^3) ∘ S) (f.symm i))) = _ + apply (Equiv.Perm.sum_comp _ _ _ ?_) + simp + +end Charges + +/-- The permutations acting on the ACC system. -/ +@[simp] +def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where + group := permGroup n + groupInst := inferInstance + rep := permCharges + linearInvariant := by + intro i + simp at i + match i with + | 0 => exact accGrav_invariant + quadInvariant := by + intro i + simp at i + exact Fin.elim0 i + cubicInvariant := accCube_invariant + + +lemma FamilyPermutations_charges_apply (S : (PureU1 n).charges) + (i : Fin n) (f : (FamilyPermutations n).group) : + ((FamilyPermutations n).rep f S) i = S (f.invFun i) := by + rfl + +lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols) + (i : Fin n) (f : (FamilyPermutations n).group) : + ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by + rfl + + +/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/ +def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where + toFun s := + if s = i then + j + else + if s = j then + i + else + s + invFun s := + if s = i then + j + else + if s = j then + i + else + s + left_inv s := by + aesop + right_inv s := by + aesop + +lemma pairSwap_self_inv {n : ℕ} (i j : Fin n) : (pairSwap i j)⁻¹ = (pairSwap i j) := by + rfl + +lemma pairSwap_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun i = j := by + simp [pairSwap] + +lemma pairSwap_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun j = i := by + simp [pairSwap] + +lemma pairSwap_inv_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun i = j := by + simp [pairSwap] + +lemma pairSwap_inv_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun j = i := by + simp [pairSwap] + +lemma pairSwap_other {n : ℕ} (i j k : Fin n) (hik : i ≠ k) (hjk : j ≠ k) : + (pairSwap i j).toFun k = k := by + simp [pairSwap] + split + simp_all + split + simp_all + rfl + +lemma pairSwap_inv_other {n : ℕ} {i j k : Fin n} (hik : i ≠ k) (hjk : j ≠ k) : + (pairSwap i j).invFun k = k := by + simp [pairSwap] + split + simp_all + split + simp_all + rfl + +/-- A permutation of fermions which takes one ordered subset into another. -/ +noncomputable def permOfInjection (f g : Fin m ↪ Fin n) : (FamilyPermutations n).group := + Equiv.extendSubtype (g.toEquivRange.symm.trans f.toEquivRange) + +section permTwo + +variable {i j i' j' : Fin n} (hij : i ≠ j) (hij' : i' ≠ j') + +/-- Given two distinct elements, an embedding of `Fin 2` into `Fin n`. -/ +def permTwoInj : Fin 2 ↪ Fin n where + toFun s := match s with + | 0 => i + | 1 => j + inj' s1 s2 := by + aesop + +lemma permTwoInj_fst : i ∈ Set.range ⇑(permTwoInj hij) := by + simp only [Set.mem_range] + use 0 + rfl + +lemma permTwoInj_fst_apply : + (Function.Embedding.toEquivRange (permTwoInj hij)).symm ⟨i, permTwoInj_fst hij⟩ = 0 := by + exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl + +lemma permTwoInj_snd : j ∈ Set.range ⇑(permTwoInj hij) := by + simp only [Set.mem_range] + use 1 + rfl + +lemma permTwoInj_snd_apply : + (Function.Embedding.toEquivRange (permTwoInj hij)).symm + ⟨j, permTwoInj_snd hij⟩ = 1 := by + exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl + +/-- A permutation which swaps `i` with `i'` and `j` with `j'`. -/ +noncomputable def permTwo : (FamilyPermutations n).group := + permOfInjection (permTwoInj hij) (permTwoInj hij') + +lemma permTwo_fst : (permTwo hij hij').toFun i' = i := by + rw [permTwo, permOfInjection] + have ht := Equiv.extendSubtype_apply_of_mem + ((permTwoInj hij').toEquivRange.symm.trans + (permTwoInj hij).toEquivRange) i' (permTwoInj_fst hij') + simp at ht + simp [ht, permTwoInj_fst_apply] + rfl + +lemma permTwo_snd : (permTwo hij hij').toFun j' = j := by + rw [permTwo, permOfInjection] + have ht := Equiv.extendSubtype_apply_of_mem + ((permTwoInj hij' ).toEquivRange.symm.trans + (permTwoInj hij).toEquivRange) j' (permTwoInj_snd hij') + simp at ht + simp [ht, permTwoInj_snd_apply] + rfl + +end permTwo + +section permThree + +variable {i j k i' j' k' : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (hij' : i' ≠ j') + (hjk' : j' ≠ k') (hik' : i' ≠ k') + +/-- Given three distinct elements an embedding of `Fin 3` into `Fin n`. -/ +def permThreeInj : Fin 3 ↪ Fin n where + toFun s := match s with + | 0 => i + | 1 => j + | 2 => k + inj' s1 s2 := by + aesop + +lemma permThreeInj_fst : i ∈ Set.range ⇑(permThreeInj hij hjk hik) := by + simp only [Set.mem_range] + use 0 + rfl + +lemma permThreeInj_fst_apply : + (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm + ⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := by + exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl + + +lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by + simp only [Set.mem_range] + use 1 + rfl + +lemma permThreeInj_snd_apply : + (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm + ⟨j, permThreeInj_snd hij hjk hik⟩ = 1 := by + exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl + +lemma permThreeInj_thd : k ∈ Set.range ⇑(permThreeInj hij hjk hik) := by + simp only [Set.mem_range] + use 2 + rfl + +lemma permThreeInj_thd_apply : + (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm + ⟨k, permThreeInj_thd hij hjk hik⟩ = 2 := by + exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl + +/-- A permutation which swaps three distinct elements with another three. -/ +noncomputable def permThree : (FamilyPermutations n).group := + permOfInjection (permThreeInj hij hjk hik) (permThreeInj hij' hjk' hik') + +lemma permThree_fst : (permThree hij hjk hik hij' hjk' hik').toFun i' = i := by + rw [permThree, permOfInjection] + have ht := Equiv.extendSubtype_apply_of_mem + ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans + (permThreeInj hij hjk hik).toEquivRange) i' (permThreeInj_fst hij' hjk' hik') + simp at ht + simp [ht, permThreeInj_fst_apply] + rfl + +lemma permThree_snd : (permThree hij hjk hik hij' hjk' hik').toFun j' = j := by + rw [permThree, permOfInjection] + have ht := Equiv.extendSubtype_apply_of_mem + ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans + (permThreeInj hij hjk hik).toEquivRange) j' (permThreeInj_snd hij' hjk' hik') + simp at ht + simp [ht, permThreeInj_snd_apply] + rfl + +lemma permThree_thd : (permThree hij hjk hik hij' hjk' hik').toFun k' = k := by + rw [permThree, permOfInjection] + have ht := Equiv.extendSubtype_apply_of_mem + ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans + (permThreeInj hij hjk hik).toEquivRange) k' (permThreeInj_thd hij' hjk' hik') + simp at ht + simp [ht, permThreeInj_thd_apply] + rfl + +end permThree + +lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} + {a b : Fin n} (hab : a ≠ b) + (h : ∀ (f : (FamilyPermutations n).group), + P ((((FamilyPermutations n).linSolRep f S).val a), + (((FamilyPermutations n).linSolRep f S).val b) + )) : ∀ (i j : Fin n) (_ : i ≠ j), + P (S.val i, S.val j) := by + intro i j hij + have h1 := h (permTwo hij hab ).symm + rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply] at h1 + simp at h1 + change P + (S.val ((permTwo hij hab ).toFun a), + S.val ((permTwo hij hab ).toFun b)) at h1 + erw [permTwo_fst,permTwo_snd] at h1 + exact h1 + +lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols} + {a b c : Fin n} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) + (h : ∀ (f : (FamilyPermutations n).group), + P ((((FamilyPermutations n).linSolRep f S).val a),( + (((FamilyPermutations n).linSolRep f S).val b), + (((FamilyPermutations n).linSolRep f S).val c) + ))) : ∀ (i j k : Fin n) (_ : i ≠ j) (_ : j ≠ k) (_ : i ≠ k), + P (S.val i, (S.val j, S.val k)) := by + intro i j k hij hjk hik + have h1 := h (permThree hij hjk hik hab hbc hac).symm + rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply, + FamilyPermutations_anomalyFreeLinear_apply] at h1 + simp at h1 + change P + (S.val ((permThree hij hjk hik hab hbc hac).toFun a), + S.val ((permThree hij hjk hik hab hbc hac).toFun b), + S.val ((permThree hij hjk hik hab hbc hac).toFun c)) at h1 + erw [permThree_fst,permThree_snd, permThree_thd] at h1 + exact h1 + + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean new file mode 100644 index 0000000..896ff4b --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.PureU1.Permutations +/-! +# Sort for Pure U(1) charges + +We define the sort function for Pure U(1) charges, and prove some basic properties. + +-/ + +universe v u + +open Nat +open Finset + +namespace PureU1 + +variable {n : ℕ} + +/-- We say a charge is shorted if for all `i ≤ j`, then `S i ≤ S j`. -/ +@[simp] +def sorted {n : ℕ} (S : (PureU1 n).charges) : Prop := + ∀ i j (_ : i ≤ j), S i ≤ S j + +/-- Given a charge assignment `S`, the corresponding sorted charge assignment. -/ +@[simp] +def sort {n : ℕ} (S : (PureU1 n).charges) : (PureU1 n).charges := + ((FamilyPermutations n).rep (Tuple.sort S).symm S) + +lemma sort_sorted {n : ℕ} (S : (PureU1 n).charges) : sorted (sort S) := by + simp only [sorted, PureU1_numberCharges, sort, FamilyPermutations, permGroup, permCharges, + MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply] + intro i j hij + exact Tuple.monotone_sort S hij + +lemma sort_perm {n : ℕ} (S : (PureU1 n).charges) (M :(FamilyPermutations n).group) : + sort ((FamilyPermutations n).rep M S) = sort S := + @Tuple.comp_perm_comp_sort_eq_comp_sort n ℚ _ S M⁻¹ + +lemma sort_apply {n : ℕ} (S : (PureU1 n).charges) (j : Fin n) : + sort S j = S ((Tuple.sort S) j) := by + rfl + +lemma sort_zero {n : ℕ} (S : (PureU1 n).charges) (hS : sort S = 0) : S = 0 := by + funext i + have hj : ∀ j, sort S j = 0 := by + rw [hS] + intro j + rfl + have hi := hj ((Tuple.sort S).invFun i) + rw [sort_apply] at hi + simp at hi + rw [hi] + rfl + +lemma sort_projection {n : ℕ} (S : (PureU1 n).charges) : sort (sort S) = sort S := + sort_perm S (Tuple.sort S).symm + +/-- The sort function acting on `LinSols`. -/ +def sortAFL {n : ℕ} (S : (PureU1 n).LinSols) : (PureU1 n).LinSols := + ((FamilyPermutations n).linSolRep (Tuple.sort S.val).symm S) + +lemma sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) : (sortAFL S).val = sort S.val := by + rfl + + +lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols) (hS : sortAFL S = 0) : S = 0 := by + apply ACCSystemLinear.LinSols.ext + have h1 : sort S.val = 0 := by + rw [← sortAFL_val] + rw [hS] + rfl + exact sort_zero S.val h1 + +end PureU1 diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean new file mode 100644 index 0000000..f50c078 --- /dev/null +++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.AnomalyCancellation.PureU1.Sort +import Mathlib.Logic.Equiv.Fin +/-! +# Vector like charges + +For the `n`-even case we define the property of a charge assignment being vector like. + +## TODO + +The `n`-odd case. + +-/ +universe v u + +open Nat +open Finset +open BigOperators + +namespace PureU1 + +variable {n : ℕ} + +/-- + Given a natural number `n`, this lemma proves that `n + n` is equal to `2 * n`. +-/ +lemma split_equal (n : ℕ) : n + n = 2 * n := (Nat.two_mul n).symm + + +lemma split_odd (n : ℕ) : n + 1 + n = 2 * n + 1 := by omega + +/-- A charge configuration for n even is vector like if when sorted the `i`th element +is equal to the negative of the `n + i`th element. -/ +@[simp] +def vectorLikeEven (S : (PureU1 (2 * n)).charges) : Prop := + ∀ (i : Fin n), (sort S) (Fin.cast (split_equal n) (Fin.castAdd n i)) + = - (sort S) (Fin.cast (split_equal n) (Fin.natAdd n i)) + + +end PureU1