Minimally allows a finite set of terms #
Given a set of charges x : Charges
corresponding to charges of the representations
present in the theory, and a finite set of
potential terms Ts : Finset PotentialTerm
, we say that x
minimally allows Ts
if it allows each term in Ts
and no proper subset of x
allows
each term in Ts
.
def
SuperSymmetry.SU5.Charges.MinimallyAllowsFinsetTerms
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(Ts : Finset PotentialTerm)
:
A collection of charges x : Charges
is said to minimally allow
a finite set of potential terms Ts
if it allows
all terms in Ts
and no strict subset of it allows all terms in Ts
.
Equations
- x.MinimallyAllowsFinsetTerms Ts = ∀ y ∈ x.powerset, y = x ↔ ∀ T ∈ Ts, y.AllowsTerm T
Instances For
instance
SuperSymmetry.SU5.Charges.instDecidableMinimallyAllowsFinsetTerms
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(x : Charges 𝓩)
(Ts : Finset PotentialTerm)
:
Equations
- x.instDecidableMinimallyAllowsFinsetTerms Ts = inferInstanceAs (Decidable (∀ y ∈ x.powerset, y = x ↔ ∀ T ∈ Ts, y.AllowsTerm T))
theorem
SuperSymmetry.SU5.Charges.allowsTerm_of_minimallyAllowsFinsetTerms
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{Ts : Finset PotentialTerm}
{x : Charges 𝓩}
{T : PotentialTerm}
(h : x.MinimallyAllowsFinsetTerms Ts)
(hT : T ∈ Ts)
:
x.AllowsTerm T
@[simp]
theorem
SuperSymmetry.SU5.Charges.minimallyAllowsFinsetTerms_singleton
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{x : Charges 𝓩}
{T : PotentialTerm}
:
Minimally allows top and bottom Yukawa #
def
SuperSymmetry.SU5.Charges.minTopBottom
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
:
The set of charges of the form (qHd, qHu, {q5}, {-qHd-q5, q10, qHu - q10})
This includes every charge which minimally allows for the top and bottom Yukawas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SuperSymmetry.SU5.Charges.allowsTerm_topYukawa_of_mem_minTopBottom
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x : Charges 𝓩}
(h : x ∈ minTopBottom S5 S10)
:
theorem
SuperSymmetry.SU5.Charges.allowsTerm_bottomYukawa_of_mem_minTopBottom
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x : Charges 𝓩}
(h : x ∈ minTopBottom S5 S10)
:
theorem
SuperSymmetry.SU5.Charges.mem_minTopBottom_of_minimallyAllowsFinsetTerms
{𝓩 : Type}
[AddCommGroup 𝓩]
[DecidableEq 𝓩]
{x : Charges 𝓩}
{S5 S10 : Finset 𝓩}
(h : x.MinimallyAllowsFinsetTerms {PotentialTerm.topYukawa, PotentialTerm.bottomYukawa})
(hx : x ∈ ofFinset S5 S10)
: