Completions of charges #
We say a set of charges is complete if it has all types of fields.
Given a collection of charges x
in ofFinset S5 S10
,
the completions of x
are the, minimimal charges y
in ofFinset S5 S10
which are a super sets
of x
and are complete.
This module defines the IsComplete
proposition and completions of charges and provides
lemmas about them.
Completions #
instance
SuperSymmetry.SU5.Charges.instDecidableIsCompleteOfDecidableEq
{𝓩 : Type}
[DecidableEq 𝓩]
(x : Charges 𝓩)
:
theorem
SuperSymmetry.SU5.Charges.isComplete_mono
{𝓩 : Type}
{x y : Charges 𝓩}
(h : x ⊆ y)
(hx : x.IsComplete)
:
Completions #
Note the completions are not monotonic with respect to the subset relation.
def
SuperSymmetry.SU5.Charges.completions
{𝓩 : Type}
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
(x : Charges 𝓩)
:
Given a collection of charges x
in ofFinset S5 S10
,
the minimimal charges y
in ofFinset S5 S10
which are a super sets of x
and are
complete.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SuperSymmetry.SU5.Charges.completions_nodup
{𝓩 : Type}
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
(x : Charges 𝓩)
:
(completions S5 S10 x).Nodup
theorem
SuperSymmetry.SU5.Charges.completions_eq_singleton_of_complete
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
(x : Charges 𝓩)
(hcomplete : x.IsComplete)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.self_mem_completions_iff_isComplete
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
(x : Charges 𝓩)
:
theorem
SuperSymmetry.SU5.Charges.mem_completions_isComplete
{𝓩 : Type}
[DecidableEq 𝓩]
{S5 S10 : Finset 𝓩}
{x y : Charges 𝓩}
(hx : y ∈ completions S5 S10 x)
:
theorem
SuperSymmetry.SU5.Charges.self_subset_mem_completions
{𝓩 : Type}
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
(x y : Charges 𝓩)
(hy : y ∈ completions S5 S10 x)
:
theorem
SuperSymmetry.SU5.Charges.exist_completions_subset_of_complete
{𝓩 : Type}
[DecidableEq 𝓩]
(S5 S10 : Finset 𝓩)
(x y : Charges 𝓩)
(hsubset : x ⊆ y)
(hy : y ∈ ofFinset S5 S10)
(hycomplete : y.IsComplete)
:
∃ z ∈ completions S5 S10 x, z ⊆ y
Completions of minimal top yukawa #
A fast version of completions
for an x
which is in
minimallyAllowsTermsOfFinset S5 S10 .topYukawa
.
Equations
Instances For
theorem
SuperSymmetry.SU5.Charges.completionsTopYukawa_nodup
{𝓩 : Type}
{S5 : Finset 𝓩}
(x : Charges 𝓩)
:
(completionsTopYukawa S5 x).Nodup
theorem
SuperSymmetry.SU5.Charges.completions_eq_completionsTopYukawa_of_mem_minimallyAllowsTermsOfFinset
{𝓩 : Type}
[DecidableEq 𝓩]
[AddCommGroup 𝓩]
{S5 S10 : Finset 𝓩}
(x : Charges 𝓩)
(hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 PotentialTerm.topYukawa)
: