Base change of the pinned Dynkin-type Lie algebra

The pinned Lie algebra TauCeti.DynkinType.lieAlgebra is Geck's explicit matrix construction over ℚ. This file extends the underlying pinned root system to an arbitrary characteristic-zero domain K equipped with a rational algebra structure and identifies the resulting Geck Lie algebra with K ⊗[ℚ] TauCeti.DynkinType.lieAlgebra t ht.

The comparison is explicit. Mathlib's matrix scalar-extension equivalence sends every numbered matrix hᵢ, eᵢ, and fᵢ over ℚ to the matrix constructed from the scalar-extended root system over K; because both Lie algebras are generated by those matrices, it restricts to the required Lie equivalence. This makes Mathlib's algebraically-closed-field results about Geck's construction available to descent arguments for the pinned rational carrier.

That descent is the gap the pinned carrier still has. Mathlib proves Geck's Lie algebra semisimple only over an algebraically closed field, while the SimplyConnectedRootDatum/LieAlgebra/Basic.lean module records that ℚ is not one. It therefore leaves semisimplicity of TauCeti.DynkinType.lieAlgebra unclaimed; TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/KostantForm.lean inherits the same gap. Taking K to be an algebraic closure of ℚ turns those results into statements about K ⊗[ℚ] TauCeti.DynkinType.lieAlgebra t ht, from which LieModule.traceForm_baseChange carries the nondegenerate Killing form back to ℚ. The Chevalley ℤ-form is a lattice in that Lie algebra, while the Kostant ℤ-form is an integral form in its universal enveloping algebra. Thus this comparison is a prerequisite of the construction rather than a parallel to it: positive characteristic enters only afterwards, when the resulting integral data is base changed along ℤ → k.

Main definitions

• TauCeti.DynkinType.rootSystemBaseChange: the pinned rational root system extended to K.
• TauCeti.DynkinType.baseChangeBase: its Bourbaki-numbered base.
• TauCeti.DynkinType.lieAlgebraBaseChange: Geck's Lie algebra over K for that base.
• TauCeti.DynkinType.lieAlgebraBaseChangeEquiv: the Lie equivalence from the scalar extension of the pinned rational Lie algebra.

References

The matrix construction is M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247. This is a prerequisite for the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

