Symmetries of Geck's construction

Geck's construction attaches to a root pairing P with base b an explicit Lie subalgebra of the matrices indexed by b.support ⊕ ι, generated as a Lie subalgebra by the numbered matrices RootPairing.GeckConstruction.h i, RootPairing.GeckConstruction.e i and RootPairing.GeckConstruction.f i. Every entry of those matrices is a Cartan integer, a root-string coefficient, or the truth value of an additive relation between roots: no sign is chosen, unlike the construction of a Lie algebra directly on H ⊕ K^Φ, whose structure constants need a choice of extraspecial pairs.

This file is about the consequence of that. An equivalence g of root pairings whose index bijection restricts to an equivalence τ of their bases identifies the corresponding index types, and reindexing a matrix along that equivalence carries each of the three numbered families to the other, moving the number along:

h i ↦ h (τ i),   e i ↦ e (τ i),   f i ↦ f (τ i).

So reindexing restricts to an equivalence of the two Geck Lie algebras. On the defining modules it is a permutation of coordinates, TauCeti.geckModuleEquiv, intended as input to a later Chevalley--Demazure descent; unlike an automorphism moving root vectors by signs, it needs no further renormalisation first.

Nothing here uses RootPairing.Base.equivOfCartanMatrixEq or any other rigidity statement. The equivalence g is data supplied by the caller, and the hypothesis hτ says only that its index bijection restricts to τ. In the automorphism case, a caller holding only a permutation τ of the nodes that preserves the Cartan matrix gets such a g from Mathlib's RootPairing.Base.equivOfCartanMatrixEq, and hτ is then TauCeti.equivOfCartanMatrixEq_indexEquiv_apply read in the other direction.

Main definitions

• TauCeti.geckIndexEquiv: the sum of an equivalence of base supports and the index equivalence of root pairings.
• TauCeti.geckModuleEquiv: the resulting coordinate permutation of the defining module.
• TauCeti.geckLieEquivOfEquiv: the resulting equivalence of Geck's Lie algebras.

Main results

• TauCeti.reindex_geckIndexEquiv_h, TauCeti.reindex_geckIndexEquiv_e and TauCeti.reindex_geckIndexEquiv_f: conjugation carries the numbered matrix at i to the one at τ i.
• TauCeti.map_lieAlgebra_geckIndexEquiv: reindexing carries one Geck Lie algebra onto the other.
• TauCeti.geckLieEquivOfEquiv_h, TauCeti.geckLieEquivOfEquiv_e and TauCeti.geckLieEquivOfEquiv_f: the Lie equivalence carries each numbered generator to its counterpart.
• TauCeti.geckModuleEquiv_mulVec_h, TauCeti.geckModuleEquiv_mulVec_e and TauCeti.geckModuleEquiv_mulVec_f: the coordinate permutation intertwines the action of the numbered matrix at i with the action of the one at τ i.

Roadmap

This advances Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md, whose "Pinnings" bullet asks for the graph automorphism attached to a pinning as named data. The planned consumer is milestone L1, "ordinary and graph-twisted Steinberg maps", of TauCetiRoadmap/CFSGStatement/README.md, through the planned TauCeti.GraphTwistedIndex.graphAut. This file supplies the coordinate permutation and its matrix intertwining relation; a caller must still transport that relation to Geck's representation and prove preservation of its integral lattice before applying TauCeti.UniversalEnvelopingAlgebra.kostantElementaryNumberedSymmetryAut.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.

def TauCeti.geckIndexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) : ↥b.support ⊕ ι ≃ ↥b₂.support ⊕ ι₂

The equivalence of the index types of Geck's matrices formed from an equivalence τ of base supports and the index equivalence of a root-pairing equivalence g.

The b.support summand indexes the Cartan coordinates and the ι summand indexes the root coordinates, so the permutation is τ on the first and g.indexEquiv on the second. The numbered matrix lemmas separately assume that these agree on the base.

Equations

• TauCeti.geckIndexEquiv g τ = τ.sumCongr (↑g).indexEquiv

@[simp]

