Properties of the 𝔤₂ root system.

The 𝔤₂ root pairing is special enough to deserve its own API. We provide one in this file.

As an application we prove the key result that a crystallographic, reduced, irreducible root pairing containing two roots of Coxeter weight three is spanned by this pair of roots (and thus is two-dimensional). This result is usually proved only for pairs of roots belonging to a base (as a corollary of the fact that no node can have degree greater than three) and moreover usually requires stronger assumptions on the coefficients than here.

Main results:

• RootPairing.EmbeddedG2: a data-bearing typeclass which distinguishes a pair of roots whose pairing is -3 (equivalently, with a distinguished choice of base). This is a sufficient condition for the span of this pair of roots to be a 𝔤₂ root system.
• RootPairing.IsG2: a prop-valued typeclass characterising the 𝔤₂ root system.
• RootPairing.IsNotG2: a prop-valued typeclass stating that a crystallographic, reduced, irreducible root system is not 𝔤₂.
• RootPairing.EmbeddedG2.shortRoot: the distinguished short root, which we often donate α
• RootPairing.EmbeddedG2.longRoot: the distinguished long root, which we often donate β
• RootPairing.EmbeddedG2.shortAddLong: the short root α + β
• RootPairing.EmbeddedG2.twoShortAddLong: the short root 2α + β
• RootPairing.EmbeddedG2.threeShortAddLong: the long root 3α + β
• RootPairing.EmbeddedG2.threeShortAddTwoLong: the long root 3α + 2β
• RootPairing.EmbeddedG2.span_eq_top: a crystallographic reduced irreducible root pairing containing two roots with pairing -3 is spanned by this pair (thus two-dimensional).
• RootPairing.EmbeddedG2.card_index_eq_twelve: the 𝔤₂root pairing has twelve roots.

TODO

Once sufficient API for RootPairing.Base has been developed:

• Add def EmbeddedG2.toBase [P.EmbeddedG2] : P.Base with support := {long P, short P}
• Given P satisfying [P.IsG2], distinct elements of a base must pair to -3 (in one order).

class RootPairing.EmbeddedG2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) extends P.IsValuedIn ℤ, P.IsReduced : Type u_1

A data-bearing typeclass which distinguishes a pair of roots whose pairing is -3. This is a sufficient condition for the span of this pair of roots to be a 𝔤₂ root system.

• exists_value (i j : ι) : ∃ (s : ℤ), (algebraMap ℤ R) s = P.pairing i j
• eq_or_eq_neg (i j : ι) (h : ¬LinearIndependent R ![P.root i, P.root j]) : P.root i = P.root j ∨ P.root i = -P.root j
• long : ι

  The distinguished long root of an embedded 𝔤₂ root pairing.

• short : ι

  The distinguished short root of an embedded 𝔤₂ root pairing.

• pairingIn_long_short : P.pairingIn ℤ (long P) (short P) = -3

class RootPairing.IsG2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) extends P.IsValuedIn ℤ, P.IsReduced, P.IsIrreducible : Prop

A prop-valued typeclass characterising the 𝔤₂ root system.

• exists_value (i j : ι) : ∃ (s : ℤ), (algebraMap ℤ R) s = P.pairing i j
• eq_or_eq_neg (i j : ι) (h : ¬LinearIndependent R ![P.root i, P.root j]) : P.root i = P.root j ∨ P.root i = -P.root j
• nontrivial : Nontrivial M
• nontrivial' : Nontrivial N
• eq_top_of_invtSubmodule_reflection (q : Submodule R M) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
• eq_top_of_invtSubmodule_coreflection (q : Submodule R N) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤
• exists_pairingIn_neg_three : ∃ (i : ι) (j : ι), P.pairingIn ℤ i j = -3

class RootPairing.IsNotG2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) extends P.IsValuedIn ℤ, P.IsReduced, P.IsIrreducible : Prop

A prop-valued typeclass stating that a crystallographic, reduced, irreducible root system is not 𝔤₂.

• exists_value (i j : ι) : ∃ (s : ℤ), (algebraMap ℤ R) s = P.pairing i j
• eq_or_eq_neg (i j : ι) (h : ¬LinearIndependent R ![P.root i, P.root j]) : P.root i = P.root j ∨ P.root i = -P.root j
• nontrivial : Nontrivial M
• nontrivial' : Nontrivial N
• eq_top_of_invtSubmodule_reflection (q : Submodule R M) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
• eq_top_of_invtSubmodule_coreflection (q : Submodule R N) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤
• pairingIn_mem_zero_one_two (i j : ι) : P.pairingIn ℤ i j ∈ {-2, -1, 0, 1, 2}

