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 ofU(1)
,β€ Γ β€
in the case ofU(1) Γ U(1)
,Fin 2
in the case ofβ€β
etc.
Equations
Instances For
Equations
- SuperSymmetry.SU5.Charges.instDecidableEq = inferInstanceAs (DecidableEq (Option π© Γ Option π© Γ Finset π© Γ Finset π©))
##Β Subsest relation
Equations
- One or more equations did not get rendered due to their size.
Equations
- SuperSymmetry.SU5.Charges.hasSSubset = { SSubset := fun (x y : SuperSymmetry.SU5.Charges π©) => x β y β§ x β y }
Equations
The empty charges #
Card #
Powerset #
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
ofFinset #
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.