Documentation

TauCeti.LinearAlgebra.RootSystem.GeckConstruction.DividedPower

Integral divided powers in Geck's representation #

For a crystallographic reduced root pairing, Geck's construction gives numbered raising and lowering matrices RootPairing.GeckConstruction.e and RootPairing.GeckConstruction.f over \mathbb{Q}. This file proves that every divided power of either matrix has integer entries.

On a root vector, the n-th power of a raising matrix has coefficient (p + 1).ascFactorial n, where p is the distance to the bottom of its root string. Dividing by n! leaves the binomial coefficient (p + n).choose n. The exceptional three-dimensional string through the simple root is handled separately. The lowering result is transported through Geck's involution RootPairing.GeckConstruction.ω.

The coefficient-tracking root-string induction refines the proof pattern of Mathlib's private nilpotence helper RootPairing.GeckConstruction.isNilpotent_e_aux in Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple. The matrices and their relations come from Geck's construction in Geck.

Main declarations #

source
theorem RootPairing.GeckConstruction.dividedPower_e_apply_inl_inr_neg {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] {P : RootPairing ι ℚ M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (s : ↥b.support) (n : ℕ) :
have _i := P.indexNeg; TauCeti.Associative.dividedPower n (e s) (Sum.inl s) (Sum.inr (-↑s)) = if n = 1 then 1 else 0

The distinguished upper-right coordinate of a divided power of a Geck raising generator. It is 1 in degree one and vanishes in every other degree.

source
@[simp]
theorem RootPairing.GeckConstruction.dividedPower_f_apply_inl_inr {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] {P : RootPairing ι ℚ M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (s : ↥b.support) (n : ℕ) :
TauCeti.Associative.dividedPower n (f s) (Sum.inl s) (Sum.inr ↑s) = if n = 1 then 1 else 0

The distinguished upper-right coordinate of a divided power of a Geck lowering generator. It is 1 in degree one and vanishes in every other degree.

source
theorem RootPairing.GeckConstruction.exists_intCast_dividedPower_e_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] {P : RootPairing ι ℚ M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (s : ↥b.support) (n : ℕ) (i j : ↥b.support ⊕ ι) :
∃ (z : ℤ), ↑z = TauCeti.Associative.dividedPower n (e s) i j

Every entry of a divided power of a numbered raising operator in Geck's representation is an integer.

source
theorem RootPairing.GeckConstruction.exists_intCast_dividedPower_f_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] {P : RootPairing ι ℚ M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (s : ↥b.support) (n : ℕ) (i j : ↥b.support ⊕ ι) :
∃ (z : ℤ), ↑z = TauCeti.Associative.dividedPower n (f s) i j

Every entry of a divided power of a numbered lowering operator in Geck's representation is an integer.