theorem TauCeti.DynkinType.instCharZero (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : CharZero K

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.rootSystemBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : RootPairing (Fin t.numRoots) K (Fin t.rank → K) (Fin t.rank → K)

The pinned rational root system of a Dynkin type, extended to a characteristic-zero domain.

Equations

• t.rootSystemBaseChange ht K = TauCeti.rootPairingBaseChange K (t.rationalRootSystem ht) ⋯

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.baseChangeBase (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : (t.rootSystemBaseChange ht K).Base

The pinned Bourbaki-numbered base after extending the rational root system to K.

Equations

• t.baseChangeBase ht K = TauCeti.rootPairingBaseChangeBase K (t.rationalRootSystem ht) ⋯ (t.rationalBase ht)

noncomputable def TauCeti.DynkinType.supportBaseChangeEquiv (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : ↥(t.baseChangeBase ht K).support ≃ ↥(t.rationalBase ht).support

The support of the scalar-extended base is canonically the support of the rational base.

Equations

• t.supportBaseChangeEquiv ht K = TauCeti.supportEquivRootPairingBaseChangeBase K (t.rationalRootSystem ht) ⋯ (t.rationalBase ht)

@[simp]

theorem TauCeti.DynkinType.coe_supportBaseChangeEquiv (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (i : ↥(t.baseChangeBase ht K).support) : ↑((t.supportBaseChangeEquiv ht K) i) = ↑i

@[simp]

theorem TauCeti.DynkinType.coe_supportBaseChangeEquiv_symm (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (i : ↥(t.rationalBase ht).support) : ↑((t.supportBaseChangeEquiv ht K).symm i) = ↑i

instance TauCeti.DynkinType.instIsCrystallographicRootSystemBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : (t.rootSystemBaseChange ht K).IsCrystallographic

instance TauCeti.DynkinType.instIsRootSystemRootSystemBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : (t.rootSystemBaseChange ht K).IsRootSystem

instance TauCeti.DynkinType.instIsReducedRootSystemBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : (t.rootSystemBaseChange ht K).IsReduced

theorem TauCeti.DynkinType.hasCartanType_baseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : HasCartanType (t.rootSystemBaseChange ht K) (t.baseChangeBase ht K) t

The scalar-extended pinned base realizes the same Dynkin type and Bourbaki numbering.

noncomputable def TauCeti.DynkinType.geckIndexBaseChangeEquiv (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : ↥(t.baseChangeBase ht K).support ⊕ Fin t.numRoots ≃ t.GeckIndex ht

The index equivalence identifying the matrix coordinates before and after scalar extension. The root indices are unchanged, and the two base supports have the same underlying indices.

Equations

• t.geckIndexBaseChangeEquiv ht K = (t.supportBaseChangeEquiv ht K).sumCongr (Equiv.refl (Fin t.numRoots))

noncomputable def TauCeti.DynkinType.lieAlgebraBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : LieSubalgebra K (Matrix (↥(t.baseChangeBase ht K).support ⊕ Fin t.numRoots) (↥(t.baseChangeBase ht K).support ⊕ Fin t.numRoots) K)

Geck's explicit matrix Lie algebra for the scalar-extended pinned root system.

Equations

• t.lieAlgebraBaseChange ht K = RootPairing.GeckConstruction.lieAlgebra (t.baseChangeBase ht K)

@[simp]

theorem TauCeti.DynkinType.lieAlgebraBaseChange_def (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : t.lieAlgebraBaseChange ht K = RootPairing.GeckConstruction.lieAlgebra (t.baseChangeBase ht K)

The Geck generators under base change

@[simp]

theorem TauCeti.DynkinType.h_baseChangeBase (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (i : ↥(t.rationalBase ht).support) : (Matrix.reindexAlgEquiv K K (t.geckIndexBaseChangeEquiv ht K)) (RootPairing.GeckConstruction.h ((t.supportBaseChangeEquiv ht K).symm i)) = (RootPairing.GeckConstruction.h i).map ⇑(algebraMap ℚ K)

The Cartan generators of Geck's construction commute with scalar extension.

@[simp]

theorem TauCeti.DynkinType.e_baseChangeBase (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (i : ↥(t.rationalBase ht).support) : (Matrix.reindexAlgEquiv K K (t.geckIndexBaseChangeEquiv ht K)) (RootPairing.GeckConstruction.e ((t.supportBaseChangeEquiv ht K).symm i)) = (RootPairing.GeckConstruction.e i).map ⇑(algebraMap ℚ K)

The raising generators of Geck's construction commute with scalar extension.

@[simp]

theorem TauCeti.DynkinType.f_baseChangeBase (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (i : ↥(t.rationalBase ht).support) : (Matrix.reindexAlgEquiv K K (t.geckIndexBaseChangeEquiv ht K)) (RootPairing.GeckConstruction.f ((t.supportBaseChangeEquiv ht K).symm i)) = (RootPairing.GeckConstruction.f i).map ⇑(algebraMap ℚ K)

The lowering generators of Geck's construction commute with scalar extension.

Restriction to the generated Lie algebras

noncomputable def TauCeti.DynkinType.ambientLieAlgebraBaseChangeEquiv (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : TensorProduct ℚ K (Matrix (t.GeckIndex ht) (t.GeckIndex ht) ℚ) ≃ₗ⁅K⁆ Matrix (↥(t.baseChangeBase ht K).support ⊕ Fin t.numRoots) (↥(t.baseChangeBase ht K).support ⊕ Fin t.numRoots) K

Scalar extension of the ambient rational matrix Lie algebra, followed by the canonical reindexing to the scalar-extended base support.

Equations

• t.ambientLieAlgebraBaseChangeEquiv ht K = (TauCeti.matrixBaseChangeLieEquiv (t.GeckIndex ht) ℚ K).trans (Matrix.reindexAlgEquiv K K (t.geckIndexBaseChangeEquiv ht K).symm).toLieEquiv

@[simp]

theorem TauCeti.DynkinType.ambientLieAlgebraBaseChangeEquiv_tmul (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (a : K) (M : Matrix (t.GeckIndex ht) (t.GeckIndex ht) ℚ) : (t.ambientLieAlgebraBaseChangeEquiv ht K) (a ⊗ₜ[ℚ] M) = a • (Matrix.reindexAlgEquiv K K (t.geckIndexBaseChangeEquiv ht K).symm) (M.map ⇑(algebraMap ℚ K))

noncomputable def TauCeti.DynkinType.lieAlgebraBaseChangeEquiv (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : TensorProduct ℚ K ↥(t.lieAlgebra ht) ≃ₗ⁅K⁆ ↥(t.lieAlgebraBaseChange ht K)

The pinned Dynkin-type Lie algebra commutes with extension of scalars. For every characteristic-zero rational algebra domain K, scalar extension of the rational pinned carrier is canonically Lie equivalent to Geck's matrix construction on the scalar-extended pinned root system.

Equations

• t.lieAlgebraBaseChangeEquiv ht K = LieEquiv.ofBijective (TauCeti.DynkinType.lieAlgebraBaseChangeLieHom✝ t ht K) ⋯

@[simp]

theorem TauCeti.DynkinType.coe_lieAlgebraBaseChangeEquiv_apply (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (x : TensorProduct ℚ K ↥(t.lieAlgebra ht)) : ↑((t.lieAlgebraBaseChangeEquiv ht K) x) = (t.ambientLieAlgebraBaseChangeEquiv ht K) ((LinearMap.baseChange K ↑(t.lieAlgebra ht).incl) x)

@[simp]

theorem TauCeti.DynkinType.lieAlgebraBaseChangeEquiv_tmul_h (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (a : K) (i : ↥(t.rationalBase ht).support) : (t.lieAlgebraBaseChangeEquiv ht K) (a ⊗ₜ[ℚ] ⟨RootPairing.GeckConstruction.h i, ⋯⟩) = a • ⟨RootPairing.GeckConstruction.h ((t.supportBaseChangeEquiv ht K).symm i), ⋯⟩

The base-change equivalence sends a pure tensor of a Cartan generator to the corresponding generator for the scalar-extended root system.

@[simp]

theorem TauCeti.DynkinType.lieAlgebraBaseChangeEquiv_tmul_e (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (a : K) (i : ↥(t.rationalBase ht).support) : (t.lieAlgebraBaseChangeEquiv ht K) (a ⊗ₜ[ℚ] ⟨RootPairing.GeckConstruction.e i, ⋯⟩) = a • ⟨RootPairing.GeckConstruction.e ((t.supportBaseChangeEquiv ht K).symm i), ⋯⟩

The base-change equivalence sends a pure tensor of a raising generator to the corresponding generator for the scalar-extended root system.

@[simp]

theorem TauCeti.DynkinType.lieAlgebraBaseChangeEquiv_tmul_f (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] (a : K) (i : ↥(t.rationalBase ht).support) : (t.lieAlgebraBaseChangeEquiv ht K) (a ⊗ₜ[ℚ] ⟨RootPairing.GeckConstruction.f i, ⋯⟩) = a • ⟨RootPairing.GeckConstruction.f ((t.supportBaseChangeEquiv ht K).symm i), ⋯⟩

The base-change equivalence sends a pure tensor of a lowering generator to the corresponding generator for the scalar-extended root system.

theorem TauCeti.DynkinType.instCharZero_1 (K : Type u_1) [Field K] [Algebra ℚ K] : CharZero K

instance TauCeti.DynkinType.instIsIrreducibleRootSystemBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [Field K] [Algebra ℚ K] : (t.rootSystemBaseChange ht K).IsIrreducible