Irreducibility from a connected Dynkin diagram

This file proves the converse to the standard implication from irreducibility of a root pairing to connectedness of its Dynkin diagram. Over a field of characteristic zero, a crystallographic root system whose base has connected diagram is irreducible. It then checks that the standard Cartan matrix of every valid DynkinType has connected diagram and packages the result in the form used by root systems identified through TauCeti.HasCartanType.

The argument follows the usual proof in Humphreys, Introduction to Lie Algebras and Representation Theory, §10. A nonzero reflection-invariant subspace contains a root, hence a simple root. Once it contains one simple root, connectedness and reflection invariance propagate membership along every edge of the Dynkin diagram, so the simple roots span the whole space inside the subspace.

Main results

• RootPairing.isIrreducible_of_connected_diagramGraph_cartanMatrix: a connected base diagram makes a root system irreducible.
• RootPairing.eq_bot_of_forall_root_not_mem: a submodule invariant under the simple reflections and containing no simple root is trivial.
• TauCeti.DynkinType.connected_diagramGraph_cartanMatrix: every valid standard Dynkin diagram is connected.
• TauCeti.HasCartanType.isIrreducible: a root system of valid Cartan type is irreducible.

theorem TauCeti.DynkinType.connected_diagramGraph_cartanMatrix {t : DynkinType} (ht : t.Valid) : (diagramGraph t.cartanMatrix).Connected

The diagram of the standard Cartan matrix of a valid Dynkin type is connected. Validity confines each family to its canonical rank range, which is nonempty and is what the proof uses.

theorem RootPairing.eq_bot_of_forall_root_not_mem {K : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Field K] [CharZero K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsRootSystem] {b : P.Base} {q : Submodule K M} (hinv : ∀ (i : ↥b.support), q ∈ Module.End.invtSubmodule ↑(P.reflection ↑i)) (h : ∀ (i : ↥b.support), P.root ↑i ∉ q) : q = ⊥

A submodule invariant under the simple reflections and containing no simple root is trivial. If q is invariant under the reflection at each element of the base's support and misses the root there, then q = ⊥.

Invariance is asked at the support only, not under every reflection of P.

theorem RootPairing.isIrreducible_of_connected_diagramGraph_cartanMatrix {K : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Field K] [CharZero K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsCrystallographic] [P.IsRootSystem] (b : P.Base) (hconn : (TauCeti.diagramGraph b.cartanMatrix).Connected) : P.IsIrreducible

A crystallographic root system with a connected Dynkin diagram is irreducible.

Characteristic zero ensures that a nonzero integral Cartan entry stays nonzero in the field when membership propagates across an edge. It also supplies the standard 2 ≠ 0 hypothesis in Mathlib's invariant-submodule criterion for a reflection.

theorem TauCeti.HasCartanType.isIrreducible {K : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Field K] [CharZero K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsCrystallographic] [P.IsRootSystem] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) (ht : t.Valid) : P.IsIrreducible

A root system whose base has a valid standard Cartan type is irreducible.