Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations

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.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
public import Mathlib.RepresentationTheory.Basic

Permutations of SM charges with RHN.

We define the group of permutations for the SM charges with RHN.

@[expose] public section

The group of Sₙ permutations for each species.

@[simp]
def PermGroup (n : ℕ) := Fin 6 → Equiv.Perm (Fin n)

The instance of a group on PermGroup n through the target space Equiv.Perm (Fin n).

@[simp]
instance : Group (PermGroup n) := Pi.group

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

@[simps!]
def chargeMap (f : PermGroup n) : (SMνCharges n).Charges →ₗ[ℚ] (SMνCharges n).Charges where
  toFun S := toSpeciesEquiv.symm (fun i => toSpecies i S ∘ f i)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

The representation of (permGroup n) acting on the vector space of charges.


@[simp]
def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMνCharges n).Charges where
  toFun f := chargeMap f⁻¹
  map_mul' f g := byn✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    simp only [PermGroup]n✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    apply LinearMap.extn✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ ∀ (x : (SMνCharges n).Charges), (chargeMap (f * g)⁻¹) x = (chargeMap f⁻¹ * chargeMap g⁻¹) x
    intro Sn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Charges⊢ (chargeMap (f * g)⁻¹) S = (chargeMap f⁻¹ * chargeMap g⁻¹) S
    rw [charges_eq_toSpecies_eqn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    intro in✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    simp only [chargeMap_apply, Pi.inv_apply, Module.End.mul_apply]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑((f * g) i)⁻¹) =
  (toSpecies i)
    (toSpeciesEquiv.symm fun i => (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹)
    repeat rw [toSMSpecies_toSpecies_invn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ =
  (toSpecies i)
    (toSpeciesEquiv.symm fun i => (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹)n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹
    rflAll goals completed! 🐙
  map_one' := byn✝:ℕn:ℕ⊢ chargeMap 1⁻¹ = 1
    refine LinearMap.ext fun S => ?_n✝:ℕn:ℕS:(SMνCharges n).Charges⊢ (chargeMap 1⁻¹) S = 1 S
    rw [charges_eq_toSpecies_eqn✝:ℕn:ℕS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)n✝:ℕn:ℕS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)]n✝:ℕn:ℕS:(SMνCharges n).Charges⊢ ∀ (i : Fin 6), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)
    intro in✝:ℕn:ℕS:(SMνCharges n).Chargesi:Fin 6⊢ (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)
    exact toSMSpecies_toSpecies_inv _ _All goals completed! 🐙

              lemma repCharges_toSpecies (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j :=
  toSMSpecies_toSpecies_inv _ _

lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
    ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
    ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := byn:ℕm:ℕf:PermGroup nS:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) ((repCharges f) S)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i
  rw [repCharges_toSpeciesn:ℕm:ℕf:PermGroup nS:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) in:ℕm:ℕf:PermGroup nS:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i]n:ℕm:ℕf:PermGroup nS:(SMνCharges n).Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i
  exact Equiv.sum_comp (f⁻¹ j) ((fun a => a ^ m) ∘ toSpecies j S)All goals completed! 🐙lemma accGrav_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accGrav (repCharges f S) = accGrav S :=
  accGrav_ext (byn:ℕf:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (j : Fin 6), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accSU2 (repCharges f S) = accSU2 S :=
  accSU2_ext (byn:ℕf:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (j : Fin 6), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accSU3 (repCharges f S) = accSU3 S :=
  accSU3_ext (byn:ℕf:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (j : Fin 6), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accYY (repCharges f S) = accYY S :=
  accYY_ext (byn:ℕf:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (j : Fin 6), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accQuad (repCharges f S) = accQuad S :=
  accQuad_ext (toSpecies_sum_invariant 2 f S)lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
    accCube (repCharges f S) = accCube S :=
  accCube_ext (byn:ℕf:PermGroup nS:(SMνCharges n).Charges⊢ ∀ (j : Fin 6),
  ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) ((repCharges f) S)) i = ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) S) i simpa using toSpecies_sum_invariant 3 f SAll goals completed! 🐙)