PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.Map

Mapping charges from different sets #

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

There are various properties which are preserved under this mapping:

There are some properties which are reflected under this mapping:

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

def SuperSymmetry.SU5.Charges.map {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩) :
Charges 𝓩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
Instances For
    @[simp]
    theorem SuperSymmetry.SU5.Charges.map_empty {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) :
    theorem SuperSymmetry.SU5.Charges.map_map {𝓩 𝓩1 𝓩2 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [AddCommGroup 𝓩2] [DecidableEq 𝓩2] (f : 𝓩 →+ 𝓩1) (g : 𝓩1 →+ 𝓩2) (x : Charges 𝓩) :
    map g (map f x) = map (g.comp f) x
    @[simp]
    theorem SuperSymmetry.SU5.Charges.map_id {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] (x : Charges 𝓩) :
    map (AddMonoidHom.id 𝓩) x = x
    theorem SuperSymmetry.SU5.Charges.map_ofFieldLabel {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩) (F : FieldLabel) :
    theorem SuperSymmetry.SU5.Charges.mem_map_ofPotentialTerm_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {i : 𝓩1} [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩) (T : PotentialTerm) :
    theorem SuperSymmetry.SU5.Charges.mem_map_ofPotentialTerm'_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {i : 𝓩1} [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩) (T : PotentialTerm) :
    theorem SuperSymmetry.SU5.Charges.map_subset {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {f : 𝓩 →+ 𝓩1} {x y : Charges 𝓩} (h : x y) :
    map f x map f y
    theorem SuperSymmetry.SU5.Charges.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
    theorem SuperSymmetry.SU5.Charges.map_allowsTerm {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : Charges 𝓩} {T : PotentialTerm} (h : x.AllowsTerm T) :
    (map f x).AllowsTerm T
    theorem SuperSymmetry.SU5.Charges.map_isPhenoConstrained {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (f : 𝓩 →+ 𝓩1) {x : Charges 𝓩} (h : x.IsPhenoConstrained) :
    theorem SuperSymmetry.SU5.Charges.map_isComplete_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] {f : 𝓩 →+ 𝓩1} {x : Charges 𝓩} :
    theorem SuperSymmetry.SU5.Charges.mem_map_ofYukawaTerms_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : Charges 𝓩} {i : 𝓩1} :
    theorem SuperSymmetry.SU5.Charges.mem_map_ofYukawaTermsNSum_iff {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] {f : 𝓩 →+ 𝓩1} {x : Charges 𝓩} {n : } {i : 𝓩1} :

    Preimage #

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

    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.
    Instances For
      theorem SuperSymmetry.SU5.Charges.preimageOfFinset_eq {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩1) :
      (preimageOfFinset S5 S10 f x) = {y : Charges 𝓩 | map f y = x y ofFinset S5 S10}
      def SuperSymmetry.SU5.Charges.preimageOfFinsetCard {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩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.
      Instances For
        theorem SuperSymmetry.SU5.Charges.preimageOfFinset_card_eq {𝓩 𝓩1 : Type} [AddCommGroup 𝓩] [AddCommGroup 𝓩1] [DecidableEq 𝓩1] [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : Charges 𝓩1) :