The Lie algebra of the tangent space at the identity

Counit-valued derivations of a bialgebra A — the tangent vectors at the identity point (TauCeti.Bialgebra.CounitAlgebra) — are closed under the commutator of the convolution product: for derivations d₁ d₂ the linear map d₁ ⋆ d₂ - d₂ ⋆ d₁ is again a derivation. This equips the tangent space with LieRing and LieAlgebra R structures: the Lie algebra of the corresponding affine monoid scheme — of the affine group scheme, when A is a Hopf algebra (ReductiveGroups roadmap, Layer 2, Lie(G)).

The closure proof is composition-level, with no Sweedler-style computation. Multiplication of the bialgebra is a coalgebra morphism (Bialgebra.mulCoalgHom), so precomposing with it is multiplicative into the convolution algebra on A ⊗[R] A (LinearMap.convMul_comp_coalgHom_distrib). There the Leibniz rule for d reads d ∘ mul = 1 ⊠ d + d ⊠ 1 for the exterior convolution product ⊠ of two factors on the two tensor legs, and ⊠ is itself multiplicative (TensorProduct.map_convMul_map pushed through Algebra.TensorProduct.lmul'). Expanding, the cross terms d₁ ⊠ d₂ + d₂ ⊠ d₁ of the two composite products coincide and cancel in the commutator. Commutativity of B matters to closure itself, not only to this route: over a noncommutative coefficient ring the commutator of counit-valued derivations need not satisfy the Leibniz rule, the obstruction being the value commutators ⁅d₁ x, d₂ y⁆.

Main declarations

• Derivation.instBracketCounitAlgebra, Derivation.instLieRingCounitAlgebra, and Derivation.instLieAlgebraCounitAlgebra: the Bracket, LieRing, and LieAlgebra R instances on Derivation R A (Bialgebra.CounitAlgebra R A B);
• Derivation.coe_bracket, Derivation.bracket_apply: the bracket is the convolution commutator.

No antipode enters: everything is stated over a bialgebra. The ring (rather than semiring) hypotheses are those of the additive group of derivations in Mathlib (Derivation R A M is an AddCommGroup for CommRing R, CommRing A), which the commutator needs. This bracket is the convolution commutator; it cannot collide with Mathlib's composition-commutator LieRing (Derivation R A A), even at B = A: the two carrier types differ in their Module A instance argument — the coefficient action here is through the counit (a • m = algebraMap R B (counit a) * m, Bialgebra.CounitAlgebra.algebraMap_apply), not multiplication — so neither elaboration nor instance search can identify the types, and no diamond exists. The CounitAlgebra suffix also distinguishes their declaration names from Mathlib's Derivation.instBracket, Derivation.instLieRing, and Derivation.instLieAlgebra.

@[instance_reducible]

noncomputable instance Derivation.instBracketCounitAlgebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommRing B] [Algebra R B] : Bracket (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))

The Lie bracket of tangent vectors at the identity: the commutator of the convolution product.

Equations

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

@[simp]

theorem Derivation.coe_bracket {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommRing B] [Algebra R B] (d₁ d₂ : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : ↑⁅d₁, d₂⁆ = (WithConv.toConv ↑d₁ * WithConv.toConv ↑d₂).ofConv - (WithConv.toConv ↑d₂ * WithConv.toConv ↑d₁).ofConv

The bracket of counit-valued derivations is the convolution commutator of their underlying linear maps.

@[simp]

theorem Derivation.bracket_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommRing B] [Algebra R B] (d₁ d₂ : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (a : A) : ⁅d₁, d₂⁆ a = (LinearMap.mul' R (TauCeti.Bialgebra.CounitAlgebra R A B)) ((TensorProduct.map ↑d₁ ↑d₂) (CoalgebraStruct.comul a)) - (LinearMap.mul' R (TauCeti.Bialgebra.CounitAlgebra R A B)) ((TensorProduct.map ↑d₂ ↑d₁) (CoalgebraStruct.comul a))

The bracket of tangent vectors, valuewise: the difference of the two convolution products, in convolution normal form.

@[instance_reducible]

noncomputable instance Derivation.instLieRingCounitAlgebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] : LieRing (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))

The tangent space at the identity is a Lie ring under the convolution commutator.

Equations

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

@[instance_reducible]

noncomputable instance Derivation.instLieAlgebraCounitAlgebra {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] : LieAlgebra R (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))

The tangent space at the identity is a Lie algebra over the base ring.

Equations

• Derivation.instLieAlgebraCounitAlgebra = { toModule := Derivation.instModule, lie_smul := ⋯ }

@[instance_reducible]

noncomputable instance Derivation.instLieAlgebraCoefficients {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] : LieAlgebra B (Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B))

The tangent space at the identity is a Lie algebra over the coefficient ring.

Equations

• Derivation.instLieAlgebraCoefficients = { toModule := TauCeti.instModuleDerivationCounitAlgebra, lie_smul := ⋯ }