Geck's construction of a Lie algebra associated to a root system

This file contains an implementation of Geck's construction of a semisimple Lie algebra from a reduced crystallographic root system. It follows Geck quite closely.

Main definitions:

• RootPairing.GeckConstruction.lieAlgebra: the Geck construction of the Lie algebra associated to a root system with distinguished base.
• RootPairing.GeckConstruction.cartanSubalgebra: a distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.
• RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra: the distinguished subalgebra is contained in the Geck construction.

Alternative approaches

There are at least three ways to construct a Lie algebra from a root system:

1. As a quotient of a free Lie algebra, using the Serre relations
2. Directly defining the Lie bracket on $H ⊕ K^∣Φ|$
3. The Geck construction

We comment on these as follows:

1. This construction takes just a matrix as input. It yields a semisimple Lie algebra iff the matrix is a Cartan matrix but it is quite a lot of work to prove this. On the other hand, it also allows construction of Kac-Moody Lie algebras. It has been implemented as Matrix.ToLieAlgebra but as of May 2025, almost nothing has been proved about it in Mathlib.
2. This construction takes a root system with base as input, together with sufficient additional data to determine a collection of extraspecial pairs of roots. The additional data for the extraspecial pairs is required to pin down certain signs when defining the Lie bracket. (These signs can be interpreted as a set-theoretic splitting of Tits's extension of the Weyl group by an elementary 2-group of order $2^l$ where $l$ is the rank.)
3. This construction takes a root system with base as input and is implemented here.

There seems to be no known construction of a Lie algebra from a root system without first choosing a base: https://mathoverflow.net/questions/495434/

def RootPairing.GeckConstruction.h {ι : 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.IsCrystallographic] {b : P.Base} (i : ↥b.support) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

theorem RootPairing.GeckConstruction.h_def {ι : 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.IsCrystallographic] {b : P.Base} [DecidableEq ι] (i : ↥b.support) : h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) => ↑(P.pairingIn ℤ x ↑i))

theorem RootPairing.GeckConstruction.h_eq_diagonal {ι : 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.IsCrystallographic] {b : P.Base} [DecidableEq ι] (i : ↥b.support) : h i = Matrix.diagonal (Sum.elim 0 fun (x : ι) => ↑(P.pairingIn ℤ x ↑i))

theorem RootPairing.GeckConstruction.span_range_h_le_range_diagonal {ι : 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.IsCrystallographic] {b : P.Base} [DecidableEq ι] : Submodule.span R (Set.range h) ≤ (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range

@[simp]

theorem RootPairing.GeckConstruction.diagonal_elim_mem_span_h_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.IsCrystallographic] {b : P.Base} [DecidableEq ι] {d : ι → R} : Matrix.diagonal (Sum.elim 0 d) ∈ Submodule.span R (Set.range h) ↔ d ∈ Submodule.span R (Set.range fun (i : ↥b.support) (j : ι) => ↑(P.pairingIn ℤ j ↑i))

theorem RootPairing.GeckConstruction.apply_sum_inl_eq_zero_of_mem_span_h {ι : 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.IsCrystallographic] {b : P.Base} (i : ↥b.support) (j : ↥b.support ⊕ ι) {x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R} (hx : x ∈ Submodule.span R (Set.range h)) : x j (Sum.inl i) = 0

theorem RootPairing.GeckConstruction.lie_h_h {ι : 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.IsCrystallographic] {b : P.Base} [Fintype ι] (i j : ↥b.support) : ⁅h i, h j⁆ = 0

def RootPairing.GeckConstruction.e {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] (i : ↥b.support) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

def RootPairing.GeckConstruction.f {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] (i : ↥b.support) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

def RootPairing.GeckConstruction.ω {ι : 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} (b : P.Base) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R

An involutive matrix which can transfer results between RootPairing.GeckConstruction.e and RootPairing.GeckConstruction.f.

def RootPairing.GeckConstruction.lieAlgebra {ι : 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.IsCrystallographic] (b : P.Base) [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Geck's construction of the Lie algebra associated to a root system with distinguished base.

Note that it is convenient to include range h in the Lie span, to make it elementary that it contains RootPairing.GeckConstruction.cartanSubalgebra, and not depend on RootPairing.GeckConstruction.lie_e_f_same.

def RootPairing.GeckConstruction.cartanSubalgebra {ι : 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.IsCrystallographic] (b : P.Base) [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

A distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.

See also RootPairing.GeckConstruction.cartanSubalgebra'.

def RootPairing.GeckConstruction.cartanSubalgebra' {ι : 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.IsCrystallographic] (b : P.Base) [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] : LieSubalgebra R ↥(lieAlgebra b)

A distinguished Cartan subalgebra of the Geck construction.

theorem RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan {ι : 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.IsCrystallographic] (b : P.Base) [Fintype ι] [DecidableEq ι] : cartanSubalgebra b = LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Set.range h)

@[simp]

theorem RootPairing.GeckConstruction.h_mem_cartanSubalgebra {ι : 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.IsCrystallographic] {b : P.Base} [Fintype ι] [DecidableEq ι] (i : ↥b.support) : h i ∈ cartanSubalgebra b

@[simp]

theorem RootPairing.GeckConstruction.h_mem_cartanSubalgebra' {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] (i : ↥b.support) (hi : h i ∈ lieAlgebra b) : ⟨h i, hi⟩ ∈ cartanSubalgebra' b

theorem RootPairing.GeckConstruction.h_mem_lieAlgebra {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] (i : ↥b.support) : h i ∈ lieAlgebra b

theorem RootPairing.GeckConstruction.e_mem_lieAlgebra {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] (i : ↥b.support) : e i ∈ lieAlgebra b

theorem RootPairing.GeckConstruction.f_mem_lieAlgebra {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] (i : ↥b.support) : f i ∈ lieAlgebra b

def RootPairing.GeckConstruction.h' {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] (i : ↥b.support) : ↥(cartanSubalgebra' b)