def RootPairing.IsG2.toEmbeddedG2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsG2] : P.EmbeddedG2

By making an arbitrary choice of roots pairing to -3, we can obtain an embedded 𝔤₂ root system just from the knowledge that such a pairs exists.

Equations

• RootPairing.IsG2.toEmbeddedG2 P = { toIsValuedIn := ⋯, toIsReduced := ⋯, long := ⋯.choose, short := ⋯.choose, pairingIn_long_short := ⋯ }

theorem RootPairing.IsG2.nonempty {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsG2] : Nonempty ι

theorem RootPairing.isG2_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] : P.IsG2 ↔ ∃ (i : ι) (j : ι), P.pairingIn ℤ i j = -3

theorem RootPairing.isNotG2_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] : P.IsNotG2 ↔ ∀ (i j : ι), P.pairingIn ℤ i j ∈ {-2, -1, 0, 1, 2}

@[simp]

theorem RootPairing.not_isG2_iff_isNotG2 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Finite ι] [CharZero R] [IsDomain R] : ¬P.IsG2 ↔ P.IsNotG2

theorem RootPairing.IsG2.pairingIn_mem_zero_one_three {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Finite ι] [CharZero R] [IsDomain R] [P.IsG2] (i j : ι) (h : P.root i ≠ P.root j) (h' : P.root i ≠ -P.root j) : P.pairingIn ℤ i j ∈ {-3, -1, 0, 1, 3}

theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le_two {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] (i j : ι) [P.IsNotG2] : chainBotCoeff i j + chainTopCoeff i j ≤ 2

theorem RootPairing.pairingIn_le_zero_of_root_add_mem {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] {i j : ι} [P.IsNotG2] (h : P.root i + P.root j ∈ Set.range ⇑P.root) : P.pairingIn ℤ i j ≤ 0

For a reduced, crystallographic, irreducible root pairing other than 𝔤₂, if the sum of two roots is a root, they cannot make an acute angle.

To see that this lemma fails for 𝔤₂, let α (short) and β (long) be a base. Then the roots α + β and 2α + β make an angle π / 3 even though 3α + 2β is a root. We can even witness as:

example (P : RootPairing ι R M N) [P.EmbeddedG2] :
    P.pairingIn ℤ (EmbeddedG2.shortAddLong P) (EmbeddedG2.twoShortAddLong P) = 1 := by
  simp

theorem RootPairing.zero_le_pairingIn_of_root_sub_mem {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] {i j : ι} [P.IsNotG2] (h : P.root i - P.root j ∈ Set.range ⇑P.root) : 0 ≤ P.pairingIn ℤ i j

theorem RootPairing.chainBotCoeff_if_one_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] {i j : ι} [P.IsNotG2] (h : P.root i + P.root j ∈ Set.range ⇑P.root) : chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0

For a reduced, crystallographic, irreducible root pairing other than 𝔤₂, if the sum of two roots is a root, the bottom chain coefficient is either one or zero according to whether they are perpendicular.

To see that this lemma fails for 𝔤₂, let α (short) and β (long) be a base. Then the roots α and α + β provide a counterexample.

theorem RootPairing.chainTopCoeff_if_one_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] {i j : ι} [P.IsNotG2] (h : P.root i - P.root j ∈ Set.range ⇑P.root) : chainTopCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0

def RootPairing.EmbeddedG2.ofPairingInThree {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] [P.IsCrystallographic] [P.IsReduced] (long short : ι) (h : P.pairingIn ℤ long short = 3) : P.EmbeddedG2

A pair of roots which pair to +3 are also sufficient to distinguish an embedded 𝔤₂.

Equations

• RootPairing.EmbeddedG2.ofPairingInThree P long short h = { toIsValuedIn := inst✝¹, toIsReduced := inst✝, long := (P.reflectionPerm long) long, short := short, pairingIn_long_short := ⋯ }

@[simp]

theorem RootPairing.EmbeddedG2.ofPairingInThree_short {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] [P.IsCrystallographic] [P.IsReduced] (long short : ι) (h : P.pairingIn ℤ long short = 3) : EmbeddedG2.short P = short

