Documentation

Mathlib.LinearAlgebra.RootSystem.Irreducible

Irreducible root pairings #

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

Main definitions / results: #

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) :

The sublattice of invariant submodules of the root space.

Equations
Instances For
    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} :
    @[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) :
    @[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) :
    Equations
    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] :
    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.

    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] :
      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.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.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 : ι) :
        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 jSubmodule.span R (P.root '' s)is, P.IsOrthogonal j i) :
        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 ι), Φ.NonemptyP.root '' Φ q(∀ iΦ, q LinearMap.ker (P.coroot' i))Φ = Set.univ) :
        q =