The element h i, as a term of the Cartan subalgebra cartanSubalgebra' b.

@[simp]

theorem RootPairing.GeckConstruction.span_range_h'_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} [P.IsCrystallographic] (b : P.Base) [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] [DecidableEq ι] : Submodule.span R (Set.range h') = ⊤

@[simp]

theorem RootPairing.GeckConstruction.ω_mul_ω {ι : 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} {b : P.Base} [DecidableEq ι] [Fintype ι] : ω b * ω b = 1

theorem RootPairing.GeckConstruction.ω_mul_h {ι : 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.IsCrystallographic] {b : P.Base} [CharZero R] [Fintype ι] (i : ↥b.support) : ω b * h i = -h i * ω b

theorem RootPairing.GeckConstruction.ω_mul_e {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] (i : ↥b.support) : ω b * e i = f i * ω b

theorem RootPairing.GeckConstruction.ω_mul_f {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] (i : ↥b.support) : ω b * f i = e i * ω b

theorem RootPairing.GeckConstruction.lie_e_f_mul_ω {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [Fintype ι] (i j : ↥b.support) : ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆

@[reducible, inline]

abbrev RootPairing.GeckConstruction.u {ι : 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} {b : P.Base} [DecidableEq ι] (i : ↥b.support) : ↥b.support ⊕ ι → R

Geck's name for the "left" basis elements of b.support ⊕ ι.

@[reducible, inline]

abbrev RootPairing.GeckConstruction.v {ι : 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} (b : P.Base) [DecidableEq ι] (i : ι) : ↥b.support ⊕ ι → R

Geck's name for the "right" basis elements of b.support ⊕ ι.

theorem RootPairing.GeckConstruction.apply_inr_eq_zero_of_mem_span_range_u {ι : 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} (b : P.Base) [DecidableEq ι] (j : ι) {x : ↥b.support ⊕ ι → R} (hx : x ∈ Submodule.span R (Set.range u)) : x (Sum.inr j) = 0

theorem RootPairing.GeckConstruction.lie_e_lie_f_apply {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] (i j : ↥b.support) : ⁅e i, ⁅f i, u j⁆⁆ = |b.cartanMatrix i j| • u i

instance RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra {ι : 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.IsCrystallographic] {b : P.Base} [DecidableEq ι] [Fintype ι] : IsLieAbelian ↥(cartanSubalgebra b)

instance RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra' {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] : IsLieAbelian ↥(cartanSubalgebra' b)

instance RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] : LieModule.IsTriangularizable R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R)

theorem RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] : cartanSubalgebra b ≤ lieAlgebra b

theorem RootPairing.GeckConstruction.e_lie_u {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] (i j : ↥b.support) : ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b ↑i

theorem RootPairing.GeckConstruction.e_lie_v_ne {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] {i j : ι} {k : ↥b.support} (h : P.root j = P.root ↑k + P.root i) : ⁅e k, v b i⁆ = (↑(chainBotCoeff (↑k) i) + 1) • v b j

theorem RootPairing.GeckConstruction.f_lie_v_same {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] (i : ↥b.support) : ⁅f i, v b ↑i⁆ = u i

theorem RootPairing.GeckConstruction.f_lie_v_ne {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] {i j : ι} {k : ↥b.support} (h : P.root i = P.root j + P.root ↑k) : ⁅f k, v b i⁆ = (↑(chainTopCoeff (↑k) i) + 1) • v b j

def RootPairing.GeckConstruction.ωConj {ι : 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} (b : P.Base) [DecidableEq ι] [Fintype ι] : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R ≃ₗ⁅R⁆ Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R

The conjugation x ↦ ωxω as an equivalence of Lie algebras.

@[simp]

theorem RootPairing.GeckConstruction.ωConj_toFun {ι : 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} (b : P.Base) [DecidableEq ι] [Fintype ι] (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) : (ωConj b) x = ω b * x * ω b

@[simp]

theorem RootPairing.GeckConstruction.ωConj_invFun {ι : 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} (b : P.Base) [DecidableEq ι] [Fintype ι] (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) : (ωConj b).invFun x = ω b * x * ω b

theorem RootPairing.GeckConstruction.ωConj_mem_of_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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] {x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R} (hx : x ∈ lieAlgebra b) : (ωConj b) x ∈ lieAlgebra b

def RootPairing.GeckConstruction.ωConjLieSubmodule {ι : 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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R) → LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)

The equivalence x ↦ ωxω as an operation on Lie submodules of the Geck construction.

@[simp]

theorem RootPairing.GeckConstruction.mem_ωConjLieSubmodule_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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] (N✝ : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)) {x : ↥b.support ⊕ ι → R} : x ∈ ωConjLieSubmodule N✝ ↔ (ω b).mulVec x ∈ N✝

@[simp]

theorem RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_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.IsCrystallographic] {b : P.Base} [Finite ι] [IsDomain R] [CharZero R] [DecidableEq ι] [Fintype ι] (N✝ : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)) : ωConjLieSubmodule N✝ = ⊤ ↔ N✝ = ⊤