@[simp]

theorem RootPairing.EmbeddedG2.ofPairingInThree_long {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] [P.IsCrystallographic] [P.IsReduced] (long short : ι) (h : P.pairingIn ℤ long short = 3) : EmbeddedG2.long P = (P.reflectionPerm long) long

instance RootPairing.EmbeddedG2.instIsG2OfIsIrreducible {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [P.IsIrreducible] : P.IsG2

@[simp]

theorem RootPairing.EmbeddedG2.pairing_long_short {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : P.pairing (long P) (short P) = -3

def RootPairing.EmbeddedG2.shortAddLong {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : ι

The index of the root α + β where α is the short root and β is the long root.

Equations

• RootPairing.EmbeddedG2.shortAddLong P = (P.reflectionPerm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P)

def RootPairing.EmbeddedG2.twoShortAddLong {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : ι

The index of the root 2α + β where α is the short root and β is the long root.

Equations

• RootPairing.EmbeddedG2.twoShortAddLong P = (P.reflectionPerm (RootPairing.EmbeddedG2.short P)) ((P.reflectionPerm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P))

def RootPairing.EmbeddedG2.threeShortAddLong {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : ι

The index of the root 3α + β where α is the short root and β is the long root.

Equations

• RootPairing.EmbeddedG2.threeShortAddLong P = (P.reflectionPerm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P)

def RootPairing.EmbeddedG2.threeShortAddTwoLong {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : ι

The index of the root 3α + 2β where α is the short root and β is the long root.

Equations

• RootPairing.EmbeddedG2.threeShortAddTwoLong P = (P.reflectionPerm (RootPairing.EmbeddedG2.long P)) ((P.reflectionPerm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P))

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.shortRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The short root α.

Equations

• RootPairing.EmbeddedG2.shortRoot P = P.root (RootPairing.EmbeddedG2.short P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.longRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The long root β.

Equations

• RootPairing.EmbeddedG2.longRoot P = P.root (RootPairing.EmbeddedG2.long P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.shortAddLongRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The short root α + β.

Equations

• RootPairing.EmbeddedG2.shortAddLongRoot P = P.root (RootPairing.EmbeddedG2.shortAddLong P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.twoShortAddLongRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The short root 2α + β.

Equations

• RootPairing.EmbeddedG2.twoShortAddLongRoot P = P.root (RootPairing.EmbeddedG2.twoShortAddLong P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.threeShortAddLongRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The short root 3α + β.

Equations

• RootPairing.EmbeddedG2.threeShortAddLongRoot P = P.root (RootPairing.EmbeddedG2.threeShortAddLong P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.threeShortAddTwoLongRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : M

The short root 3α + 2β.

Equations

• RootPairing.EmbeddedG2.threeShortAddTwoLongRoot P = P.root (RootPairing.EmbeddedG2.threeShortAddTwoLong P)

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.allRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : List M

The list of all 12 roots belonging to the embedded 𝔤₂.

Equations

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

theorem RootPairing.EmbeddedG2.allRoots_subset_range_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [DecidableEq M] : ↑(allRoots P).toFinset ⊆ Set.range ⇑P.root

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_short_long {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : P.pairingIn ℤ (short P) (long P) = -1

@[simp]

theorem RootPairing.EmbeddedG2.pairing_short_long {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : P.pairing (short P) (long P) = -1

theorem RootPairing.EmbeddedG2.shortAddLongRoot_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : shortAddLongRoot P = shortRoot P + longRoot P

theorem RootPairing.EmbeddedG2.twoShortAddLongRoot_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : twoShortAddLongRoot P = 2 • shortRoot P + longRoot P

theorem RootPairing.EmbeddedG2.threeShortAddLongRoot_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] : threeShortAddLongRoot P = 3 • shortRoot P + longRoot P

theorem RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : threeShortAddTwoLongRoot P = 3 • shortRoot P + 2 • longRoot P

theorem RootPairing.EmbeddedG2.linearIndependent_short_long {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : LinearIndependent R ![shortRoot P, longRoot P]

@[reducible, inline]

abbrev RootPairing.EmbeddedG2.allCoeffs : List (Fin 2 → ℤ)

The coefficients of each root in the 𝔤₂ root pairing, relative to the base.

Equations

• RootPairing.EmbeddedG2.allCoeffs = [![0, 1], ![0, -1], ![1, 0], ![-1, 0], ![1, 1], ![-1, -1], ![2, 1], ![-2, -1], ![3, 1], ![-3, -1], ![3, 2], ![-3, -2]]

theorem RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : allRoots P = List.map (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P])) allCoeffs

theorem RootPairing.EmbeddedG2.allRoots_nodup {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] : (allRoots P).Nodup

theorem RootPairing.EmbeddedG2.mem_span_of_mem_allRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] {x : M} (hx : x ∈ allRoots P) : x ∈ Submodule.span ℤ {longRoot P, shortRoot P}

theorem RootPairing.EmbeddedG2.long_eq_three_mul_short {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (B : P.InvariantForm) : (B.form (longRoot P)) (longRoot P) = 3 * (B.form (shortRoot P)) (shortRoot P)

@[simp]

theorem RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.EmbeddedG2] (B : P.InvariantForm) : (B.form (shortAddLongRoot P)) (shortAddLongRoot P) = (B.form (shortRoot P)) (shortRoot P)

α + β is short.

@[simp]

theorem RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.EmbeddedG2] (B : P.InvariantForm) : (B.form (twoShortAddLongRoot P)) (twoShortAddLongRoot P) = (B.form (shortRoot P)) (shortRoot P)

2α + β is short.

@[simp]

theorem RootPairing.EmbeddedG2.threeShortAddLongRoot_longRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.EmbeddedG2] (B : P.InvariantForm) : (B.form (threeShortAddLongRoot P)) (threeShortAddLongRoot P) = (B.form (longRoot P)) (longRoot P)

3α + β is long.

@[simp]

theorem RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.EmbeddedG2] (B : P.InvariantForm) : (B.form (threeShortAddTwoLongRoot P)) (threeShortAddTwoLongRoot P) = (B.form (longRoot P)) (longRoot P)

3α + 2β is long.

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_shortAddLong_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_shortAddLong_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ i (shortAddLong P) = P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ i (twoShortAddLong P) = 2 * P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P)

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i

@[simp]

theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι) : P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 * P.pairingIn ℤ i (long P)

theorem RootPairing.EmbeddedG2.isOrthogonal_short_and_long {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] {i : ι} (hi : P.root i ∉ allRoots P) : P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)

@[simp]

theorem RootPairing.EmbeddedG2.span_eq_top {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] : Submodule.span R {longRoot P, shortRoot P} = ⊤

def RootPairing.EmbeddedG2.basis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] : Module.Basis (Fin 2) R M

The distinguished basis carried by an EmbeddedG2.

In fact this is a RootPairing.Base. TODO Upgrade to this stronger statement.

Equations

• RootPairing.EmbeddedG2.basis P = Module.Basis.mk ⋯ ⋯

theorem RootPairing.EmbeddedG2.mem_allRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] (i : ι) : P.root i ∈ allRoots P

def RootPairing.EmbeddedG2.indexEquivAllRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] : ι ≃ { x : M // x ∈ (allRoots P).toFinset }

The natural labelling of RootPairing.EmbeddedG2.allRoots.

Equations

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

@[simp]

theorem RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] (i : ι) : ↑((indexEquivAllRoots P) i) = P.root i

@[simp]

theorem RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] (x : { x : M // x ∈ (allRoots P).toFinset }) : (indexEquivAllRoots P).symm x = Exists.choose ⋯

theorem RootPairing.EmbeddedG2.card_index_eq_twelve {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] : Nat.card ι = 12

theorem RootPairing.EmbeddedG2.setOf_index_eq_univ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] : {long P, -long P, short P, -short P, shortAddLong P, -shortAddLong P, twoShortAddLong P, -twoShortAddLong P, threeShortAddLong P, -threeShortAddLong P, threeShortAddTwoLong P, -threeShortAddTwoLong P} = Set.univ

@[simp]

theorem RootPairing.IsG2.card_base_support_eq_two {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsG2] (b : P.Base) [Finite ι] [CharZero R] [IsDomain R] : b.support.card = 2

theorem RootPairing.IsG2.span_eq_rootSpan_int {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsG2] {b : P.Base} [Finite ι] [CharZero R] [IsDomain R] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) (h_ne : i ≠ j) : Submodule.span ℤ {P.root i, P.root j} = P.rootSpan ℤ