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.

def PureU1.PermGroup (n : ℕ) : Type

The permutation group of the n-fermions.

Equations

• PureU1.PermGroup n = Equiv.Perm (Fin n)

instance PureU1.instGroupPermGroup {n : ℕ} : Group (PermGroup n)

The type PermGroup n inherits the instance of a group from Equiv.Perm.

Equations

• PureU1.instGroupPermGroup = Equiv.Perm.permGroup

def PureU1.chargeMap {n : ℕ} (f : PermGroup n) : (PureU1 n).Charges →ₗ[ℚ] (PureU1 n).Charges

The image of an element of permGroup under the representation on charges.

Equations

• PureU1.chargeMap f = { toFun := fun (S : (PureU1 n).Charges) => S ∘ f.toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PureU1.chargeMap_apply {n : ℕ} (f : PermGroup n) (S : (PureU1 n).Charges) (a✝ : Fin (PureU1 n).numberCharges) : (chargeMap f) S a✝ = S (f a✝)

def PureU1.permCharges {n : ℕ} : Representation ℚ (PermGroup n) (PureU1 n).Charges

The representation of permGroup acting on the vector space of charges.

Equations

• PureU1.permCharges = { toFun := fun (f : PureU1.PermGroup n) => PureU1.chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ }

theorem PureU1.accGrav_invariant {n : ℕ} (f : PermGroup n) (S : (PureU1 n).Charges) : (accGrav n) ((permCharges f) S) = (accGrav n) S

theorem PureU1.accCube_invariant {n : ℕ} (f : PermGroup n) (S : (PureU1 n).Charges) : (accCube n) ((permCharges f) S) = (accCube n) S

def PureU1.FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n)

The permutations acting on the ACC system.

Equations

• PureU1.FamilyPermutations n = { group := PureU1.PermGroup n, groupInst := inferInstance, rep := PureU1.permCharges, linearInvariant := ⋯, quadInvariant := ⋯, cubicInvariant := ⋯ }

theorem PureU1.FamilyPermutations_charges_apply {n : ℕ} (S : (PureU1 n).Charges) (i : Fin n) (f : (FamilyPermutations n).group) : ((FamilyPermutations n).rep f) S i = S (f.invFun i)

theorem PureU1.FamilyPermutations_anomalyFreeLinear_apply {n : ℕ} (S : (PureU1 n).LinSols) (i : Fin n) (f : (FamilyPermutations n).group) : (((FamilyPermutations n).linSolRep f) S).val i = S.val (f.invFun i)

noncomputable def PureU1.permOfInjection {m n : ℕ} (f g : Fin m ↪ Fin n) : (FamilyPermutations n).group

A permutation of fermions which takes one ordered subset into another.

Equations

• PureU1.permOfInjection f g = (g.toEquivRange.symm.trans f.toEquivRange).extendSubtype

def PureU1.permTwoInj {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Fin 2 ↪ Fin n

Given two distinct elements, an embedding of Fin 2 into Fin n.

Equations

• PureU1.permTwoInj hij = { toFun := fun (s : Fin 2) => match s with | 0 => i | 1 => j, inj' := ⋯ }

theorem PureU1.permTwoInj_fst {n : ℕ} {i j : Fin n} (hij : i ≠ j) : i ∈ Set.range ⇑(permTwoInj hij)

theorem PureU1.permTwoInj_fst_apply {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (permTwoInj hij).toEquivRange.symm ⟨i, ⋯⟩ = 0

theorem PureU1.permTwoInj_snd {n : ℕ} {i j : Fin n} (hij : i ≠ j) : j ∈ Set.range ⇑(permTwoInj hij)

theorem PureU1.permTwoInj_snd_apply {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (permTwoInj hij).toEquivRange.symm ⟨j, ⋯⟩ = 1

noncomputable def PureU1.permTwo {n : ℕ} {i j i' j' : Fin n} (hij : i ≠ j) (hij' : i' ≠ j') : (FamilyPermutations n).group

A permutation which swaps i with i' and j with j'.

Equations

• PureU1.permTwo hij hij' = PureU1.permOfInjection (PureU1.permTwoInj hij) (PureU1.permTwoInj hij')

theorem PureU1.permTwo_fst {n : ℕ} {i j i' j' : Fin n} (hij : i ≠ j) (hij' : i' ≠ j') : (permTwo hij hij').toFun i' = i

theorem PureU1.permTwo_snd {n : ℕ} {i j i' j' : Fin n} (hij : i ≠ j) (hij' : i' ≠ j') : (permTwo hij hij').toFun j' = j

def PureU1.permThreeInj {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : Fin 3 ↪ Fin n

Given three distinct elements an embedding of Fin 3 into Fin n.

Equations

• PureU1.permThreeInj hij hjk hik = { toFun := fun (s : Fin 3) => match s with | 0 => i | 1 => j | 2 => k, inj' := ⋯ }

theorem PureU1.permThreeInj_fst {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : i ∈ Set.range ⇑(permThreeInj hij hjk hik)

theorem PureU1.permThreeInj_fst_apply {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : (permThreeInj hij hjk hik).toEquivRange.symm ⟨i, ⋯⟩ = 0

theorem PureU1.permThreeInj_snd {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : j ∈ Set.range ⇑(permThreeInj hij hjk hik)

theorem PureU1.permThreeInj_snd_apply {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : (permThreeInj hij hjk hik).toEquivRange.symm ⟨j, ⋯⟩ = 1

theorem PureU1.permThreeInj_thd {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : k ∈ Set.range ⇑(permThreeInj hij hjk hik)

theorem PureU1.permThreeInj_thd_apply {n : ℕ} {i j k : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : (permThreeInj hij hjk hik).toEquivRange.symm ⟨k, ⋯⟩ = 2

noncomputable def PureU1.permThree {n : ℕ} {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') : (FamilyPermutations n).group

A permutation which swaps three distinct elements with another three.

Equations

• PureU1.permThree hij hjk hik hij' hjk' hik' = PureU1.permOfInjection (PureU1.permThreeInj hij hjk hik) (PureU1.permThreeInj hij' hjk' hik')

theorem PureU1.permThree_fst {n : ℕ} {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') : (permThree hij hjk hik hij' hjk' hik').toFun i' = i

theorem PureU1.permThree_snd {n : ℕ} {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') : (permThree hij hjk hik hij' hjk' hik').toFun j' = j

theorem PureU1.permThree_thd {n : ℕ} {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') : (permThree hij hjk hik hij' hjk' hik').toFun k' = k

theorem PureU1.Prop_two {n : ℕ} (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)

theorem PureU1.Prop_three {n : ℕ} (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)