Mapping charge spectra values

i. Overview

In this module we define a function map which takes an additive monoid homomorphism f : 𝓩 →+ 𝓩1 and a charge spectra x : ChargeSpectrum 𝓩, and returns the charge x.map f : ChargeSpectrum 𝓩1 obtained by mapping the elements of x by f.

There are various properties which are preserved under this mapping:

• Anomaly cancellation.
• The presence of a specific term in the potential.
• Being complete.

There are some properties which are reflected under this mapping:

• Not being pheno-constrained.
• Not regenerating dangerous Yukawa terms at a given level.

We define the preimage of this mapping within a subset ofFinset S5 S10 of Charges 𝓩 in a computationaly efficient way.

ii. Key results

• map : The mapping of charge spectra under an additive monoid homomorphism.
• map_allowsTerm : If a charge spectrum allows a potential term, then so does its mapping.
• map_isPhenoConstrained : If a charge spectrum is pheno-constrained, then so is its mapping.
• map_isComplete_iff : A charge spectrum is complete if and only if its mapping is complete.
• map_yukawaGeneratesDangerousAtLevel : A charge spectrum regenerates dangerous Yukawa terms at a given level then so does its mapping.
• preimageOfFinset : The preimage of a charge spectrum in ofFinset S5 S10 under a mapping.
• preimageOfFinsetCard : The cardinality of the preimage of a charge spectrum in ofFinset S5 S10 under a mapping.

iii. Table of contents

• A. The mapping of charge spectra
  • A.1. Mapping the empty charge spectrum gives the empty charge spectrum
  • A.2. Mapping of charge spectra obeys composing maps
  • A.3. Mapping of charge spectra obeys the identity
  • A.4. The charges of a field label commute with mapping of charge spectra
  • A.5. Mappings of charge spectra preserve the subset relation
  • A.6. Mappings of charge spectra and charges of potential terms
  • A.7. Mapping charge spectra of `allowsTermForm
  • A.8. Mapping preserves whether a charge spectrum allows a potential term
  • A.9. Mapping preserves if a charge spectrum is pheno-constrained
  • A.10. Mapping preserves completeness of charge spectra
  • A.11. Mapping commutes with charges of Yukawa terms
  • A.12. Mapping of chareg spectra and regenerating dangerous Yukawa terms
• B. Preimage of a charge spectrum under a mapping
  • B.1. preimageOfFinset gives the actual preimage
  • B.2. Efficient definition for the cardinality of the preimage
  • B.3. Definition for the cardinality equals cardinality of the preimage

iv. References

There are no known references for the material in this module.

A. The mapping of charge spectra

def SuperSymmetry.SU5.ChargeSpectrum.map {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) : ChargeSpectrum 𝓩1

Given an additive monoid homomorphisms f : 𝓩 →+ 𝓩1, for a charge x : Charges 𝓩, x.map f is the charge of Charges 𝓩1 obtained by mapping the elements of x by f.

Equations

• SuperSymmetry.SU5.ChargeSpectrum.map f x = { qHd := ⇑f <$> x.qHd, qHu := ⇑f <$> x.qHu, Q5 := Finset.image (⇑f) x.Q5, Q10 := Finset.image (⇑f) x.Q10 }

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.map_empty {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) : map f ∅ = ∅

A.2. Mapping of charge spectra obeys composing maps

theorem SuperSymmetry.SU5.ChargeSpectrum.map_map {𝓩 𝓩1 𝓩2 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [AddCommGroup 𝓩2] [DecidableEq 𝓩2] (f : 𝓩 →+ 𝓩1) (g : 𝓩1 →+ 𝓩2) (x : ChargeSpectrum 𝓩) : map g (map f x) = map (g.comp f) x

A.3. Mapping of charge spectra obeys the identity

@[simp]

theorem SuperSymmetry.SU5.ChargeSpectrum.map_id {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : map (AddMonoidHom.id 𝓩) x = x

A.4. The charges of a field label commute with mapping of charge spectra

theorem SuperSymmetry.SU5.ChargeSpectrum.map_ofFieldLabel {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) (F : FieldLabel) : (map f x).ofFieldLabel F = Finset.image (⇑f) (x.ofFieldLabel F)

A.5. Mappings of charge spectra preserve the subset relation

theorem SuperSymmetry.SU5.ChargeSpectrum.map_subset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {f : 𝓩 →+ 𝓩1} {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) : map f x ⊆ map f y

A.6. Mappings of charge spectra and charges of potential terms

theorem SuperSymmetry.SU5.ChargeSpectrum.map_ofPotentialTerm_toFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : ((map f x).ofPotentialTerm T).toFinset = Finset.image (⇑f) (x.ofPotentialTerm T).toFinset

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_map_ofPotentialTerm_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {i : 𝓩1} [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : i ∈ (map f x).ofPotentialTerm T ↔ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm T)

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_map_ofPotentialTerm'_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {i : 𝓩1} [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : i ∈ (map f x).ofPotentialTerm' T ↔ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm' T)

theorem SuperSymmetry.SU5.ChargeSpectrum.map_ofPotentialTerm'_toFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : ((map f x).ofPotentialTerm' T).toFinset = Finset.image (⇑f) (x.ofPotentialTerm' T).toFinset

A.7. Mapping charge spectra of `allowsTermForm

