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.

def RootPairing.invtRootSubmodule {ι : 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) : Sublattice (Submodule R M)

The sublattice of invariant submodules of the root space.

Equations

• P.invtRootSubmodule = ⨅ (i : ι), Module.End.invtSubmodule ↑(P.reflection i)

theorem RootPairing.mem_invtRootSubmodule_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) {q : Submodule R M} : q ∈ P.invtRootSubmodule ↔ ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)

@[simp]

theorem RootPairing.invtRootSubmodule.top_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) : ⊤ ∈ P.invtRootSubmodule

@[simp]

theorem RootPairing.invtRootSubmodule.bot_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) : ⊥ ∈ P.invtRootSubmodule

@[instance_reducible]

instance RootPairing.instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule {ι : 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) : BoundedOrder ↥P.invtRootSubmodule

Equations

• P.instBoundedOrderSubtypeSubmoduleMemSublatticeInvtRootSubmodule = { top := ⟨⊤, ⋯⟩, le_top := ⋯, bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

instance RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule {ι : 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] : Nontrivial ↥P.invtRootSubmodule

@[simp]

theorem RootPairing.coe_bot {ι : 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) : ↑⊥ = ⊥

@[simp]

theorem RootPairing.coe_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) : ↑⊤ = ⊤

theorem RootPairing.eq_zero_iff_forall_coroot'_eq_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) [P.IsRootSystem] {x : M} : x = 0 ↔ ∀ (i : ι), (P.coroot' i) x = 0

theorem RootPairing.invtRootSubmodule.le_ker_coroot' {ι : 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 : RootPairing ι K M N} (q : ↥P.invtRootSubmodule) {k : ι} (hk : P.root k ∉ ↑q) : ↑q ≤ LinearMap.ker (P.coroot' k)

theorem RootPairing.invtRootSubmodule.eq_bot_iff {ι : 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 : RootPairing ι K M N} [P.IsRootSystem] (q : ↥P.invtRootSubmodule) : q = ⊥ ↔ ∀ (i : ι), P.root i ∉ ↑q

theorem RootPairing.invtRootSubmodule.eq_top_iff {ι : 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] {P : RootPairing ι K M N} [P.IsRootSystem] (q : ↥P.invtRootSubmodule) : q = ⊤ ↔ Set.range ⇑P.root ⊆ ↑↑q

theorem RootPairing.invtRootSubmodule.eq_span_root {ι : 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 : RootPairing ι K M N} [P.IsRootSystem] (q : ↥P.invtRootSubmodule) : ↑q = Submodule.span K (⇑P.root '' {i : ι | P.root i ∈ ↑q})

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

theorem RootPairing.not_isIrreducible_of_subsingleton {ι : 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) [Subsingleton M] : ¬P.IsIrreducible

theorem RootPairing.Equiv.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} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) [P.IsIrreducible] : P₂.IsIrreducible

instance RootPairing.instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible {ι : 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] : P.IsRootSystem

A nonempty irreducible root pairing is a root system.

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.toPerfPair.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.isIrreducible_iff_invtRootSubmodule {ι : 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) : P.IsIrreducible ↔ IsSimpleOrder ↥P.invtRootSubmodule

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] [IsDomain R] [Module.IsTorsionFree R M] (q : Submodule R M) (hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) : ∃ (Φ : Set ι), (∀ i ∈ Φ, ¬Disjoint q (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 RootPairing.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 : RootPairing ι K M N) [P.IsRootSystem] (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 = ⊤