theorem TauCeti.geckIndexEquiv_apply_inl {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (i : ↥b.support) : (geckIndexEquiv g τ) (Sum.inl i) = Sum.inl (τ i)

@[simp]

theorem TauCeti.geckIndexEquiv_apply_inr {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (i : ι) : (geckIndexEquiv g τ) (Sum.inr i) = Sum.inr ((↑g).indexEquiv i)

@[simp]

theorem TauCeti.geckIndexEquiv_symm_apply_inl {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (i : ↥b₂.support) : (geckIndexEquiv g τ).symm (Sum.inl i) = Sum.inl (τ.symm i)

@[simp]

theorem TauCeti.geckIndexEquiv_symm_apply_inr {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (i : ι₂) : (geckIndexEquiv g τ).symm (Sum.inr i) = Sum.inr ((↑g).indexEquiv.symm i)

The coordinate permutation of the defining module

def TauCeti.geckModuleEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) : (↥b.support ⊕ ι → R) ≃ₗ[R] ↥b₂.support ⊕ ι₂ → R

The coordinate equivalence of the defining modules induced by geckIndexEquiv. The numbered matrix lemmas separately assume that the two component equivalences agree on the base.

Equations

• TauCeti.geckModuleEquiv g τ = LinearEquiv.funCongrLeft R R (TauCeti.geckIndexEquiv g τ).symm

@[simp]

theorem TauCeti.geckModuleEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (v : ↥b.support ⊕ ι → R) (x : ↥b₂.support ⊕ ι₂) : (geckModuleEquiv g τ) v x = v ((geckIndexEquiv g τ).symm x)

@[simp]

theorem TauCeti.geckModuleEquiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) (v : ↥b₂.support ⊕ ι₂ → R) (x : ↥b.support ⊕ ι) : (geckModuleEquiv g τ).symm v x = v ((geckIndexEquiv g τ) x)

@[simp]

theorem TauCeti.geckModuleEquiv_single {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [DecidableEq ι] [DecidableEq ι₂] (x : ↥b.support ⊕ ι) (r : R) : (geckModuleEquiv g τ) (Pi.single x r) = Pi.single ((geckIndexEquiv g τ) x) r

The coordinate permutation carries the coordinate vector at x to the one at geckIndexEquiv g τ x. Taking r = 1 this says that it carries Geck's u i and v i to u (τ i) and v (g.indexEquiv i).

@[simp]

theorem TauCeti.geckModuleEquiv_mulVec {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] (A : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (v : ↥b.support ⊕ ι → R) : (geckModuleEquiv g τ) (A.mulVec v) = ((Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)) A).mulVec ((geckModuleEquiv g τ) v)

The coordinate permutation intertwines the action of a matrix with the action of its conjugate.

Conjugating the numbered matrices

@[simp]

theorem TauCeti.reindex_geckIndexEquiv_h {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] (i : ↥b.support) : (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)) (RootPairing.GeckConstruction.h i) = RootPairing.GeckConstruction.h (τ i)

Conjugation by the index permutation carries the Cartan generator h i to the one numbered by τ i.

@[simp]

theorem TauCeti.reindex_geckIndexEquiv_e {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (i : ↥b.support) : (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)) (RootPairing.GeckConstruction.e i) = RootPairing.GeckConstruction.e (τ i)

Conjugation by the index permutation carries the raising matrix numbered by i to the one numbered by τ i.

@[simp]

theorem TauCeti.reindex_geckIndexEquiv_f {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (i : ↥b.support) : (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)) (RootPairing.GeckConstruction.f i) = RootPairing.GeckConstruction.f (τ i)

Conjugation by the index permutation carries the lowering matrix numbered by i to the one numbered by τ i.

The equivalence of Geck's Lie algebras

theorem TauCeti.map_lieAlgebra_geckIndexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] : LieSubalgebra.map (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)).toLieEquiv.toLieHom (RootPairing.GeckConstruction.lieAlgebra b) = RootPairing.GeckConstruction.lieAlgebra b₂

Geck's Lie algebra is invariant under base-preserving equivalence of root pairings. Reindexing carries the Lie subalgebra spanned by the source numbered matrices onto the target one, because it carries each of the three numbered families onto its target counterpart.

