Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QFT.QED.AnomalyCancellation.Permutations
public import Mathlib.Data.Fin.Tuple.SortSort for Pure U(1) charges
We define the sort function for Pure U(1) charges, and prove some basic properties.
@[expose] public section
A charge is sorted if for all i ≤ j, then 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) := n:ℕS:(PureU1 n).Charges⊢ Sorted (sort S)
n:ℕS:(PureU1 n).Charges⊢ ∀ (i j : Fin (PureU1 n).numberCharges),
i ≤ j →
({ toFun := fun f => chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ } (Equiv.symm (Tuple.sort S))) S i ≤
({ toFun := fun f => chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ } (Equiv.symm (Tuple.sort S))) S j
n:ℕS:(PureU1 n).Chargesi:Fin (PureU1 n).numberChargesj:Fin (PureU1 n).numberChargeshij:i ≤ j⊢ ({ toFun := fun f => chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ } (Equiv.symm (Tuple.sort S))) S i ≤
({ toFun := fun f => chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ } (Equiv.symm (Tuple.sort S))) S j
All goals completed! 🐙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) := n:ℕS:(PureU1 n).Chargesj:Fin n⊢ sort S j = S ((Tuple.sort S) j)
All goals completed! 🐙n:ℕS:(PureU1 n).ChargeshS:sort S = 0i:Fin (PureU1 n).numberChargeshj:∀ (j : Fin (PureU1 n).numberCharges), sort S j = 0hi:S i = 0⊢ 0 = 0 i
All goals completed! 🐙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.