PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5U1.Charges.Basic

Charges #

One of the data structures associated with the F-theory SU(5)+U(1) GUT model are the charges assocatied with the matter fields. In this module we define the type Charges, the elements of which correspond to the collection of charges associated with the matter content of a theory.

def FTheory.SU5U1.Charges :

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

Equations

FTheory.SU5U1.Charges = (Option ℤ × Option ℤ × Finset ℤ × Finset ℤ)

Instances For

instance FTheory.SU5U1.Charges.instDecidableEq :

DecidableEq Charges

Equations

FTheory.SU5U1.Charges.instDecidableEq = inferInstanceAs (DecidableEq (Option ℤ × Option ℤ × Finset ℤ × Finset ℤ))

unsafe instance FTheory.SU5U1.Charges.instRepr :

Equations

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

def FTheory.SU5U1.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

Instances For

theorem FTheory.SU5U1.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 FTheory.SU5U1.Charges.hasSubset :

HasSubset Charges

Equations

FTheory.SU5U1.Charges.hasSubset = { Subset := fun (x y : FTheory.SU5U1.Charges) => 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 }

instance FTheory.SU5U1.Charges.hasSSubset :

HasSSubset Charges

Equations

FTheory.SU5U1.Charges.hasSSubset = { SSubset := fun (x y : FTheory.SU5U1.Charges) => x ⊆ y ∧ x ≠ y }

instance FTheory.SU5U1.Charges.subsetDecidable (x y : Charges) :

Decidable (x ⊆ y)

Equations

x.subsetDecidable y = instDecidableAnd

theorem FTheory.SU5U1.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 FTheory.SU5U1.Charges.subset_refl (x : Charges) :

x ⊆ x

theorem Option.toFinset_inj {x y : Option ℤ} :

x = y ↔ x.toFinset = y.toFinset

theorem FTheory.SU5U1.Charges.subset_trans {x y z : Charges} (hxy : x ⊆ y) (hyz : y ⊆ z) :

x ⊆ z

theorem FTheory.SU5U1.Charges.subset_antisymm {x y : Charges} (hxy : x ⊆ y) (hyx : y ⊆ x) :

x = y

The empty charges #

instance FTheory.SU5U1.Charges.emptyInst :

EmptyCollection Charges

Equations

FTheory.SU5U1.Charges.emptyInst = { emptyCollection := (none , none , ∅, ∅) }

@[simp]

theorem FTheory.SU5U1.Charges.empty_subset (x : Charges) :

@[simp]

theorem FTheory.SU5U1.Charges.subset_of_empty_iff_empty {x : Charges} :

x ⊆ ∅ ↔ x = ∅

Card #

def FTheory.SU5U1.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

Instances For

@[simp]

theorem FTheory.SU5U1.Charges.card_empty :

theorem FTheory.SU5U1.Charges.card_subset_le {x y : Charges} (h : x ⊆ y) :

x.card ≤ y.card

theorem FTheory.SU5U1.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}

Instances For

@[simp]

theorem Option.mem_powerset_iff {x : Option ℤ} (y : Option ℤ) :

y ∈ x.powerset ↔ y.toFinset ⊆ x.toFinset

def FTheory.SU5U1.Charges.powerset (x : 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))

Instances For

@[simp]

theorem FTheory.SU5U1.Charges.mem_powerset_iff_subset {x y : Charges} :

x ∈ y.powerset ↔ x ⊆ y

theorem FTheory.SU5U1.Charges.self_mem_powerset (x : Charges) :

x ∈ x.powerset

theorem FTheory.SU5U1.Charges.empty_mem_powerset (x : Charges) :

∅ ∈ x.powerset

@[simp]

theorem FTheory.SU5U1.Charges.powerset_of_empty :

∅.powerset = {∅}

theorem FTheory.SU5U1.Charges.powerset_subset_iff_subset {x y : Charges} :

x.powerset ⊆ y.powerset ↔ x ⊆ y

theorem FTheory.SU5U1.Charges.min_exists_inductive (S : Finset Charges) (hS : S ≠ ∅) (n : ℕ) (hn : S.card = n) :

∃ y ∈ S, y.powerset ∩ S = {y}

theorem FTheory.SU5U1.Charges.min_exists (S : Finset Charges) (hS : S ≠ ∅) :

∃ y ∈ S, y.powerset ∩ S = {y}

ofFinset #

def FTheory.SU5U1.Charges.ofFinset (S5 S10 : Finset ℤ) :

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 FTheory.SU5U1.Charges.qHd_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x2 : Option ℤ × Finset ℤ × Finset ℤ) (hsub : (some z, x2) ∈ ofFinset S5 S10) :

z ∈ S5

theorem FTheory.SU5U1.Charges.qHu_mem_ofFinset (S5 S10 : Finset ℤ) (z : ℤ) (x1 : Option ℤ) (x2 : Finset ℤ × Finset ℤ) (hsub : (x1, some z, x2) ∈ ofFinset S5 S10) :

z ∈ S5

theorem FTheory.SU5U1.Charges.mem_ofFinset_Q5_subset (S5 S10 : Finset ℤ) {x : Charges} (hx : x ∈ ofFinset S5 S10) :

