Documentation

Mathlib.LinearAlgebra.RootSystem.Hom

Morphisms of root pairings #

This file defines morphisms of root pairings, following the definition of morphisms of root data given in SGA III Exp. 21 Section 6.

Main definitions: #

TODO #

structure RootPairing.Hom {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) :
Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)

A morphism of root pairings is a pair of mutually transposed maps of weight and coweight spaces that preserves roots and coroots. We make the map of indexing sets explicit.

  • weightMap : M →ₗ[R] M₂

    A linear map on weight space.

  • coweightMap : N₂ →ₗ[R] N

    A contravariant linear map on coweight space.

  • indexEquiv : ι ι₂

    A bijection on index sets.

  • weight_coweight_transpose : self.weightMap.dualMap ∘ₗ Q.toDualRight = P.toDualRight ∘ₗ self.coweightMap
  • root_weightMap : self.weightMap P.root = Q.root self.indexEquiv
  • coroot_coweightMap : self.coweightMap Q.coroot = P.coroot self.indexEquiv.symm
Instances For
    theorem RootPairing.Hom.ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst✝ : CommRing R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst✝⁵ : AddCommGroup M₂} {inst✝⁶ : Module R M₂} {inst✝⁷ : AddCommGroup N₂} {inst✝⁸ : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Hom Q} (weightMap : x.weightMap = y.weightMap) (coweightMap : x.coweightMap = y.coweightMap) (indexEquiv : x.indexEquiv = y.indexEquiv) :
    x = y
    theorem RootPairing.Hom.weight_coweight_transpose_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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (x : N₂) (f : P.Hom Q) :
    f.weightMap.dualMap (Q.toDualRight x) = P.toDualRight (f.coweightMap x)
    theorem RootPairing.Hom.root_weightMap_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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι) (f : P.Hom Q) :
    f.weightMap (P.root i) = Q.root (f.indexEquiv i)
    theorem RootPairing.Hom.coroot_coweightMap_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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι₂) (f : P.Hom Q) :
    f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i)
    def RootPairing.Hom.id {ι : 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.Hom P

    The identity morphism of a root pairing.

    Equations
    • RootPairing.Hom.id P = { weightMap := LinearMap.id, coweightMap := LinearMap.id, indexEquiv := Equiv.refl ι, weight_coweight_transpose := , root_weightMap := , coroot_coweightMap := }
    Instances For
      @[simp]
      theorem RootPairing.Hom.id_indexEquiv_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) (a : ι) :
      (RootPairing.Hom.id P).indexEquiv.symm a = a
      @[simp]
      theorem RootPairing.Hom.id_coweightMap_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) (a : N) :
      (RootPairing.Hom.id P).coweightMap a = a
      @[simp]
      theorem RootPairing.Hom.id_weightMap_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) (a : M) :
      (RootPairing.Hom.id P).weightMap a = a
      @[simp]
      theorem RootPairing.Hom.id_indexEquiv_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) (a : ι) :
      (RootPairing.Hom.id P).indexEquiv a = a
      def RootPairing.Hom.comp {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) :
      P.Hom P₂

      Composition of morphisms

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem RootPairing.Hom.comp_coweightMap_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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a✝ : N₂) :
        (g.comp f).coweightMap a✝ = f.coweightMap (g.coweightMap a✝)
        @[simp]
        theorem RootPairing.Hom.comp_indexEquiv_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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a✝ : ι) :
        (g.comp f).indexEquiv a✝ = g.indexEquiv (f.indexEquiv a✝)
        @[simp]
        theorem RootPairing.Hom.comp_indexEquiv_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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a✝ : ι₂) :
        (g.comp f).indexEquiv.symm a✝ = f.indexEquiv.symm (g.indexEquiv.symm a✝)
        @[simp]
        theorem RootPairing.Hom.comp_weightMap_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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (a✝ : M) :
        (g.comp f).weightMap a✝ = g.weightMap (f.weightMap a✝)
        @[simp]
        theorem RootPairing.Hom.id_comp {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Hom Q) :
        f.comp (RootPairing.Hom.id P) = f
        @[simp]
        theorem RootPairing.Hom.comp_id {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Hom Q) :
        (RootPairing.Hom.id Q).comp f = f
        @[simp]
        theorem RootPairing.Hom.comp_assoc {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7} {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} {ι₃ : Type u_11} {M₃ : Type u_12} {N₃ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃} (h : P₂.Hom P₃) (g : P₁.Hom P₂) (f : P.Hom P₁) :
        (h.comp g).comp f = h.comp (g.comp f)
        instance RootPairing.Hom.instMonoid {ι : 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) :
        Monoid (P.Hom P)

        The endomorphism monoid of a root pairing.

        Equations
        @[simp]
        theorem RootPairing.Hom.weightMap_one {ι : 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) :
        @[simp]
        theorem RootPairing.Hom.coweightMap_one {ι : 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) :
        @[simp]
        theorem RootPairing.Hom.indexEquiv_one {ι : 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) :
        @[simp]
        theorem RootPairing.Hom.weightMap_mul {ι : 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) (x y : P.Hom P) :
        (x * y).weightMap = x.weightMap ∘ₗ y.weightMap
        @[simp]
        theorem RootPairing.Hom.coweightMap_mul {ι : 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) (x y : P.Hom P) :
        (x * y).coweightMap = y.coweightMap ∘ₗ x.coweightMap
        @[simp]
        theorem RootPairing.Hom.indexEquiv_mul {ι : 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) (x y : P.Hom P) :
        (x * y).indexEquiv = x.indexEquiv y.indexEquiv
        @[reducible, inline]
        abbrev RootPairing.End {ι : 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) :
        Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)

        The endomorphism monoid of a root pairing.

        Equations
        • P.End = P.Hom P
        Instances For
          def RootPairing.Hom.weightHom {ι : 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.End →* Module.End R M

          The weight space representation of endomorphisms

          Equations
          Instances For
            theorem RootPairing.Hom.weightHom_injective {ι : 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) :
            def RootPairing.Hom.coweightHom {ι : 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.End →* (N →ₗ[R] N)ᵐᵒᵖ

            The coweight space representation of endomorphisms

            Equations
            Instances For
              theorem RootPairing.Hom.coweightHom_injective {ι : 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) :
              def RootPairing.Hom.indexHom {ι : 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.End →* ι ι

              The permutation representation of the endomorphism monoid on the root index set

              Equations
              Instances For
                structure RootPairing.Equiv {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) extends P.Hom Q :
                Type (max (max (max (max (max u_1 u_3) u_4) u_5) u_6) u_7)

                An equivalence of root pairings is a morphism where the maps of weight and coweight spaces are bijective.

                See also RootPairing.Equiv.toEndUnit.

                Instances For
                  theorem RootPairing.Equiv.ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst✝ : CommRing R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst✝⁵ : AddCommGroup M₂} {inst✝⁶ : Module R M₂} {inst✝⁷ : AddCommGroup N₂} {inst✝⁸ : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Equiv Q} (weightMap : (↑x).weightMap = (↑y).weightMap) (coweightMap : (↑x).coweightMap = (↑y).coweightMap) (indexEquiv : (↑x).indexEquiv = (↑y).indexEquiv) :
                  x = y
                  def RootPairing.Equiv.weightEquiv {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) :
                  M ≃ₗ[R] M₂

                  The linear equivalence of weight spaces given by an equivalence of root pairings.

                  Equations
                  Instances For
                    @[simp]
                    theorem RootPairing.Equiv.weightEquiv_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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M) :
                    (RootPairing.Equiv.weightEquiv P Q e) m = (↑e).weightMap m
                    @[simp]
                    theorem RootPairing.Equiv.weightEquiv_symm_weightMap {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M) :
                    (RootPairing.Equiv.weightEquiv P Q e).symm ((↑e).weightMap m) = m
                    @[simp]
                    theorem RootPairing.Equiv.weightMap_weightEquiv_symm {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M₂) :
                    (↑e).weightMap ((RootPairing.Equiv.weightEquiv P Q e).symm m) = m
                    def RootPairing.Equiv.coweightEquiv {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) :
                    N₂ ≃ₗ[R] N

                    The contravariant equivalence of coweight spaces given by an equivalence of root pairings.

                    Equations
                    Instances For
                      @[simp]
                      theorem RootPairing.Equiv.coweightEquiv_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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N₂) :
                      (RootPairing.Equiv.coweightEquiv P Q e) n = (↑e).coweightMap n
                      @[simp]
                      theorem RootPairing.Equiv.coweightEquiv_symm_coweightMap {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N₂) :
                      (RootPairing.Equiv.coweightEquiv P Q e).symm ((↑e).coweightMap n) = n
                      @[simp]
                      theorem RootPairing.Equiv.coweightMap_coweightEquiv_symm {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N) :
                      (↑e).coweightMap ((RootPairing.Equiv.coweightEquiv P Q e).symm n) = n
                      def RootPairing.Equiv.id {ι : 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.Equiv P

                      The identity equivalence of a root pairing.

                      Equations
                      Instances For
                        @[simp]
                        theorem RootPairing.Equiv.id_indexEquiv_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) (a : ι) :
                        (↑(RootPairing.Equiv.id P)).indexEquiv.symm a = a
                        @[simp]
                        theorem RootPairing.Equiv.id_indexEquiv_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) (a : ι) :
                        (↑(RootPairing.Equiv.id P)).indexEquiv a = a
                        @[simp]
                        theorem RootPairing.Equiv.id_coweightMap_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) (a : N) :
                        (↑(RootPairing.Equiv.id P)).coweightMap a = a
                        @[simp]
                        theorem RootPairing.Equiv.id_weightMap_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) (a : M) :
                        (↑(RootPairing.Equiv.id P)).weightMap a = a
                        def RootPairing.Equiv.comp {ι : 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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) :
                        P.Equiv P₂

                        Composition of equivalences

                        Equations
                        • g.comp f = { toHom := (↑g).comp f, bijective_weightMap := , bijective_coweightMap := }
                        Instances For
                          @[simp]
                          theorem RootPairing.Equiv.comp_indexEquiv_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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) (a✝ : ι) :
                          (↑(g.comp f)).indexEquiv a✝ = (↑g).indexEquiv ((↑f).indexEquiv a✝)
                          @[simp]
                          theorem RootPairing.Equiv.comp_coweightMap_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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) (a✝ : N₂) :
                          (↑(g.comp f)).coweightMap a✝ = (↑f).coweightMap ((↑g).coweightMap a✝)
                          @[simp]
                          theorem RootPairing.Equiv.comp_indexEquiv_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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) (a✝ : ι₂) :
                          (↑(g.comp f)).indexEquiv.symm a✝ = (↑f).indexEquiv.symm ((↑g).indexEquiv.symm a✝)
                          @[simp]
                          theorem RootPairing.Equiv.comp_weightMap_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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) (a✝ : M) :
                          (↑(g.comp f)).weightMap a✝ = (↑g).weightMap ((↑f).weightMap a✝)
                          @[simp]
                          theorem RootPairing.Equiv.toHom_comp {ι : 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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Equiv P₂) (f : P.Equiv P₁) :
                          (g.comp f) = (↑g).comp f
                          @[simp]
                          theorem RootPairing.Equiv.id_comp {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                          f.comp (RootPairing.Equiv.id P) = f
                          @[simp]
                          theorem RootPairing.Equiv.comp_id {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                          (RootPairing.Equiv.id Q).comp f = f
                          @[simp]
                          theorem RootPairing.Equiv.comp_assoc {ι : 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] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10} {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} {ι₃ : Type u_14} {M₃ : Type u_15} {N₃ : Type u_16} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃} (h : P₂.Equiv P₃) (g : P₁.Equiv P₂) (f : P.Equiv P₁) :
                          (h.comp g).comp f = h.comp (g.comp f)
                          instance RootPairing.Equiv.instMonoid {ι : 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) :
                          Monoid (P.Equiv P)

                          Equivalences form a monoid.

                          Equations
                          @[simp]
                          theorem RootPairing.Equiv.weightEquiv_one {ι : 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) :
                          (RootPairing.Equiv.weightEquiv P P 1) = LinearMap.id
                          @[simp]
                          theorem RootPairing.Equiv.coweightEquiv_one {ι : 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) :
                          (RootPairing.Equiv.coweightEquiv P P 1) = LinearMap.id
                          @[simp]
                          theorem RootPairing.Equiv.toHom_one {ι : 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) :
                          1 = 1
                          @[simp]
                          theorem RootPairing.Equiv.mul_eq_comp {ι : 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} (x y : P.Equiv P) :
                          x * y = x.comp y
                          @[simp]
                          theorem RootPairing.Equiv.weightEquiv_comp_toLin {ι : 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} (x y : P.Equiv P) :
                          @[simp]
                          theorem RootPairing.Equiv.weightEquiv_mul {ι : 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} (x y : P.Equiv P) :
                          @[simp]
                          theorem RootPairing.Equiv.coweightEquiv_comp_toLin {ι : 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} (x y : P.Equiv P) :
                          @[simp]
                          theorem RootPairing.Equiv.coweightEquiv_mul {ι : 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} (x y : P.Equiv P) :
                          def RootPairing.Equiv.symm {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                          Q.Equiv P

                          The inverse of a root pairing equivalence.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem RootPairing.Equiv.inv_weightMap {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                            (↑(RootPairing.Equiv.symm P Q f)).weightMap = (RootPairing.Equiv.weightEquiv P Q f).symm
                            @[simp]
                            theorem RootPairing.Equiv.inv_coweightMap {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                            (↑(RootPairing.Equiv.symm P Q f)).coweightMap = (RootPairing.Equiv.coweightEquiv P Q f).symm
                            @[simp]
                            theorem RootPairing.Equiv.inv_indexEquiv {ι : 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] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q) :
                            (↑(RootPairing.Equiv.symm P Q f)).indexEquiv = (↑f).indexEquiv.symm
                            instance RootPairing.Equiv.instGroup {ι : 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) :
                            Group (P.Equiv P)

                            Equivalences form a group.

                            Equations
                            @[reducible, inline]
                            abbrev RootPairing.Aut {ι : 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) :
                            Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)

                            The automorphism group of a root pairing.

                            Equations
                            • P.Aut = P.Equiv P
                            Instances For
                              def RootPairing.Equiv.toEndUnit {ι : 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.Aut ≃* P.Endˣ

                              The isomorphism between the automorphism group of a root pairing and the group of invertible endomorphisms.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem RootPairing.Equiv.toEndUnit_val {ι : 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) (g : P.Aut) :
                                theorem RootPairing.Equiv.toEndUnit_inv {ι : 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) (g : P.Aut) :
                                def RootPairing.Equiv.weightHom {ι : 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.Aut →* M ≃ₗ[R] M

                                The weight space representation of automorphisms

                                Equations
                                Instances For
                                  @[simp]
                                  theorem RootPairing.Equiv.weightHom_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) (e : P.Equiv P) :
                                  theorem RootPairing.Equiv.weightHom_toLinearMap {ι : 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} (g : P.Aut) :
                                  theorem RootPairing.Equiv.weightHom_injective {ι : 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) :
                                  @[simp]
                                  theorem RootPairing.Equiv.weightEquiv_inv {ι : 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} (g : P.Aut) :
                                  def RootPairing.Equiv.coweightHom {ι : 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.Aut →* (N ≃ₗ[R] N)ᵐᵒᵖ

                                  The coweight space representation of automorphisms

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem RootPairing.Equiv.coweightHom_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) (g : P.Aut) :
                                    theorem RootPairing.Equiv.coweightHom_toLinearMap {ι : 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} (g : P.Aut) :
                                    theorem RootPairing.Equiv.coweightHom_op {ι : 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} (g : P.Aut) :
                                    @[simp]
                                    theorem RootPairing.Equiv.coweightEquiv_inv {ι : 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} (g : P.Aut) :
                                    def RootPairing.Equiv.indexHom {ι : 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.Aut →* ι ι

                                    The permutation representation of the automorphism group on the root index set

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem RootPairing.Equiv.indexHom_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) (g : P.Aut) :
                                      (RootPairing.Equiv.indexHom P) g = (↑g).indexEquiv
                                      @[simp]
                                      theorem RootPairing.Equiv.indexEquiv_inv {ι : 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} (g : P.Aut) :
                                      (↑g⁻¹).indexEquiv = ((RootPairing.Equiv.indexHom P) g)⁻¹
                                      def RootPairing.Equiv.reflection {ι : 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) (i : ι) :
                                      P.Aut

                                      The automorphism of a root pairing given by a reflection.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem RootPairing.Equiv.reflection_weightEquiv {ι : 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) (i : ι) :
                                        @[simp]
                                        theorem RootPairing.Equiv.reflection_coweightEquiv {ι : 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) (i : ι) :
                                        @[simp]
                                        theorem RootPairing.Equiv.reflection_indexEquiv {ι : 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) (i : ι) :
                                        (↑(RootPairing.Equiv.reflection P i)).indexEquiv = P.reflection_perm i
                                        @[simp]
                                        theorem RootPairing.Equiv.reflection_inv {ι : 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) (i : ι) :
                                        instance RootPairing.Equiv.instMulActionAut {ι : 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) :
                                        MulAction P.Aut M
                                        Equations
                                        instance RootPairing.Equiv.instMulActionAut_1 {ι : 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) :
                                        MulAction P.Aut ι
                                        Equations