Base change of the tangent Lie algebra

For a commutative bialgebra H over R and a commutative R-algebra K, restriction along h ↦ 1 ⊗ h identifies the tangent Lie algebra of K ⊗[R] H over K with the K-valued tangent derivations of H. The inverse sends d to a ⊗ h ↦ a * d h. This comparison requires neither flatness nor finiteness. It connects geometric base change to the coefficient-valued tangent space and its convolution bracket. For an extension of fields, finrank_lie_baseChange deduces invariance of Lie dimension when the original augmentation cotangent space is finite-dimensional, and isKilling_lie_baseChange_iff shows that the Lie algebra has nondegenerate Killing form exactly when its base change does.

References

• J. S. Milne, Algebraic Groups (2017), §10.a.

The tensor calculation for compatibility with convolution follows the point comparison in TauCeti.Algebra.AlgebraicGroup.BaseChange.Basic.

noncomputable def TauCeti.tangentBaseChangeLieEquiv {R : Type u_1} {K : Type u_2} {H : Type u_3} [CommRing R] [CommRing K] [CommRing H] [Algebra R K] [Bialgebra R H] : Derivation R H (Bialgebra.CounitAlgebra R H K) ≃ₗ⁅K⁆ Derivation K (TensorProduct R K H) (Bialgebra.CounitAlgebra K (TensorProduct R K H) K)

The Lie algebra of a base-changed affine monoid is its coefficient-valued tangent Lie algebra. The comparison preserves the convolution bracket and needs no flatness assumption.

Equations

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

@[simp]

theorem TauCeti.tangentBaseChangeLieEquiv_tmul {R : Type u_1} {K : Type u_2} {H : Type u_3} [CommRing R] [CommRing K] [CommRing H] [Algebra R K] [Bialgebra R H] (d : Derivation R H (Bialgebra.CounitAlgebra R H K)) (a : K) (h : H) : (tangentBaseChangeLieEquiv d) (a ⊗ₜ[R] h) = (Bialgebra.CounitAlgebra.algEquivSelf K (TensorProduct R K H) K).symm (a * (Bialgebra.CounitAlgebra.algEquivSelf R H K) (d h))

Base change extends a tangent vector by K-linearity.

@[simp]

theorem TauCeti.tangentBaseChangeLieEquiv_symm_apply {R : Type u_1} {K : Type u_2} {H : Type u_3} [CommRing R] [CommRing K] [CommRing H] [Algebra R K] [Bialgebra R H] (d : Derivation K (TensorProduct R K H) (Bialgebra.CounitAlgebra K (TensorProduct R K H) K)) (h : H) : (tangentBaseChangeLieEquiv.symm d) h = (Bialgebra.CounitAlgebra.algEquivSelf R H K).symm ((Bialgebra.CounitAlgebra.algEquivSelf K (TensorProduct R K H) K) (d (1 ⊗ₜ[R] h)))

The inverse Lie comparison restricts along h ↦ 1 ⊗ h.

theorem TauCeti.finrank_lie_baseChange {k : Type u_1} {K : Type u_2} {H : Type u_3} [Field k] [Field K] [Algebra k K] [CommRing H] [Bialgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] : Module.finrank K (Derivation K (TensorProduct k K H) (Bialgebra.CounitAlgebra K (TensorProduct k K H) K)) = Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k))

Extension of the ground field preserves the dimension of the Lie algebra of an affine monoid whose augmentation cotangent space is finite-dimensional. This compares the Lie algebras of the original and base-changed coordinate rings, not merely their coefficient spaces.

theorem TauCeti.isKilling_lie_baseChange_iff {k : Type u_1} {K : Type u_2} {H : Type u_3} [Field k] [Field K] [Algebra k K] [CommRing H] [Bialgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] : LieAlgebra.IsKilling K (Derivation K (TensorProduct k K H) (Bialgebra.CounitAlgebra K (TensorProduct k K H) K)) ↔ LieAlgebra.IsKilling k (Derivation k H (Bialgebra.CounitAlgebra k H k))

Extension of the ground field preserves and reflects nondegeneracy of the Killing form of the Lie algebra of an affine monoid whose augmentation cotangent space is finite-dimensional: the Lie algebra of K ⊗[k] H has nondegenerate Killing form exactly when Lie(G) does.