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

def SuperSymmetry.SU5.Charges.IsComplete (x : Charges) : Prop

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 ≠ ∅)

instance SuperSymmetry.SU5.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 ≠ ∅))

@[simp]

theorem SuperSymmetry.SU5.Charges.not_isComplete_empty : ¬∅.IsComplete

theorem SuperSymmetry.SU5.Charges.isComplete_mono {x y : Charges} (h : x ⊆ y) (hx : x.IsComplete) : y.IsComplete

Completions

Note the completions are not monotonic with respect to the subset relation.

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

theorem SuperSymmetry.SU5.Charges.completions_eq_singleton_of_complete {S5 S10 : Finset ℤ} (x : Charges) (hcomplete : x.IsComplete) : completions S5 S10 x = {x}

@[simp]

theorem SuperSymmetry.SU5.Charges.self_mem_completions_iff_isComplete {S5 S10 : Finset ℤ} (x : Charges) : x ∈ completions S5 S10 x ↔ x.IsComplete

theorem SuperSymmetry.SU5.Charges.mem_completions_isComplete {S5 S10 : Finset ℤ} {x y : Charges} (hx : y ∈ completions S5 S10 x) : y.IsComplete

theorem SuperSymmetry.SU5.Charges.self_subset_mem_completions (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ completions S5 S10 x) : x ⊆ y

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