The differential on derivations

A morphism φ : A' →ₐc[R] A of bialgebras sends a counit-valued derivation of A to one of A' by precomposition. The construction splits the transport into the two halves Mathlib provides: restricting the domain along φ (Derivation.compAlgebraMap, over local scalar-tower instances for φ), and moving the coefficients across the canonical identification of the two counit coefficient algebras, which is A'-linear precisely because bialgebra morphisms intertwine counits (LinearEquiv.compDer). The Leibniz rule therefore comes from those two facts and is not reproved here.

Main declarations

• TauCeti.derivationComp: precomposition of counit-valued derivations along a bialgebra morphism, as an R-linear map — the derivation form of the differential.
• TauCeti.derivationComp_apply, TauCeti.algEquivSelf_derivationComp_apply, TauCeti.derivationComp_id, TauCeti.derivationComp_comp: it acts by precomposition, functorially and compatibly with the counit coefficient identifications.
• TauCeti.derivationComp_injective_of_surjective: precomposition along a surjective bialgebra morphism is injective.

The intertwining with the tangent dictionaries is TauCeti.tangentKerMap_derivationMulEquivTangentKer in TauCeti.Algebra.AlgebraicGroup.Tangent.Map.

noncomputable def TauCeti.derivationComp {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'] [Semiring B] [Algebra R B] (φ : A' →ₐc[R] A) : Derivation R A (Bialgebra.CounitAlgebra R A B) →ₗ[R] Derivation R A' (Bialgebra.CounitAlgebra R A' B)

Precomposition of counit-valued derivations along a bialgebra morphism, as an R-linear map: the derivation form of the differential, sending an R-derivation d : A → B at the identity point of A to a ↦ d (φ a) at the identity point of A'.

(The commutativity hypotheses on A and A' are those of Derivation itself.)

Equations

• TauCeti.derivationComp φ = { toFun := TauCeti.derivationCompAux✝ φ, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.derivationComp_apply {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'] [Semiring B] [Algebra R B] (φ : A' →ₐc[R] A) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) (a : A') : ((derivationComp φ) d) a = d (↑φ a)

The differential acts on derivations by precomposition.

theorem TauCeti.algEquivSelf_derivationComp_apply {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'] [Semiring B] [Algebra R B] (φ : A' →ₐc[R] A) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) (a : A') : (Bialgebra.CounitAlgebra.algEquivSelf R A' B) (((derivationComp φ) d) a) = (Bialgebra.CounitAlgebra.algEquivSelf R A B) (d (↑φ a))

The derivation differential is literal precomposition after identifying the two counit coefficient algebras with the original coefficient algebra.

theorem TauCeti.derivationComp_injective_of_surjective {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'] [Semiring B] [Algebra R B] (φ : A' →ₐc[R] A) (hφ : Function.Surjective ⇑φ) : Function.Injective ⇑(derivationComp φ)

Precomposition of derivations along a surjective bialgebra morphism is injective.

@[simp]

theorem TauCeti.derivationComp_id {R : Type u_1} {A : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : derivationComp (BialgHom.id R A) = LinearMap.id

Precomposition along the identity is the identity map.

@[simp]

theorem TauCeti.derivationComp_comp {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'] [Semiring B] [Algebra R B] {A'' : Type u_5} [CommSemiring A''] [Bialgebra R A''] (φ : A' →ₐc[R] A) (χ : A'' →ₐc[R] A') : derivationComp (φ.comp χ) = derivationComp χ ∘ₗ derivationComp φ

Precomposition along a composite is the composition of the precompositions.

theorem TauCeti.derivationComp_derivationComp_eq_self_of_comp_eq_id {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'] [Semiring B] [Algebra R B] (φ : A' →ₐc[R] A) (χ : A →ₐc[R] A') (h : φ.comp χ = BialgHom.id R A) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) : (derivationComp χ) ((derivationComp φ) d) = d

Precomposition along a section undoes precomposition along its retraction. If φ.comp χ is the identity — so χ is a section of φ — then derivationComp χ undoes derivationComp φ.

theorem TauCeti.derivationComp_derivationComp_eq_zero_of_comp_eq_counit_smul_one {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'] [Semiring B] [Algebra R B] {A'' : Type u_5} [CommSemiring A''] [Bialgebra R A''] (φ : A' →ₐc[R] A) (χ : A'' →ₐc[R] A') (hcomp : ∀ (a : A''), ↑φ (↑χ a) = CoalgebraStruct.counit a • 1) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) : (derivationComp χ) ((derivationComp φ) d) = 0

A composite landing in the base kills every derivation. If φ ∘ χ sends each element to the scalar multiple of 1 given by its counit, then precomposing along χ after φ annihilates derivations.