Sort for Pure U(1) charges

We define the sort function for Pure U(1) charges, and prove some basic properties.

def PureU1.Sorted {n : ℕ} (S : (PureU1 n).Charges) : Prop

A charge is sorted if for all i ≤ j, then S i ≤ S j.

Equations

• PureU1.Sorted S = ∀ (i j : Fin (PureU1 n).numberCharges), i ≤ j → S i ≤ S j

def PureU1.sort {n : ℕ} (S : (PureU1 n).Charges) : (PureU1 n).Charges

Given a charge assignment S, the corresponding sorted charge assignment.

Equations

• PureU1.sort S = ((PureU1.FamilyPermutations n).rep (Equiv.symm (Tuple.sort S))) S

theorem PureU1.sort_sorted {n : ℕ} (S : (PureU1 n).Charges) : Sorted (sort S)

theorem PureU1.sort_perm {n : ℕ} (S : (PureU1 n).Charges) (M : (FamilyPermutations n).group) : sort (((FamilyPermutations n).rep M) S) = sort S

theorem PureU1.sort_apply {n : ℕ} (S : (PureU1 n).Charges) (j : Fin n) : sort S j = S ((Tuple.sort S) j)

theorem PureU1.sort_zero {n : ℕ} (S : (PureU1 n).Charges) (hS : sort S = 0) : S = 0

theorem PureU1.sort_projection {n : ℕ} (S : (PureU1 n).Charges) : sort (sort S) = sort S

def PureU1.sortAFL {n : ℕ} (S : (PureU1 n).LinSols) : (PureU1 n).LinSols

The sort function acting on LinSols.

Equations

• PureU1.sortAFL S = ((PureU1.FamilyPermutations n).linSolRep (Equiv.symm (Tuple.sort S.val))) S

theorem PureU1.sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) : (sortAFL S).val = sort S.val

theorem PureU1.sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols) (hS : sortAFL S = 0) : S = 0