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)
:
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 = ⊤
Instances
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]
:
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]
:
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 := ⋯ }
Instances For
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))
:
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 = ⊤)
:
When the coefficients are a field, the coroot conditions for irreducibility follow from those for the roots.
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 : ι)
:
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 : ι)
: