The differential is a Lie algebra morphism

Precomposition of counit-valued derivations along a bialgebra morphism (TauCeti.derivationComp) preserves the convolution commutator: the differential of a morphism of affine monoid schemes is a morphism of Lie algebras (ReductiveGroups roadmap, Layer 2, "the differential of a homomorphism"). The bracket identity uses only the coalgebra half of the morphism — it intertwines the convolution products termwise; the algebra half already entered in derivationComp, which needs d (φ (x * y)) = d (φ x * φ y) to produce a derivation at all.

Main declarations

• TauCeti.derivationComp_bracket: the differential preserves the bracket.
• TauCeti.derivationCompLieHom: the differential as a morphism of Lie algebras.
• TauCeti.derivationCompLieHom_injective_of_surjective: the differential of a surjective bialgebra morphism is injective.
• TauCeti.derivationCompLieHom_bijective_of_surjective_of_finrank_eq: a surjective bialgebra morphism between equal-dimensional tangent Lie algebras induces a bijection.

@[simp]

theorem TauCeti.derivationComp_bracket {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommSemiring A'] [Bialgebra R A'] [CommRing B] [Algebra R B] (φ : A' →ₐc[R] A) (d₁ d₂ : Derivation R A (Bialgebra.CounitAlgebra R A B)) : (derivationComp φ) ⁅d₁, d₂⁆ = ⁅(derivationComp φ) d₁, (derivationComp φ) d₂⁆

The differential preserves the convolution commutator: a bialgebra morphism intertwines comultiplications, hence convolution products of derivations termwise.

noncomputable def TauCeti.derivationCompLieHom {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing A'] [Bialgebra R A'] [CommRing B] [Algebra R B] (φ : A' →ₐc[R] A) : Derivation R A (Bialgebra.CounitAlgebra R A B) →ₗ⁅B⁆ Derivation R A' (Bialgebra.CounitAlgebra R A' B)

The differential on derivations, as a morphism of Lie algebras over the coefficient ring.

Equations

• TauCeti.derivationCompLieHom φ = { toFun := ⇑(TauCeti.derivationComp φ), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem TauCeti.derivationCompLieHom_apply {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing A'] [Bialgebra R A'] [CommRing B] [Algebra R B] (φ : A' →ₐc[R] A) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) : (derivationCompLieHom φ) d = (derivationComp φ) d

theorem TauCeti.derivationCompLieHom_injective_of_surjective {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing A'] [Bialgebra R A'] [CommRing B] [Algebra R B] (φ : A' →ₐc[R] A) (hφ : Function.Surjective ⇑φ) : Function.Injective ⇑(derivationCompLieHom φ)

The differential of a surjective bialgebra morphism is injective.

@[simp]

theorem TauCeti.derivationCompLieHom_id {R : Type u_1} {A : Type u_2} {B : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] : derivationCompLieHom (BialgHom.id R A) = LieHom.id

The bundled differential along the identity is the identity Lie morphism.

@[simp]

theorem TauCeti.derivationCompLieHom_comp {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing A'] [Bialgebra R A'] [CommRing B] [Algebra R B] {A'' : Type u_5} [CommRing A''] [Bialgebra R A''] (φ : A' →ₐc[R] A) (χ : A'' →ₐc[R] A') : derivationCompLieHom (φ.comp χ) = (derivationCompLieHom χ).comp (derivationCompLieHom φ)

The bundled differential along a composite is the composite of the bundled differentials.

theorem TauCeti.derivationCompLieHom_bijective_of_surjective_of_finrank_eq {k : Type u_1} {A : Type u_2} {A' : Type u_3} [Field k] [CommRing A] [Bialgebra k A] [CommRing A'] [Bialgebra k A'] [Module.Finite k (Derivation k A (Bialgebra.CounitAlgebra k A k))] [Module.Finite k (Derivation k A' (Bialgebra.CounitAlgebra k A' k))] (φ : A' →ₐc[k] A) (hφ : Function.Surjective ⇑φ) (hfinrank : Module.finrank k (Derivation k A (Bialgebra.CounitAlgebra k A k)) = Module.finrank k (Derivation k A' (Bialgebra.CounitAlgebra k A' k))) : Function.Bijective ⇑(derivationCompLieHom φ)

A surjective bialgebra morphism between equal-dimensional tangent Lie algebras induces a bijection on tangent Lie algebras.