Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps

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.PlusU1.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps

Family Maps for SM with RHN

We give some properties of the family maps for the SM with RHN, in particular, we define family universal maps in the case of LinSols, QuadSols, and Sols.

@[expose] public section

The family universal maps on LinSols.


def familyUniversalLinear (n : ℕ) :
    (PlusU1 1).LinSols →ₗ[ℚ] (PlusU1 n).LinSols where
  toFun S := chargeToLinear (familyUniversal n S.val)
    (byn✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ accGrav ((familyUniversal n) S.val) = 0 rw [familyUniversal_accGrav,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * accGrav S.val = 0All goals completed! 🐙 gravSol S,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ accSU2 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU2,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * accSU2 S.val = 0All goals completed! 🐙 SU2Sol S,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ accSU3 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU3,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * accSU3 S.val = 0All goals completed! 🐙 SU3Sol S,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ accYY ((familyUniversal n) S.val) = 0 rw [familyUniversal_accYY,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * accYY S.val = 0All goals completed! 🐙 YYsol S,n✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).LinSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
  map_add' S T := rfl
  map_smul' a S := rfl

The family universal maps on QuadSols.


def familyUniversalQuad (n : ℕ) :
    (PlusU1 1).QuadSols → (PlusU1 n).QuadSols := fun S =>
  chargeToQuad (familyUniversal n S.val)
    (byn✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ accGrav ((familyUniversal n) S.val) = 0 rw [familyUniversal_accGrav,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * accGrav S.val = 0All goals completed! 🐙 gravSol S.1,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ accSU2 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU2,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * accSU2 S.val = 0All goals completed! 🐙 SU2Sol S.1,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ accSU3 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU3,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * accSU3 S.val = 0All goals completed! 🐙 SU3Sol S.1,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ accYY ((familyUniversal n) S.val) = 0 rw [familyUniversal_accYY,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * accYY S.val = 0All goals completed! 🐙 YYsol S.1,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ accQuad ((familyUniversal n) S.val) = 0 rw [familyUniversal_accQuad,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * accQuad S.val = 0All goals completed! 🐙 quadSol S,n✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).QuadSols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)

The family universal maps on Sols.


def familyUniversalAF (n : ℕ) :
    (PlusU1 1).Sols → (PlusU1 n).Sols := fun S =>
  chargeToAF (familyUniversal n S.val)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accGrav ((familyUniversal n) S.val) = 0 rw [familyUniversal_accGrav,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accGrav S.val = 0All goals completed! 🐙 gravSol S.1.1,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accSU2 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU2,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accSU2 S.val = 0All goals completed! 🐙 SU2Sol S.1.1,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accSU3 ((familyUniversal n) S.val) = 0 rw [familyUniversal_accSU3,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accSU3 S.val = 0All goals completed! 🐙 SU3Sol S.1.1,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accYY ((familyUniversal n) S.val) = 0 rw [familyUniversal_accYY,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accYY S.val = 0All goals completed! 🐙 YYsol S.1.1,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accQuad ((familyUniversal n) S.val) = 0 rw [familyUniversal_accQuad,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accQuad S.val = 0All goals completed! 🐙 quadSol S.1,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)
    (byn✝:ℕn:ℕS:(PlusU1 1).Sols⊢ accCube ((familyUniversal n) S.val) = 0 rw [familyUniversal_accCube,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * accCube S.val = 0All goals completed! 🐙 cubeSol S,n✝:ℕn:ℕS:(PlusU1 1).Sols⊢ ↑n * 0 = 0All goals completed! 🐙 mul_zeron✝:ℕn:ℕS:(PlusU1 1).Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙)