Documentation

Mathlib.LinearAlgebra.RootSystem.Basic

Root data and root systems #

This file contains basic results for root systems and root data.

Main definitions / results: #

TODO #

@[simp]
theorem RootPairing.equiv_of_mapsTo_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 : PerfectPairing R M N) (root : ι M) (coroot : ι N) (i : ι) (h : ∀ (i : ι), Set.MapsTo ((Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range root) (Set.range root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (j : ι) :
(RootPairing.equiv_of_mapsTo p root coroot i h hp).symm j = .choose
@[simp]
theorem RootPairing.equiv_of_mapsTo_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 : PerfectPairing R M N) (root : ι M) (coroot : ι N) (i : ι) (h : ∀ (i : ι), Set.MapsTo ((Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range root) (Set.range root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (j : ι) :
(RootPairing.equiv_of_mapsTo p root coroot i h hp) j = .choose
def RootPairing.equiv_of_mapsTo {ι : Type u_1} {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 : PerfectPairing R M N) (root : ι M) (coroot : ι N) (i : ι) (h : ∀ (i : ι), Set.MapsTo ((Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range root) (Set.range root)) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) :
ι ι

The bijection on the indexing set induced by reflection.

Equations
  • RootPairing.equiv_of_mapsTo p root coroot i h hp = { toFun := fun (j : ι) => .choose, invFun := fun (j : ι) => .choose, left_inv := , right_inv := }
Instances For
    theorem RootPairing.injOn_dualMap_subtype_span_root_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] (P : RootPairing ι R M N) [NoZeroSMulDivisors M] :
    Set.InjOn (((Submodule.span R (Set.range P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (Set.range P.coroot)

    Even though the roots may not span, coroots are distinguished by their pairing with the roots. The proof depends crucially on the fact that there are finitely-many roots.

    Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI.

    theorem RootPairing.ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] {P₁ : RootPairing ι R M N} {P₂ : RootPairing ι R M N} (he : P₁.toLin = P₂.toLin) (hr : P₁.root = P₂.root) (hc : Set.range P₁.coroot = Set.range P₂.coroot) :
    P₁ = P₂

    In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.

    Formally, the point is that the hypothesis hc depends only on the range of the coroot mappings.

    def RootPairing.mk' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] (p : PerfectPairing R M N) (root : ι M) (coroot : ι N) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (hr : ∀ (i : ι), Set.MapsTo ((Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range root) (Set.range root)) (hc : ∀ (i : ι), Set.MapsTo ((Module.preReflection (coroot i) (p.toLin (root i)))) (Set.range coroot) (Set.range coroot)) :
    RootPairing ι R M N

    In characteristic zero if there is no torsion, to check that two finite familes of of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem RootSystem.ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] {P₁ : RootSystem ι R M N} {P₂ : RootSystem ι R M N} (he : P₁.toLin = P₂.toLin) (hr : P₁.root = P₂.root) :
      P₁ = P₂

      In characteristic zero if there is no torsion, a finite root system is determined entirely by its roots.

      def RootSystem.mk' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] (p : PerfectPairing R M N) (root : ι M) (coroot : ι N) (hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) (hs : ∀ (i : ι), Set.MapsTo ((Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range root) (Set.range root)) (hsp : Submodule.span R (Set.range root) = ) :
      RootSystem ι R M N

      In characteristic zero if there is no torsion, to check that a finite family of roots form a root system, we do not need to check that the coroots are stable under reflections since this follows from the corresponding property for the roots.

      Equations
      Instances For