PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.Basic

Charges #

The data structure associated with additional charges in the SU(5) GUT model.

These charges are permitted to sit within any type 𝓩 which is usually taken to be β„€ (for U(1) charges) or multiples thereof.

The type such that an element corresponds to the collection of charges associated with the matter content of the theory. The order of charges is implicitly taken to be qHd, qHu, Q5, Q10.

The Q5 and Q10 charges are represented by Finset rather than Multiset, so multiplicity is not included.

This is defined for a general type 𝓩, which could be e.g.

  • β„€ in the case of U(1),
  • β„€ Γ— β„€ in the case of U(1) Γ— U(1),
  • Fin 2 in the case of β„€β‚‚ etc.
Equations
Instances For
    def SuperSymmetry.SU5.Charges.toProd {𝓩 : Type} (x : Charges 𝓩) :
    Option 𝓩 Γ— Option 𝓩 Γ— Finset 𝓩 Γ— Finset 𝓩

    The explicit casting of a term of type Charges 𝓩 to a term of Option 𝓩 Γ— Option 𝓩 Γ— Finset 𝓩 Γ— Finset 𝓩.

    Equations
    Instances For
      theorem SuperSymmetry.SU5.Charges.eq_of_parts {𝓩 : Type} {x y : Charges 𝓩} (h1 : x.1 = y.1) (h2 : x.2.1 = y.2.1) (h3 : x.2.2.1 = y.2.2.1) (h4 : x.2.2.2 = y.2.2.2) :
      x = y
      theorem SuperSymmetry.SU5.Charges.eq_iff {𝓩 : Type} {x y : Charges 𝓩} :
      x = y ↔ x.1 = y.1 ∧ x.2.1 = y.2.1 ∧ x.2.2.1 = y.2.2.1 ∧ x.2.2.2 = y.2.2.2

      Basic instances on the type Charges 𝓩. #

      unsafe instance SuperSymmetry.SU5.Charges.instRepr {𝓩 : Type} [Repr 𝓩] :
      Repr (Charges 𝓩)
      Equations
      • One or more equations did not get rendered due to their size.

      ##Β Subsest relation

      instance SuperSymmetry.SU5.Charges.hasSubset {𝓩 : Type} :
      HasSubset (Charges 𝓩)
      Equations
      • One or more equations did not get rendered due to their size.
      theorem SuperSymmetry.SU5.Charges.subset_def {𝓩 : Type} {x y : Charges 𝓩} :
      x βŠ† y ↔ x.1.toFinset βŠ† y.1.toFinset ∧ x.2.1.toFinset βŠ† y.2.1.toFinset ∧ x.2.2.1 βŠ† y.2.2.1 ∧ x.2.2.2 βŠ† y.2.2.2
      @[simp]
      theorem SuperSymmetry.SU5.Charges.subset_refl {𝓩 : Type} (x : Charges 𝓩) :
      x βŠ† x
      theorem Option.toFinset_inj {𝓩 : Type} {x y : Option 𝓩} :
      theorem SuperSymmetry.SU5.Charges.subset_trans {𝓩 : Type} {x y z : Charges 𝓩} (hxy : x βŠ† y) (hyz : y βŠ† z) :
      x βŠ† z
      theorem SuperSymmetry.SU5.Charges.subset_antisymm {𝓩 : Type} {x y : Charges 𝓩} (hxy : x βŠ† y) (hyx : y βŠ† x) :
      x = y

      The empty charges #

      @[simp]
      theorem SuperSymmetry.SU5.Charges.empty_subset {𝓩 : Type} (x : Charges 𝓩) :
      @[simp]
      @[simp]
      @[simp]

      Card #

      def SuperSymmetry.SU5.Charges.card {𝓩 : Type} (x : Charges 𝓩) :

      The cardinality of a Charges is defined to be the sum of the cardinalities of each of the underlying finite sets of charges, with Option β„€ turned to finsets.

      Equations
      Instances For
        theorem SuperSymmetry.SU5.Charges.card_mono {𝓩 : Type} {x y : Charges 𝓩} (h : x βŠ† y) :
        theorem SuperSymmetry.SU5.Charges.eq_of_subset_card {𝓩 : Type} {x y : Charges 𝓩} (h : x βŠ† y) (hcard : x.card = y.card) :
        x = y

        Powerset #

        def Option.powerset {𝓩 : Type} [DecidableEq 𝓩] (x : Option 𝓩) :
        Finset (Option 𝓩)

        The powerset of x : Option 𝓩 defined as {none} if x is none and {none, some y} is x is some y.

        Equations
        Instances For
          @[simp]
          theorem Option.mem_powerset_iff {𝓩 : Type} [DecidableEq 𝓩] {x : Option 𝓩} (y : Option 𝓩) :
          def SuperSymmetry.SU5.Charges.powerset {𝓩 : Type} [DecidableEq 𝓩] (x : Charges 𝓩) :
          Finset (Charges 𝓩)

          The powerset of a charge . Given a charge x : Charges it's powerset is the finite set of all Charges which are subsets of x.

          Equations
          Instances For
            @[simp]
            theorem SuperSymmetry.SU5.Charges.mem_powerset_iff_subset {𝓩 : Type} [DecidableEq 𝓩] {x y : Charges 𝓩} :
            theorem SuperSymmetry.SU5.Charges.self_mem_powerset {𝓩 : Type} [DecidableEq 𝓩] (x : Charges 𝓩) :
            theorem SuperSymmetry.SU5.Charges.min_exists_inductive {𝓩 : Type} [DecidableEq 𝓩] (S : Finset (Charges 𝓩)) (hS : S β‰  βˆ…) (n : β„•) (hn : S.card = n) :
            βˆƒ y ∈ S, y.powerset ∩ S = {y}
            theorem SuperSymmetry.SU5.Charges.min_exists {𝓩 : Type} [DecidableEq 𝓩] (S : Finset (Charges 𝓩)) (hS : S β‰  βˆ…) :
            βˆƒ y ∈ S, y.powerset ∩ S = {y}

            ofFinset #

            def SuperSymmetry.SU5.Charges.ofFinset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) :
            Finset (Charges 𝓩)

            Given S5 S10 : Finset 𝓩 the finite set of charges associated with for which the 5-bar representation charges sit in S5 and the 10d representation charges sit in S10.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem SuperSymmetry.SU5.Charges.qHd_mem_ofFinset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (z : 𝓩) (x2 : Option 𝓩 Γ— Finset 𝓩 Γ— Finset 𝓩) (hsub : (some z, x2) ∈ ofFinset S5 S10) :
              z ∈ S5
              theorem SuperSymmetry.SU5.Charges.qHu_mem_ofFinset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) (z : 𝓩) (x1 : Option 𝓩) (x2 : Finset 𝓩 Γ— Finset 𝓩) (hsub : (x1, some z, x2) ∈ ofFinset S5 S10) :
              z ∈ S5
              theorem SuperSymmetry.SU5.Charges.mem_ofFinset_Q5_subset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x : Charges 𝓩} (hx : x ∈ ofFinset S5 S10) :
              x.2.2.1 βŠ† S5
              theorem SuperSymmetry.SU5.Charges.mem_ofFinset_Q10_subset {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x : Charges 𝓩} (hx : x ∈ ofFinset S5 S10) :
              x.2.2.2 βŠ† S10
              theorem SuperSymmetry.SU5.Charges.mem_ofFinset_antitone {𝓩 : Type} [DecidableEq 𝓩] (S5 S10 : Finset 𝓩) {x y : Charges 𝓩} (h : x βŠ† y) (hy : y ∈ ofFinset S5 S10) :
              x ∈ ofFinset S5 S10
              theorem SuperSymmetry.SU5.Charges.mem_ofFinset_iff {𝓩 : Type} [DecidableEq 𝓩] {S5 S10 : Finset 𝓩} {x : Charges 𝓩} :
              x ∈ ofFinset S5 S10 ↔ x.1.toFinset βŠ† S5 ∧ x.2.1.toFinset βŠ† S5 ∧ x.2.2.1 βŠ† S5 ∧ x.2.2.2 βŠ† S10
              theorem SuperSymmetry.SU5.Charges.ofFinset_subset_of_subset {𝓩 : Type} [DecidableEq 𝓩] {S5 S5' S10 S10' : Finset 𝓩} (h5 : S5 βŠ† S5') (h10 : S10 βŠ† S10') :
              ofFinset S5 S10 βŠ† ofFinset S5' S10'