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 #

theorem RootPairing.Hom.ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} :
∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Hom Q}, x.weightMap = y.weightMapx.coweightMap = y.coweightMapx.indexEquiv = y.indexEquivx = y
theorem RootPairing.Hom.ext_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} :
∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂} {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Hom Q}, x = y x.weightMap = y.weightMap x.coweightMap = y.coweightMap x.indexEquiv = y.indexEquiv
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.weight_coweight_transpose {ι : Type u_1} {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₂} (self : P.Hom Q) :
    self.weightMap.dualMap ∘ₗ Q.toDualRight = P.toDualRight ∘ₗ self.coweightMap
    theorem RootPairing.Hom.root_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₂} (self : P.Hom Q) :
    self.weightMap P.root = Q.root self.indexEquiv
    theorem RootPairing.Hom.coroot_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₂} (self : P.Hom Q) :
    self.coweightMap Q.coroot = P.coroot self.indexEquiv.symm
    @[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
    @[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_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
    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.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)
      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.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)
        @[simp]
        theorem RootPairing.Hom.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.Hom.reflection P i).indexEquiv = P.reflection_perm i
        @[simp]
        theorem RootPairing.Hom.reflection_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) (i : ι) (a : N) :
        (RootPairing.Hom.reflection P i).coweightMap a = a - (P.toPerfectPairing (P.root i)) a P.coroot i
        @[simp]
        theorem RootPairing.Hom.reflection_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) (i : ι) (a : M) :
        (RootPairing.Hom.reflection P i).weightMap a = a - (P.flip.toPerfectPairing (P.flip.root i)) a P.flip.coroot i
        def RootPairing.Hom.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.Hom P

        The endomorphism of a root pairing given by a reflection.

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