theorem SuperSymmetry.SU5.ChargeSpectrum.allowsTermForm_map {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {T : PotentialTerm} {f : 𝓩 →+ 𝓩1} {a b c : 𝓩} : map f (allowsTermForm a b c T) = allowsTermForm (f a) (f b) (f c) T

A.8. Mapping preserves whether a charge spectrum allows a potential term

theorem SuperSymmetry.SU5.ChargeSpectrum.map_allowsTerm {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} {T : PotentialTerm} (h : x.AllowsTerm T) : (map f x).AllowsTerm T

A.9. Mapping preserves if a charge spectrum is pheno-constrained

theorem SuperSymmetry.SU5.ChargeSpectrum.map_isPhenoConstrained {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) {x : ChargeSpectrum 𝓩} (h : x.IsPhenoConstrained) : (map f x).IsPhenoConstrained

theorem SuperSymmetry.SU5.ChargeSpectrum.not_isPhenoConstrained_of_map {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} (h : ¬(map f x).IsPhenoConstrained) : ¬x.IsPhenoConstrained

A.10. Mapping preserves completeness of charge spectra

theorem SuperSymmetry.SU5.ChargeSpectrum.map_isComplete_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} : (map f x).IsComplete ↔ x.IsComplete

A.11. Mapping commutes with charges of Yukawa terms

theorem SuperSymmetry.SU5.ChargeSpectrum.map_ofYukawaTerms_toFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} : (map f x).ofYukawaTerms.toFinset = Finset.image (⇑f) x.ofYukawaTerms.toFinset

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_map_ofYukawaTerms_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} {i : 𝓩1} : i ∈ (map f x).ofYukawaTerms ↔ i ∈ Multiset.map (⇑f) x.ofYukawaTerms

A.12. Mapping of chareg spectra and regenerating dangerous Yukawa terms

theorem SuperSymmetry.SU5.ChargeSpectrum.map_ofYukawaTermsNSum_toFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} {n : ℕ} : ((map f x).ofYukawaTermsNSum n).toFinset = Finset.image (⇑f) (x.ofYukawaTermsNSum n).toFinset

theorem SuperSymmetry.SU5.ChargeSpectrum.mem_map_ofYukawaTermsNSum_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} {n : ℕ} {i : 𝓩1} : i ∈ (map f x).ofYukawaTermsNSum n ↔ i ∈ Multiset.map (⇑f) (x.ofYukawaTermsNSum n)

theorem SuperSymmetry.SU5.ChargeSpectrum.map_phenoConstrainingChargesSP_toFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} : (map f x).phenoConstrainingChargesSP.toFinset = Finset.image (⇑f) x.phenoConstrainingChargesSP.toFinset

theorem SuperSymmetry.SU5.ChargeSpectrum.map_yukawaGeneratesDangerousAtLevel {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) {x : ChargeSpectrum 𝓩} (n : ℕ) (h : x.YukawaGeneratesDangerousAtLevel n) : (map f x).YukawaGeneratesDangerousAtLevel n

theorem SuperSymmetry.SU5.ChargeSpectrum.not_yukawaGeneratesDangerousAtLevel_of_map {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : ChargeSpectrum 𝓩} (n : ℕ) (h : ¬(map f x).YukawaGeneratesDangerousAtLevel n) : ¬x.YukawaGeneratesDangerousAtLevel n

B. Preimage of a charge spectrum under a mapping

We give a computationally efficient way of calculating the preimage of a charge s : Charges 𝓩1 in a subset ofFinset S5 S10, and then show it is equal to the actual preimage.

def SuperSymmetry.SU5.ChargeSpectrum.preimageOfFinset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) : Finset (ChargeSpectrum 𝓩)

The preimage of a charge Charges 𝓩1 in ofFinset S5 S10 ⊆ Charges 𝓩 under mapping charges through f : 𝓩 →+ 𝓩1.

Equations

• One or more equations did not get rendered due to their size.

B.1. preimageOfFinset gives the actual preimage

theorem SuperSymmetry.SU5.ChargeSpectrum.preimageOfFinset_eq {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) : ↑(preimageOfFinset S5 S10 f x) = {y : ChargeSpectrum 𝓩 | map f y = x ∧ y ∈ ofFinset S5 S10}

B.2. Efficient definition for the cardinality of the preimage

def SuperSymmetry.SU5.ChargeSpectrum.preimageOfFinsetCard {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) : ℕ

The cardiniality of the preimage of a charge Charges 𝓩1 in ofFinset S5 S10 ⊆ Charges 𝓩 under mapping charges through f : 𝓩 →+ 𝓩1.

Equations

• One or more equations did not get rendered due to their size.

B.3. Definition for the cardinality equals cardinality of the preimage

theorem SuperSymmetry.SU5.ChargeSpectrum.preimageOfFinset_card_eq {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) : preimageOfFinsetCard S5 S10 f x = (preimageOfFinset S5 S10 f x).card