Irreducible root pairings

This file contains basic definitions and results about irreducible root systems.

Main definitions / results:

• RootPairing.isSimpleModule_weylGroupRootRep_iff: a criterion for the representation of the Weyl group on root space to be irreducible.
• RootPairing.IsIrreducible: a typeclass encoding the fact that a root pairing is irreducible.
• RootPairing.IsIrreducible.mk': an alternative constructor for irreducibility when the coefficients are a field.

theorem RootPairing.isSimpleModule_weylGroupRootRep_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) [Nontrivial M] : IsSimpleModule (MonoidAlgebra R ↥P.weylGroup) P.weylGroupRootRep.asModule ↔ ∀ (q : Submodule R M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤

class RootPairing.IsIrreducible {ι : 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) : Prop

A root pairing is irreducible if it is non-trivial and contains no proper invariant submodules.

• nontrivial : Nontrivial M
• nontrivial' : Nontrivial N
• eq_top_of_invtSubmodule_reflection (q : Submodule R M) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
• eq_top_of_invtSubmodule_coreflection (q : Submodule R N) : (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤

theorem RootPairing.isIrreducible_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) : P.IsIrreducible ↔ Nontrivial M ∧ Nontrivial N ∧ (∀ (q : Submodule R M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤) ∧ ∀ (q : Submodule R N), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤

instance RootPairing.instIsIrreducibleFlip {ι : 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.IsIrreducible] : P.flip.IsIrreducible

theorem RootPairing.isSimpleModule_weylGroupRootRep {ι : 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.IsIrreducible] : IsSimpleModule (MonoidAlgebra R ↥P.weylGroup) P.weylGroupRootRep.asModule

def RootPairing.toRootSystem {ι : 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) [Nonempty ι] [NeZero 2] [P.IsIrreducible] : RootSystem ι R M N

A nonempty irreducible root pairing is a root system.

Equations

• P.toRootSystem = { toRootPairing := P, span_root_eq_top := ⋯, span_coroot_eq_top := ⋯ }

theorem RootPairing.invtSubmodule_reflection_of_invtSubmodule_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 : ι) (q : Submodule R N) (hq : q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) : Submodule.map P.toDualLeft.symm q.dualAnnihilator ∈ Module.End.invtSubmodule ↑(P.reflection i)

theorem RootPairing.IsIrreducible.mk' {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] {K : Type u_5} [Field K] [Module K M] [Module K N] [Nontrivial M] (P : RootPairing ι K M N) (h : ∀ (q : Submodule K M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤) : P.IsIrreducible

When the coefficients are a field, the coroot conditions for irreducibility follow from those for the roots.

theorem RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule {ι : 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) [NeZero 2] [NoZeroSMulDivisors R M] (q : Submodule R M) (hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) : ∃ (Φ : Set ι), (∀ i ∈ Φ, ¬Disjoint q (Submodule.span R {P.root i})) ∧ ∀ i ∉ Φ, q ≤ LinearMap.ker (P.coroot' i)

theorem RootPairing.span_orbit_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) [NeZero 2] [P.IsIrreducible] (i : ι) : Submodule.span R (MulAction.orbit (↥P.weylGroup) (P.root i)) = ⊤

theorem RootPairing.exists_form_eq_form_and_form_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) [NeZero 2] [P.IsIrreducible] (B : P.InvariantForm) (i j : ι) : ∃ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) ∧ (B.form (P.root i)) (P.root k) ≠ 0

theorem RootPairing.span_root_image_eq_top_of_forall_orthogonal {ι : 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) [NeZero 2] [P.IsIrreducible] (s : Set ι) (hne : s.Nonempty) (h : ∀ (j : ι), P.root j ∉ Submodule.span R (⇑P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i) : Submodule.span R (⇑P.root '' s) = ⊤

theorem RootSystem.eq_top_of_mem_invtSubmodule_of_forall_eq_univ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] {K : Type u_5} [Field K] [NeZero 2] [Module K M] [Module K N] (P : RootSystem ι K M N) (q : Submodule K M) (h₀ : q ≠ ⊥) (h₁ : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) (h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ LinearMap.ker (P.coroot' i)) → Φ = Set.univ) : q = ⊤