Bases for root pairings / systems

This file contains a theory of bases for root pairings / systems.

Implementation details

For reduced root pairings RootSystem.Base is equivalent to the usual definition appearing in the informal literature (e.g., it follows from [Ser87](Ch. V, §8, Proposition 7) that RootSystem.Base is equivalent to both [Ser87](Ch. V, §8, Definition 5) and [Bou02](Ch. VI, §1.5) for reduced pairings). However for non-reduced root pairings, it is more restrictive because it includes axioms on coroots as well as on roots. For example by RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem it is clear that the 1-dimensional root system {-2, -1, 0, 1, 2} ⊆ ℝ has no base in the sense of RootSystem.Base.

It is also worth remembering that it is only for reduced root systems that one has the simply transitive action of the Weyl group on the set of bases, and that the Weyl group of a non-reduced root system is the same as that of the reduced root system obtained by passing to the indivisible roots.

For infinite root systems, RootSystem.Base is usually not the right notion: linear independence is too strong.

Main definitions / results:

• RootSystem.Base: a base of a root pairing.

TODO

• Develop a theory of base / separation / positive roots for infinite systems which specialises to the concept here for finite systems.

structure RootPairing.Base {ι : 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 u_1

A base of a root pairing.

For reduced root pairings this definition is equivalent to the usual definition appearing in the informal literature but not for non-reduced root pairings it is more restrictive. See the module doc string for further remarks.

• support : Set ι

  The set of roots / coroots belonging to the base.

• linInd_root : LinearIndependent R fun (i : ↑self.support) => P.root ↑i
• linInd_coroot : LinearIndependent R fun (i : ↑self.support) => P.coroot ↑i
• root_mem_or_neg_mem (i : ι) : P.root i ∈ AddSubmonoid.closure (⇑P.root '' self.support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' self.support)
• coroot_mem_or_neg_mem (i : ι) : P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' self.support) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' self.support)

def RootPairing.Base.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} (b : P.Base) : P.flip.Base

Interchanging roots and coroots, one still has a base of a root pairing.

Equations

• b.flip = { support := b.support, linInd_root := ⋯, linInd_coroot := ⋯, root_mem_or_neg_mem := ⋯, coroot_mem_or_neg_mem := ⋯ }

@[simp]

theorem RootPairing.Base.flip_support {ι : 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} (b : P.Base) : b.flip.support = b.support

theorem RootPairing.Base.root_mem_span_int {ι : 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} (b : P.Base) (i : ι) : P.root i ∈ Submodule.span ℤ (⇑P.root '' b.support)

theorem RootPairing.Base.coroot_mem_span_int {ι : 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} (b : P.Base) (i : ι) : P.coroot i ∈ Submodule.span ℤ (⇑P.coroot '' b.support)

@[simp]

theorem RootPairing.Base.span_int_root_support {ι : 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} (b : P.Base) : Submodule.span ℤ (⇑P.root '' b.support) = Submodule.span ℤ (Set.range ⇑P.root)

@[simp]

theorem RootPairing.Base.span_int_coroot_support {ι : 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} (b : P.Base) : Submodule.span ℤ (⇑P.coroot '' b.support) = Submodule.span ℤ (Set.range ⇑P.coroot)

@[simp]

theorem RootPairing.Base.span_root_support {ι : 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} (b : P.Base) : Submodule.span R (⇑P.root '' b.support) = P.rootSpan

@[simp]

theorem RootPairing.Base.span_coroot_support {ι : 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} (b : P.Base) : Submodule.span R (⇑P.coroot '' b.support) = P.corootSpan

theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux {ι : 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} (b : P.Base) [Finite ι] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ Set.range ⇑P.root) : ∃ (z : ℤ), ↑z * t = 1

theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem {ι : 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} (b : P.Base) [Finite ι] [CharZero R] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ Set.range ⇑P.root) : t = 1 ∨ t = -1

def RootPairing.Base.toWeightBasis {ι : 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 : RootSystem ι R M N} (b : P.Base) : Basis (↑b.support) R M

A base of a root system yields a basis of the root space.

Equations

• b.toWeightBasis = Basis.mk ⋯ ⋯

@[simp]

theorem RootPairing.Base.toWeightBasis_repr_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 : RootSystem ι R M N} (b : P.Base) (a✝ : M) : b.toWeightBasis.repr a✝ = ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range fun (i : ↑b.support) => P.root ↑i)) LinearMap.id ⋯) a✝)

@[simp]

theorem RootPairing.Base.toWeightBasis_repr_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 : RootSystem ι R M N} (b : P.Base) (a : ↑b.support →₀ R) : b.toWeightBasis.repr.symm a = (Finsupp.linearCombination R fun (i : ↑b.support) => P.root ↑i) a

def RootPairing.Base.toCoweightBasis {ι : 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 : RootSystem ι R M N} (b : P.Base) : Basis (↑b.support) R N

A base of a root system yields a basis of the coroot space.

Equations

• b.toCoweightBasis = b.flip.toWeightBasis

theorem RootPairing.Base.exists_root_eq_sum_nat_or_neg {ι : 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 : RootSystem ι R M N} (b : P.Base) [Fintype ι] (i : ι) : ∃ (f : ι → ℕ), P.root i = ∑ j : ι, f j • P.root j ∨ P.root i = -∑ j : ι, f j • P.root j

theorem RootPairing.Base.exists_root_eq_sum_int {ι : 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 : RootSystem ι R M N} (b : P.Base) [Fintype ι] (i : ι) : ∃ (f : ι → ℤ), (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

theorem RootPairing.Base.exists_coroot_eq_sum_int {ι : 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 : RootSystem ι R M N} (b : P.Base) [Fintype ι] (i : ι) : ∃ (f : ι → ℤ), (0 ≤ f ∨ f ≤ 0) ∧ P.coroot i = ∑ j : ι, f j • P.coroot j