Root data and root systems

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

Main definitions / results:

• RootPairing.ext: In characteristic zero over an integral domain, the correspondence between roots and coroots is unique.
• RootSystem.ext: In characteristic zero over an integral domain, a root system is determined entirely by its roots.
• RootPairing.mk': In characteristic zero over an integral domain, to check that two finite families of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.
• RootSystem.mk': In characteristic zero over an integral domain, 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.

noncomputable 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 : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p (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 := ⋯ }

@[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 : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p (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 : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M) (coroot : ι ↪ N) (i : ι) (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2) (j : ι) : (RootPairing.equiv_of_mapsTo p root coroot i h hp) j = ⋯.choose

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 ι] [IsAddTorsionFree M] : Set.InjOn (⇑((Submodule.span R (Set.range ⇑P.root)).subtype.dualMap ∘ₗ P.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] [IsDomain R] {P₁ P₂ : RootPairing ι R M N} (he : P₁.toLinearMap = P₂.toLinearMap) (hr : P₁.root = P₂.root) (hc : Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot) : P₁ = P₂

In characteristic zero over an integral domain, 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.ext_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] [Finite ι] [CharZero R] [IsDomain R] {P₁ P₂ : RootPairing ι R M N} : P₁ = P₂ ↔ P₁.toLinearMap = P₂.toLinearMap ∧ P₁.root = P₂.root ∧ Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot

noncomputable 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] [IsDomain R] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N) (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2) (hr : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hc : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (coroot i) (p (root i)))) (Set.range ⇑coroot) (Set.range ⇑coroot)) : RootPairing ι R M N

In characteristic zero over an integral domain, to check that two finite families 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.

theorem RootPairing.IsRootSystem.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] [IsDomain R] {P₁ P₂ : RootPairing ι R M N} [P₁.IsRootSystem] [P₂.IsRootSystem] (he : P₁.toLinearMap = P₂.toLinearMap) (hr : P₁.root = P₂.root) : P₁ = P₂

In characteristic zero over an integral domain, a finite root system is determined entirely by its roots.

noncomputable def RootPairing.mk'' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Finite ι] {k : Type u_5} [Field k] [CharZero k] [Module k M] [Module k N] (p : M →ₗ[k] N →ₗ[k] k) [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N) (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2) (hs : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) (hsp : Submodule.span k (Set.range ⇑root) = ⊤) : RootPairing ι k M N

Over a field of characteristic zero, to check that a finite family of roots form a crystallographic 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. Likewise, we do not need to check that the coroots span.

Equations

• RootPairing.mk'' p root coroot hp hs hsp = RootPairing.mk' p root coroot hp hs ⋯

theorem RootPairing.isRootSystem_mk'' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Finite ι] {k : Type u_5} [Field k] [CharZero k] [Module k M] [Module k N] {p : M →ₗ[k] N →ₗ[k] k} [p.IsPerfPair] {root : ι ↪ M} {coroot : ι ↪ N} {hp : ∀ (i : ι), (p (root i)) (coroot i) = 2} {hs : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)} {hsp : Submodule.span k (Set.range ⇑root) = ⊤} (h_int : ∀ (i j : ι), ∃ (z : ℤ), ↑z = (p (root i)) (coroot j)) : (mk'' p root coroot hp hs hsp).IsRootSystem