The differential of a Hopf-algebra morphism on tangent spaces

A morphism φ : A' →ₐc[R] A of Hopf algebras induces, contravariantly on coordinate rings and hence covariantly on the corresponding affine group schemes Spec A → Spec A', a map of tangent groups at the identity — over rings these are the classical tangent spaces — by precomposition of dual-number points. The coefficient algebras Bialgebra.CounitAlgebra R A B and Bialgebra.CounitAlgebra R A' B share the carrier B and its R-algebra structure, and the identity points correspond under φ because bialgebra morphisms intertwine counits; so precomposition restricts to the tangent kernels.

Main declarations

• TauCeti.tangentKerMap: the differential, as a group homomorphism between tangent kernels.
• TauCeti.tangentKerMap_id and TauCeti.tangentKerMap_comp: functoriality.
• TauCeti.tangentKerMap_derivationMulEquivTangentKer: the differential is compatible with the derivation–tangent dictionary — transporting a derivation to a tangent point and mapping it forward is precomposition of derivations.

noncomputable def TauCeti.tangentKerMap {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] (φ : A' →ₐc[R] A) : ↥(tangentKer R A B) →* ↥(tangentKer R A' B)

The differential of a Hopf-algebra morphism on tangent kernels: a morphism φ : A' →ₐc[R] A of Hopf algebras sends a dual-number point of A over the identity to a dual-number point of A' over the identity by precomposition. The coefficient identification Bialgebra.CounitAlgebra R A B = B = Bialgebra.CounitAlgebra R A' B is definitional, and the identity points correspond because φ intertwines the counits.

Equations

• TauCeti.tangentKerMap φ = ((TauCeti.AlgHom.mapDomain φ).comp (TauCeti.tangentKer R A B).subtype).codRestrict (TauCeti.tangentKer R A' B) ⋯

theorem TauCeti.tangentKerMap_apply_val {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] (φ : A' →ₐc[R] A) (ψ : ↥(tangentKer R A B)) : ↑((tangentKerMap φ) ψ) = (AlgHom.mapDomain φ) ↑ψ

The differential acts by precomposition on dual-number points. Not a simp lemma: the pointwise form tangentKerMap_apply_val_ofConv is the canonical reduction rule, and tagging both would leave its left-hand side reducible.

@[simp]

theorem TauCeti.tangentKerMap_apply_val_ofConv {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] (φ : A' →ₐc[R] A) (ψ : ↥(tangentKer R A B)) (a : A') : (↑((tangentKerMap φ) ψ)).ofConv a = (↑ψ).ofConv (↑φ a)

The differential acts pointwise by precomposition of dual-number points.

@[simp]

theorem TauCeti.tangentKerMap_id {R : Type u_1} {A : Type u_2} {B : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : tangentKerMap (BialgHom.id R A) = MonoidHom.id ↥(tangentKer R A B)

The differential of the identity morphism is the identity.

@[simp]

theorem TauCeti.tangentKerMap_comp {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] {A'' : Type u_5} [CommSemiring A''] [HopfAlgebra R A''] (φ : A' →ₐc[R] A) (χ : A'' →ₐc[R] A') : tangentKerMap (φ.comp χ) = (tangentKerMap χ).comp (tangentKerMap φ)

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

@[simp]

theorem TauCeti.tangentKerMap_derivationMulEquivTangentKer {R : Type u_5} {A : Type u_6} {A' : Type u_7} {B : Type u_8} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring A'] [HopfAlgebra R A'] [CommSemiring B] [Algebra R B] (φ : A' →ₐc[R] A) (d : Multiplicative (Derivation R A (Bialgebra.CounitAlgebra R A B))) : (tangentKerMap φ) ((derivationMulEquivTangentKer R A B) d) = (derivationMulEquivTangentKer R A' B) (Multiplicative.ofAdd ((derivationComp φ) (Multiplicative.toAdd d)))

The differential intertwines the tangent dictionaries: the image of the dual-number point of a derivation d under tangentKerMap φ is the point of the precomposed derivation derivationComp φ d.