Root data and root systems #
This file contains basic results for root systems and root data.
Main definitions / results: #
RootPairing.ext: In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.RootSystem.ext: In characteristic zero if there is no torsion, a root system is determined entirely by its roots.RootSystem.mk': In characteristic zero if there is no torsion, to check that a 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.
Todo #
- Derived properties of pairs, e.g., (ultra)parallel linearly independent pairs generate infinite dihedral groups.
- Properties of Weyl group (faithful action on roots, finiteness for finite
ι) - Conditions for existence of Weyl-invariant form (e.g., finiteness).
theorem
RootPairing.root_ne
{ι : 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 : ι)
(j : ι)
(h : i ≠ j)
:
P.root i ≠ P.root j
theorem
RootPairing.ne_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)
(i : ι)
[CharZero R]
:
P.root i ≠ 0
theorem
RootPairing.ne_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)
(i : ι)
[CharZero R]
:
P.coroot i ≠ 0
@[simp]
theorem
RootPairing.root_coroot_eq_pairing
{ι : 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 : ι)
(j : ι)
:
(P.toLin (P.root i)) (P.coroot j) = P.pairing i j
theorem
RootPairing.coroot_root_eq_pairing
{ι : 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 : ι)
(j : ι)
:
(P.toLin.flip (P.coroot i)) (P.root j) = P.pairing j i
@[simp]
theorem
RootPairing.pairing_same
{ι : 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.pairing i i = 2
theorem
RootPairing.coroot_root_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)
(i : ι)
:
(P.toLin.flip (P.coroot i)) (P.root i) = 2
@[simp]
theorem
RootPairing.flip_flip
{ι : 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.flip.flip = P
theorem
RootPairing.reflection_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 : ι)
(x : M)
:
theorem
RootPairing.reflection_apply_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)
(i : ι)
(j : ι)
:
@[simp]
theorem
RootPairing.reflection_apply_self
{ι : 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.reflection_same
{ι : 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 : ι)
(x : M)
:
(P.reflection i) ((P.reflection i) x) = x
theorem
RootPairing.reflection_invOn_self
{ι : 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 : ι)
:
theorem
RootPairing.bijOn_reflection_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)
(i : ι)
:
theorem
RootPairing.coreflection_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 : ι)
(f : N)
:
@[simp]
theorem
RootPairing.coreflection_apply_self
{ι : 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 : ι)
:
theorem
RootPairing.coreflection_eq_flip_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 : ι)
(f : N)
:
(P.coreflection i) f = (P.flip.reflection i) f
@[simp]
theorem
RootPairing.coreflection_self
{ι : 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 : ι)
(x : N)
:
(P.coreflection i) ((P.coreflection i) x) = x
theorem
RootPairing.coreflection_invOn_self
{ι : 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 : ι)
:
theorem
RootPairing.bijOn_coreflection_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]
(P : RootPairing ι R M N)
(i : ι)
:
@[simp]
theorem
RootPairing.reflection_image_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)
(i : ι)
:
@[simp]
theorem
RootPairing.coreflection_image_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)
(i : ι)
:
theorem
RootPairing.reflection_dualMap_eq_coreflection
{ι : 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.reflection i).dualMap ∘ₗ P.toLin.flip = P.toLin.flip ∘ₗ ↑(P.coreflection i)
theorem
RootPairing.reflection_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)
(i : ι)
(j : ι)
(x : M)
:
theorem
RootPairing.isCrystallographic_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)
:
theorem
RootPairing.isReduced_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)
:
theorem
RootPairing.coxeterWeight_swap
{ι : 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 : ι)
(j : ι)
:
P.coxeterWeight i j = P.coxeterWeight j i
theorem
RootPairing.IsOrthogonal.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]
(P : RootPairing ι R M N)
(i : ι)
(j : ι)
:
P.IsOrthogonal i j ↔ P.IsOrthogonal j i
theorem
RootPairing.IsOrthogonal_comm
{ι : 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 : ι)
(j : ι)
(h : P.IsOrthogonal i j)
:
Commute (P.reflection i) (P.reflection j)
theorem
RootPairing.eq_of_pairing_pairing_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)
[Finite ι]
[NoZeroSMulDivisors ℤ M]
(i : ι)
(j : ι)
(hij : P.pairing i j = 2)
(hji : P.pairing j i = 2)
:
i = j
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]
(P : RootPairing ι R M N)
[Finite ι]
[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.
theorem
RootPairing.coroot_eq_coreflection_of_root_eq_of_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]
[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) = ⊤)
{i : ι}
{j : ι}
{k : ι}
(hk : root k = (Module.preReflection (root i) (p.toLin.flip (coroot i))) (root j))
:
coroot k = (Module.preReflection (coroot i) (p.toLin (root i))) (coroot j)
This lemma exists to support the definition RootSystem.mk' and usually should not be used
directly. The lemma RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top or even
RootSystem.coroot_eq_coreflection_of_root_eq will usually be more convenient.
theorem
RootPairing.coroot_eq_coreflection_of_root_eq_of_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)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
(hsp : Submodule.span R (Set.range ⇑P.root) = ⊤)
{i : ι}
{j : ι}
{k : ι}
(hk : P.root k = (P.reflection i) (P.root j))
:
P.coroot k = (P.coreflection i) (P.coroot j)
In characteristic zero if there is no torsion and the roots span, if the ith reflection of the
jth root is the kth root, then the corresponding relationship holds for coroots. See also
RootSystem.coroot_eq_coreflection_of_root_eq.
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 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
RootSystem.coroot_eq_coreflection_of_root_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]
[Finite ι]
(P : RootSystem ι R M N)
[CharZero R]
[NoZeroSMulDivisors R M]
{i : ι}
{j : ι}
{k : ι}
(hk : P.root k = (P.reflection i) (P.root j))
:
P.coroot k = (P.coreflection i) (P.coroot j)
In characteristic zero if there is no torsion, if the ith reflection of the jth root is the
kth root, then the corresponding relationship holds for coroots.