x.2.2.1 ⊆ S5

theorem FTheory.SU5U1.Charges.mem_ofFinset_Q10_subset (S5 S10 : Finset ℤ) {x : Charges} (hx : x ∈ ofFinset S5 S10) :

x.2.2.2 ⊆ S10

theorem FTheory.SU5U1.Charges.mem_ofFinset_of_subset (S5 S10 : Finset ℤ) {x y : Charges} (h : x ⊆ y) (hy : y ∈ ofFinset S5 S10) :

x ∈ ofFinset S5 S10

theorem FTheory.SU5U1.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 FTheory.SU5U1.Charges.ofFinset_subset_of_subset {S5 S5' S10 S10' : Finset ℤ} (h5 : S5 ⊆ S5') (h10 : S10 ⊆ S10') :

ofFinset S5 S10 ⊆ ofFinset S5' S10'

Minimal super set #

def FTheory.SU5U1.Charges.minimalSuperSet (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.

Equations

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

Instances For

theorem FTheory.SU5U1.Charges.self_subset_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :

x ⊆ y

@[simp]

theorem FTheory.SU5U1.Charges.self_not_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x : Charges) :

x ∉ minimalSuperSet S5 S10 x

theorem FTheory.SU5U1.Charges.self_neq_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :

x ≠ y

theorem FTheory.SU5U1.Charges.card_of_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :

y.card = x.card + 1

theorem FTheory.SU5U1.Charges.insert_Q5_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (z : ℤ) (hz : z ∈ S5) (hznot : z ∉ x.2.2.1) :

(x.1, x.2.1, insert z x.2.2.1, x.2.2.2) ∈ minimalSuperSet S5 S10 x

theorem FTheory.SU5U1.Charges.insert_Q10_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (z : ℤ) (hz : z ∈ S10) (hznot : z ∉ x.2.2.2) :

(x.1, x.2.1, x.2.2.1, insert z x.2.2.2) ∈ minimalSuperSet S5 S10 x

theorem FTheory.SU5U1.Charges.some_qHd_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ} {x2 : Option ℤ × Finset ℤ × Finset ℤ} (z : ℤ) (hz : z ∈ S5) :

(some z, x2) ∈ minimalSuperSet S5 S10 (none , x2)

theorem FTheory.SU5U1.Charges.some_qHu_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ} {x1 : Option ℤ} {x2 : Finset ℤ × Finset ℤ} (z : ℤ) (hz : z ∈ S5) :

(x1, some z, x2) ∈ minimalSuperSet S5 S10 (x1, none , x2)

theorem FTheory.SU5U1.Charges.exists_minimalSuperSet (S5 S10 : Finset ℤ) {x y : Charges} (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (hxneqy : x ≠ y) :

∃ z ∈ minimalSuperSet S5 S10 x, z ⊆ y

theorem FTheory.SU5U1.Charges.minimalSuperSet_induction_on_inductive {S5 S10 : Finset ℤ} (p : Charges → Prop) (hp : ∀ (x : Charges), p x → ∀ y ∈ minimalSuperSet S5 S10 x, p y) (x : Charges) (hbase : p x) (y : Charges) (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (n : ℕ) (hn : n = y.card - x.card) :

p y

Completions #

def FTheory.SU5U1.Charges.IsComplete (x : Charges) :

A collection of charges is complete if it has all types of fields.

Equations

x.IsComplete = (x.1.isSome = true ∧ x.2.1.isSome = true ∧ x.2.2.1 ≠ ∅ ∧ x.2.2.2 ≠ ∅)

Instances For

instance FTheory.SU5U1.Charges.instDecidableIsComplete (x : Charges) :

Decidable x.IsComplete

Equations

x.instDecidableIsComplete = inferInstanceAs (Decidable (x.1.isSome = true ∧ x.2.1.isSome = true ∧ x.2.2.1 ≠ ∅ ∧ x.2.2.2 ≠ ∅))

def FTheory.SU5U1.Charges.completions (S5 S10 : Finset ℤ) (x : Charges) :

Multiset 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 FTheory.SU5U1.Charges.completions_eq_singleton_of_complete {S5 S10 : Finset ℤ} (x : Charges) (hcomplete : x.IsComplete) :

completions S5 S10 x = {x}

@[simp]

theorem FTheory.SU5U1.Charges.self_mem_completions_iff_isComplete {S5 S10 : Finset ℤ} (x : Charges) :

x ∈ completions S5 S10 x ↔ x.IsComplete

theorem FTheory.SU5U1.Charges.mem_completions_isComplete {S5 S10 : Finset ℤ} {x y : Charges} (hx : y ∈ completions S5 S10 x) :

theorem FTheory.SU5U1.Charges.self_subset_mem_completions (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ completions S5 S10 x) :

x ⊆ y

theorem FTheory.SU5U1.Charges.exist_completions_subset_of_complete (S5 S10 : Finset ℤ) (x y : Charges) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (hycomplete : y.IsComplete) :

∃ z ∈ completions S5 S10 x, z ⊆ y