Charges

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

def SuperSymmetry.SU5.Charges : Type

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.

Equations

• SuperSymmetry.SU5.Charges = (Option ℤ × Option ℤ × Finset ℤ × Finset ℤ)

instance SuperSymmetry.SU5.Charges.instDecidableEq : DecidableEq Charges

Equations

• SuperSymmetry.SU5.Charges.instDecidableEq = inferInstanceAs (DecidableEq (Option ℤ × Option ℤ × Finset ℤ × Finset ℤ))

unsafe instance SuperSymmetry.SU5.Charges.instRepr : Repr Charges

Equations

• One or more equations did not get rendered due to their size.

def SuperSymmetry.SU5.Charges.toProd (x : Charges) : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ

The explicit casting of a term of Charges to a term of Option ℤ × Option ℤ × Finset ℤ × Finset ℤ.

Equations

• x.toProd = x

theorem SuperSymmetry.SU5.Charges.eq_of_parts {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

## Subsest relation

instance SuperSymmetry.SU5.Charges.hasSubset : HasSubset Charges

Equations

• One or more equations did not get rendered due to their size.

instance SuperSymmetry.SU5.Charges.hasSSubset : HasSSubset Charges

Equations

• SuperSymmetry.SU5.Charges.hasSSubset = { SSubset := fun (x y : SuperSymmetry.SU5.Charges) => x ⊆ y ∧ x ≠ y }

instance SuperSymmetry.SU5.Charges.subsetDecidable (x y : Charges) : Decidable (x ⊆ y)

Equations

• x.subsetDecidable y = instDecidableAnd

theorem SuperSymmetry.SU5.Charges.subset_def {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 (x : Charges) : x ⊆ x

theorem Option.toFinset_inj {x y : Option ℤ} : x = y ↔ x.toFinset = y.toFinset

theorem SuperSymmetry.SU5.Charges.subset_trans {x y z : Charges} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z

theorem SuperSymmetry.SU5.Charges.subset_antisymm {x y : Charges} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y

The empty charges

instance SuperSymmetry.SU5.Charges.emptyInst : EmptyCollection Charges

Equations

• SuperSymmetry.SU5.Charges.emptyInst = { emptyCollection := (none, none, ∅, ∅) }

@[simp]

theorem SuperSymmetry.SU5.Charges.empty_subset (x : Charges) : ∅ ⊆ x

@[simp]

theorem SuperSymmetry.SU5.Charges.subset_of_empty_iff_empty {x : Charges} : x ⊆ ∅ ↔ x = ∅

@[simp]

theorem SuperSymmetry.SU5.Charges.empty_qHd : ∅.1 = none

@[simp]

theorem SuperSymmetry.SU5.Charges.empty_qHu : ∅.2.1 = none

@[simp]

theorem SuperSymmetry.SU5.Charges.empty_Q5 : ∅.2.2.1 = ∅

@[simp]

theorem SuperSymmetry.SU5.Charges.empty_Q10 : ∅.2.2.2 = ∅

Card

def SuperSymmetry.SU5.Charges.card (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

• x.card = x.1.toFinset.card + x.2.1.toFinset.card + x.2.2.1.card + x.2.2.2.card

@[simp]

theorem SuperSymmetry.SU5.Charges.card_empty : ∅.card = 0

theorem SuperSymmetry.SU5.Charges.card_mono {x y : Charges} (h : x ⊆ y) : x.card ≤ y.card

theorem SuperSymmetry.SU5.Charges.eq_of_subset_card {x y : Charges} (h : x ⊆ y) (hcard : x.card = y.card) : x = y

Powerset

def Option.powerset (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

• none.powerset = {none}
• (some x_2).powerset = {none, some x_2}

@[simp]

theorem Option.mem_powerset_iff {x : Option ℤ} (y : Option ℤ) : y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset

def SuperSymmetry.SU5.Charges.powerset (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

• x.powerset = x.1.powerset.product (x.2.1.powerset.product (x.2.2.1.powerset.product x.2.2.2.powerset))

@[simp]

theorem SuperSymmetry.SU5.Charges.mem_powerset_iff_subset {x y : Charges} : x ∈ y.powerset ↔ x ⊆ y

theorem SuperSymmetry.SU5.Charges.self_mem_powerset (x : Charges) : x ∈ x.powerset

theorem SuperSymmetry.SU5.Charges.empty_mem_powerset (x : Charges) : ∅ ∈ x.powerset

@[simp]

theorem SuperSymmetry.SU5.Charges.powerset_of_empty : ∅.powerset = {∅}

theorem SuperSymmetry.SU5.Charges.powerset_mono {x y : Charges} : x.powerset ⊆ y.powerset ↔ x ⊆ y

theorem SuperSymmetry.SU5.Charges.min_exists_inductive (S : Finset Charges) (hS : S ≠ ∅) (n : ℕ) (hn : S.card = n) : ∃ y ∈ S, y.powerset ∩ S = {y}

theorem SuperSymmetry.SU5.Charges.min_exists (S : Finset Charges) (hS : S ≠ ∅) : ∃ y ∈ S, y.powerset ∩ S = {y}

ofFinset

def SuperSymmetry.SU5.Charges.ofFinset (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.

theorem SuperSymmetry.SU5.Charges.qHd_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x2 : Option ℤ × Finset ℤ × Finset ℤ) (hsub : (some z, x2) ∈ ofFinset S5 S10) : z ∈ S5

theorem SuperSymmetry.SU5.Charges.qHu_mem_ofFinset (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 (S5 S10 : Finset ℤ) {x : Charges} (hx : x ∈ ofFinset S5 S10) : x.2.2.1 ⊆ S5

theorem SuperSymmetry.SU5.Charges.mem_ofFinset_Q10_subset (S5 S10 : Finset ℤ) {x : Charges} (hx : x ∈ ofFinset S5 S10) : x.2.2.2 ⊆ S10

theorem SuperSymmetry.SU5.Charges.mem_ofFinset_antitone (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 {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 {S5 S5' S10 S10' : Finset ℤ} (h5 : S5 ⊆ S5') (h10 : S10 ⊆ S10') : ofFinset S5 S10 ⊆ ofFinset S5' S10'