noncomputable def TauCeti.geckLieEquivOfEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] : ↥(RootPairing.GeckConstruction.lieAlgebra b) ≃ₗ⁅R⁆ ↥(RootPairing.GeckConstruction.lieAlgebra b₂)

The equivalence of Geck's Lie algebras induced by a base-preserving equivalence of root pairings: the restriction of matrix reindexing.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.geckLieEquivOfEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (x : ↥(RootPairing.GeckConstruction.lieAlgebra b)) : ↑((geckLieEquivOfEquiv g τ hτ) x) = (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)) ↑x

@[simp]

theorem TauCeti.geckLieEquivOfEquiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (x : ↥(RootPairing.GeckConstruction.lieAlgebra b₂)) : ↑((geckLieEquivOfEquiv g τ hτ).symm x) = (Matrix.reindexAlgEquiv R R (geckIndexEquiv g τ)).symm ↑x

@[simp]

theorem TauCeti.geckLieEquivOfEquiv_h {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (i : ↥b.support) : (geckLieEquivOfEquiv g τ hτ) ⟨RootPairing.GeckConstruction.h i, ⋯⟩ = ⟨RootPairing.GeckConstruction.h (τ i), ⋯⟩

The Geck Lie equivalence carries the Cartan generator numbered by i to the one numbered by τ i.

@[simp]

theorem TauCeti.geckLieEquivOfEquiv_e {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (i : ↥b.support) : (geckLieEquivOfEquiv g τ hτ) ⟨RootPairing.GeckConstruction.e i, ⋯⟩ = ⟨RootPairing.GeckConstruction.e (τ i), ⋯⟩

The Geck Lie equivalence carries the raising generator numbered by i to the one numbered by τ i.

@[simp]

theorem TauCeti.geckLieEquivOfEquiv_f {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [DecidableEq ι] [Fintype ι] [DecidableEq ι₂] [Fintype ι₂] [IsDomain R] (i : ↥b.support) : (geckLieEquivOfEquiv g τ hτ) ⟨RootPairing.GeckConstruction.f i, ⋯⟩ = ⟨RootPairing.GeckConstruction.f (τ i), ⋯⟩

The Geck Lie equivalence carries the lowering generator numbered by i to the one numbered by τ i.

@[simp]

theorem TauCeti.geckModuleEquiv_mulVec_h {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [Fintype ι] [Fintype ι₂] (i : ↥b.support) (v : ↥b.support ⊕ ι → R) : (geckModuleEquiv g τ) ((RootPairing.GeckConstruction.h i).mulVec v) = (RootPairing.GeckConstruction.h (τ i)).mulVec ((geckModuleEquiv g τ) v)

The coordinate permutation carries the action of the Cartan generator h i to the action of the one numbered by τ i.

@[simp]

theorem TauCeti.geckModuleEquiv_mulVec_e {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [Fintype ι] [Fintype ι₂] [IsDomain R] (i : ↥b.support) (v : ↥b.support ⊕ ι → R) : (geckModuleEquiv g τ) ((RootPairing.GeckConstruction.e i).mulVec v) = (RootPairing.GeckConstruction.e (τ i)).mulVec ((geckModuleEquiv g τ) v)

The coordinate permutation carries the action of the raising matrix numbered by i to the action of the one numbered by τ i. This is the intertwining relation that a numbered symmetry of the Kostant data is built from.

@[simp]

theorem TauCeti.geckModuleEquiv_mulVec_f {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} {b : P.Base} {b₂ : P₂.Base} (g : P.Equiv P₂) (τ : ↥b.support ≃ ↥b₂.support) [CharZero R] [P.IsCrystallographic] [P₂.IsCrystallographic] (hτ : ∀ (i : ↥b.support), ↑(τ i) = (↑g).indexEquiv ↑i) [Fintype ι] [Fintype ι₂] [IsDomain R] (i : ↥b.support) (v : ↥b.support ⊕ ι → R) : (geckModuleEquiv g τ) ((RootPairing.GeckConstruction.f i).mulVec v) = (RootPairing.GeckConstruction.f (τ i)).mulVec ((geckModuleEquiv g τ) v)

The coordinate permutation carries the action of the lowering matrix numbered by i to the action of the one numbered by τ i.