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

TODO #

Once sufficient API for RootPairing.Base has been developed:

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.

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

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

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

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

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

        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
        Instances For
          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] :
          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] :
          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] :
          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) :

          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) :
          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
          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) :
            @[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) :
            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] :
            @[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
            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
              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
                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
                  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
                    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
                      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
                        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
                          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
                            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
                              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] :
                                  @[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] :
                                  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] :
                                  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] :
                                  @[reducible, inline]

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

                                  Equations
                                  Instances For
                                    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] :
                                    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) :
                                    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) :

                                    α + β 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) :

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

                                    3α + β is long.

                                    @[simp]

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

                                    The distinguished basis carried by an EmbeddedG2.

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

                                    Equations
                                    Instances For
                                      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 : ι) :
                                      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.
                                      Instances For
                                        @[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 }) :
                                        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
                                        @[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] :
                                        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) :