The cotangent-dual model of the tangent Lie algebra

For a commutative bialgebra H over R, the tangent space at the identity has two models: counit-valued derivations of H, and the linear dual of the augmentation cotangent space ker(ε) / ker(ε)². The existing linear equivalence between them transports the convolution commutator to the cotangent-dual model. This file records the resulting Lie algebra structure and packages the comparison as a Lie equivalence.

Main declarations

• Derivation.cotangentDualLieEquiv: the cotangent dual is canonically the tangent Lie algebra of counit-valued derivations.
• Derivation.tangentScalarExtensionLieEquiv: scalar extension of the cotangent-dual Lie algebra agrees with coefficient-valued tangent derivations.

References

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

This identifies the fixed module used by the adjoint representation with Lie(G) in Layer 2 of the ReductiveGroups roadmap.

@[instance_reducible]

noncomputable instance Derivation.instLieRingCotangentDual {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] : LieRing (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))

The Lie ring structure on the dual augmentation cotangent space, transported from counit-valued derivations through cotangentLinearEquiv.

Equations

• Derivation.instLieRingCotangentDual = Derivation.cotangentLinearEquiv.toAddEquiv.lieRing

@[instance_reducible]

noncomputable instance Derivation.instLieAlgebraCotangentDual {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] : LieAlgebra R (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))

The Lie algebra structure on the dual augmentation cotangent space, transported from counit-valued derivations through cotangentLinearEquiv.

Equations

• Derivation.instLieAlgebraCotangentDual = Derivation.cotangentLinearEquiv.lieAlgebra

noncomputable def Derivation.cotangentDualLieEquiv {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H) ≃ₗ⁅R⁆ Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)

The canonical Lie equivalence from the dual augmentation cotangent space to the tangent Lie algebra of counit-valued derivations.

Equations

• Derivation.cotangentDualLieEquiv = LinearEquiv.lieEquiv R Derivation.cotangentLinearEquiv

@[simp]

theorem Derivation.cotangentDualLieEquiv_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] (f : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) : cotangentDualLieEquiv f = cotangentLinearEquiv f

The cotangent-dual Lie equivalence has the existing cotangent linear equivalence as its underlying map.

@[simp]

theorem Derivation.cotangentDualLieEquiv_symm_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) : cotangentDualLieEquiv.symm d = cotangentLinearEquiv.symm d

The inverse cotangent-dual Lie equivalence has the inverse cotangent linear equivalence as its underlying map.

@[simp]

theorem Derivation.cotangentLinearEquiv_bracket {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] (f g : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) : cotangentLinearEquiv ⁅f, g⁆ = ⁅cotangentLinearEquiv f, cotangentLinearEquiv g⁆

The bracket on the cotangent dual is characterized by transport to the convolution bracket on counit-valued derivations.

@[simp]

theorem Derivation.tangentScalarExtensionEquiv_bracket {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] {B : Type u_1} [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (x y : TensorProduct R B (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : tangentScalarExtensionEquiv ⁅x, y⁆ = ⁅tangentScalarExtensionEquiv x, tangentScalarExtensionEquiv y⁆

The established scalar-extension equivalence preserves the Lie bracket.

noncomputable def Derivation.tangentScalarExtensionLieEquiv {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] {B : Type u_1} [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] : TensorProduct R B (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) ≃ₗ⁅B⁆ Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H B)

Scalar extension of the cotangent-dual Lie algebra is canonically Lie-equivalent to the coefficient-valued tangent Lie algebra.

Equations

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

@[simp]

theorem Derivation.tangentScalarExtensionLieEquiv_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] {B : Type u_1} [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (x : TensorProduct R B (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : tangentScalarExtensionLieEquiv x = tangentScalarExtensionEquiv x

The scalar-extension Lie equivalence has the existing scalar-extension linear equivalence as its underlying map.

@[simp]

theorem Derivation.tangentScalarExtensionLieEquiv_symm_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] {B : Type u_1} [CommRing B] [Algebra R B] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H B)) : tangentScalarExtensionLieEquiv.symm d = tangentScalarExtensionEquiv.symm d

The inverse scalar-extension Lie equivalence has the inverse scalar-extension linear equivalence as its underlying map.