Documentation

Mathlib.LinearAlgebra.RootSystem.Finite.g2

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 finite, 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.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 finite 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.

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

Instances

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) :

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.reflection_perm long) long, short := short, pairingIn_long_short := ⋯ }

Instances For

@[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) :

RootPairing.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) :

RootPairing.EmbeddedG2.long P = (P.reflection_perm long) long

@[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.reflection_perm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P)

Instances For

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.reflection_perm (RootPairing.EmbeddedG2.short P)) ((P.reflection_perm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P))

Instances For

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.reflection_perm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P)

Instances For

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.reflection_perm (RootPairing.EmbeddedG2.long P)) ((P.reflection_perm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P))

Instances For

@[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)

Instances For

@[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)

Instances For

@[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)

Instances For

@[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)

Instances For

@[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)

Instances For

@[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)

Instances For

@[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] :

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

Equations

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

Instances For

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

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]]

Instances For

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] [NoZeroSMulDivisors R M] :

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] [NoZeroSMulDivisors R M] :

(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] [NoZeroSMulDivisors R M] {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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] (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] [NoZeroSMulDivisors R M] {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] [NoZeroSMulDivisors R M] [P.IsIrreducible] :

Submodule.span R {longRoot P, shortRoot P} = ⊤

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] [NoZeroSMulDivisors R M] [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] [NoZeroSMulDivisors R M] [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.

Instances For

@[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] [NoZeroSMulDivisors R M] [P.IsIrreducible] (x : { x : M // x ∈ (allRoots P).toFinset }) :

(indexEquivAllRoots P).symm x = Exists.choose ⋯

@[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] [NoZeroSMulDivisors R M] [P.IsIrreducible] (i : ι) :

↑((indexEquivAllRoots P) i) = P.root i

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] [NoZeroSMulDivisors R M] [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] [NoZeroSMulDivisors R M] [P.IsIrreducible] :