The tangent Lie algebra of a product

The tensor product of two commutative bialgebras is the coordinate algebra of the direct product of the represented affine monoid schemes. Restricting a counit-valued derivation along the two canonical inclusions gives its two tangent components. Conversely, the canonical projections, obtained by applying the counit to the other tensor factor, extend a pair of tangent vectors back to the product. These constructions are inverse and preserve the convolution Lie bracket.

Thus the tangent Lie algebra of a direct product is canonically the product of the tangent Lie algebras of its factors. The equivalence is valid for coefficient-valued tangent vectors over an arbitrary commutative coefficient algebra; it needs no antipode, finiteness, or field hypothesis.

Main declarations

• Derivation.tensorProductLieEquiv: the canonical Lie equivalence Lie(Spec (H₁ ⊗[R] H₂)) ≃ Lie(Spec H₁) × Lie(Spec H₂).
• Derivation.tensorProductLieEquiv_apply: its two components are restriction to the tensor factors.
• Derivation.tensorProductLieEquiv_symm_apply_tmul: the inverse evaluated on a pure tensor.
• Derivation.finrank_tangent_tensorProduct: for finite-dimensional tangent spaces over a field, tangent dimensions add over products.

References

• J. S. Milne, Algebraic Groups (2017), §10.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 11.

This supplies the direct-product compatibility for Lie(G) in Layer 2, "Tangent space at the identity / Lie(G)", of the ReductiveGroups roadmap. It also gives the additive tangent-dimension formula needed by the same layer's dimension tools.

noncomputable def Derivation.tensorProductLieEquiv {R : Type u} {H₁ : Type v} {H₂ : Type w} {B : Type z} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommRing B] [Algebra R B] : Derivation R (TensorProduct R H₁ H₂) (TauCeti.Bialgebra.CounitAlgebra R (TensorProduct R H₁ H₂) B) ≃ₗ⁅B⁆ Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B) × Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B)

The tangent Lie algebra of a product is canonically the product of the tangent Lie algebras of its factors.

Equations

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

@[simp]

theorem Derivation.tensorProductLieEquiv_apply {R : Type u} {H₁ : Type v} {H₂ : Type w} {B : Type z} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommRing B] [Algebra R B] (d : Derivation R (TensorProduct R H₁ H₂) (TauCeti.Bialgebra.CounitAlgebra R (TensorProduct R H₁ H₂) B)) : tensorProductLieEquiv d = ((TauCeti.derivationComp TauCeti.Bialgebra.TensorProduct.includeLeft) d, (TauCeti.derivationComp TauCeti.Bialgebra.TensorProduct.includeRight) d)

The product tangent equivalence restricts a derivation to the two tensor factors.

@[simp]

theorem Derivation.tensorProductLieEquiv_symm_apply {R : Type u} {H₁ : Type v} {H₂ : Type w} {B : Type z} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommRing B] [Algebra R B] (d : Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B) × Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B)) : tensorProductLieEquiv.symm d = (TauCeti.derivationComp TauCeti.Bialgebra.TensorProduct.projectLeft) d.1 + (TauCeti.derivationComp TauCeti.Bialgebra.TensorProduct.projectRight) d.2

The inverse product tangent equivalence extends both components along the counit projections and adds them.

theorem Derivation.tensorProductLieEquiv_symm_apply_tmul {R : Type u} {H₁ : Type v} {H₂ : Type w} {B : Type z} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommRing B] [Algebra R B] (d : Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B) × Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B)) (h₁ : H₁) (h₂ : H₂) : (TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R (TensorProduct R H₁ H₂) B) ((tensorProductLieEquiv.symm d) (h₁ ⊗ₜ[R] h₂)) = CoalgebraStruct.counit h₂ • (TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H₁ B) (d.1 h₁) + CoalgebraStruct.counit h₁ • (TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H₂ B) (d.2 h₂)

On a pure tensor, the tangent vector assembled from d is the Leibniz sum ε(h₂) • d.1 h₁ + ε(h₁) • d.2 h₂.

instance Derivation.instFiniteTensorProductCounitAlgebra {R : Type u} {H₁ : Type v} {H₂ : Type w} {B : Type z} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommRing B] [Algebra R B] [Module.Finite B (Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B))] [Module.Finite B (Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B))] : Module.Finite B (Derivation R (TensorProduct R H₁ H₂) (TauCeti.Bialgebra.CounitAlgebra R (TensorProduct R H₁ H₂) B))

Finiteness of the two factor tangent modules implies finiteness of the tensor-product tangent module.

theorem Derivation.finrank_tangent_tensorProduct {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {B : Type u_4} [CommRing R] [CommRing H₁] [CommRing H₂] [Bialgebra R H₁] [Bialgebra R H₂] [Field B] [Algebra R B] [Module.Finite B (Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B))] [Module.Finite B (Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B))] : Module.finrank B (Derivation R (TensorProduct R H₁ H₂) (TauCeti.Bialgebra.CounitAlgebra R (TensorProduct R H₁ H₂) B)) = Module.finrank B (Derivation R H₁ (TauCeti.Bialgebra.CounitAlgebra R H₁ B)) + Module.finrank B (Derivation R H₂ (TauCeti.Bialgebra.CounitAlgebra R H₂ B))

The dimension of the tangent Lie algebra of a product is the sum of the dimensions of the tangent Lie algebras of its factors.