The tangent space at the identity point

For a bialgebra A over R, the identity B-point of the functor of points is the counit followed by the structure map — the unit of the convolution monoid whenever the latter exists. This file packages B as an A-algebra through that point (Bialgebra.CounitAlgebra), so that the dual-number dictionary TauCeti.derivationToDualNumberEquivLift applies verbatim: derivations of A at the identity point are the dual-number points lying over the identity (the dictionary applied at Bialgebra.CounitAlgebra).

For A a Hopf algebra and B commutative, the dual-number points form a convolution group, reduction of the infinitesimal part is a group homomorphism (dualNumberReduction), and its kernel tangentKer is multiplicatively equivalent to the additive monoid of derivations at the identity (derivationMulEquivTangentKer); in particular the kernel is a commutative group (the CommGroup (tangentKer R A B) instance).

This identifies counit-valued derivations with the first-order infinitesimal kernel. The additive wrapper of the kernel inherits its natural B-module structure through this identification, and derivationLinearEquivTangentKer records the resulting linear equivalence. No Lie bracket or functoriality in B is constructed here — first-order commutativity of the kernel says nothing about the Lie bracket, which appears at second order.

The synonym CounitAlgebra is a fresh scope for the point-induced algebra structure, as the dictionary requires; it does not install instances on B itself, and Bialgebra.CounitAlgebra.algEquivSelf transports back to B as an R-algebra. An algebra homomorphism between coefficient algebras transports these synonyms via Bialgebra.CounitAlgebra.mapAlgHom; Bialgebra.CounitAlgebra.map records that this transport is linear for the actions induced by the counit.

The general generator criterion Derivation.apply_eq_zero_of_mem_span says that a counit-valued derivation vanishing on counit-zero generators vanishes on their ideal span.

The exterior convolution product

This file applies the exterior convolution product LinearMap.mulTensor — two convolution linear maps applied legwise on A ⊗[R] A and multiplied in the coefficients — to counit-valued derivations. The product itself, together with its normalization rules (zero, addition, scalars) and its multiplicativity for convolution, is defined generically in TauCeti/Algebra/Coalgebra/Convolution.lean. Composing with the multiplication of A lands in this product's image: an algebra-map point satisfies g ∘ mul = g ⊠ g (AlgHom.toConv_toLinearMap_comp_mul'), and a counit-valued derivation satisfies the Leibniz rule d ∘ mul = 1 ⊠ d + d ⊠ 1 (Derivation.toConv_coe_comp_mul'). This calculus lives here, at the tangent level, because every later structure on the tangent space — the Lie bracket and the adjoint action alike — is a composition-level consequence of these three identities.

def TauCeti.Bialgebra.CounitAlgebra (_R : Type u_4) (_A : Type u_5) (B : Type u_6) : Type u_6

Type synonym: B as an A-algebra through the identity point of the functor of points — the counit followed by the structure map, which is the convolution unit whenever B is commutative (toAlgHom_eq_one_ofConv); at semiring B the convolution monoid does not exist and the composite is its generalization. Derivations of A valued in Bialgebra.CounitAlgebra R A B are the tangent vectors at the identity.

Equations

• TauCeti.Bialgebra.CounitAlgebra _R _A B = B

@[instance_reducible]

instance TauCeti.Bialgebra.CounitAlgebra.instSemiring (R : Type u_1) (A : Type u_2) (B : Type u_3) [Semiring B] : Semiring (CounitAlgebra R A B)

Equations

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

@[instance_reducible]

instance TauCeti.Bialgebra.CounitAlgebra.instAlgebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] : Algebra R (CounitAlgebra R A B)

Equations

• TauCeti.Bialgebra.CounitAlgebra.instAlgebra R A B = TauCeti.Bialgebra.CounitAlgebra.instAlgebra._aux_3 R A B

def TauCeti.Bialgebra.CounitAlgebra.algEquivSelf (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] : CounitAlgebra R A B ≃ₐ[R] B

The canonical R-algebra identification of the counit-point coefficient algebra with B itself.

Equations

• TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R A B = AlgEquiv.refl

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.algEquivSelf_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] (x : CounitAlgebra R A B) : (algEquivSelf R A B) x = x

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.algEquivSelf_symm_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] (b : B) : (algEquivSelf R A B).symm b = b

@[instance_reducible, instance 100]

instance TauCeti.Bialgebra.CounitAlgebra.instModule {R : Type u_4} {A : Type u_5} {B : Type u_6} [Semiring B] : Module B (CounitAlgebra R A B)

The coefficient synonym is a module over the coefficients, inherited from B. Its lower priority lets Algebra.toModule remain canonical when the coefficient and base rings coincide.

Equations

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

instance TauCeti.Bialgebra.CounitAlgebra.instSMulCommClass {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [Semiring B] [Algebra R B] : SMulCommClass R B (CounitAlgebra R A B)

Base and coefficient scalars commute on the synonym, inherited from B.

instance TauCeti.Bialgebra.CounitAlgebra.instIsScalarTower {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [Semiring B] [Algebra R B] : IsScalarTower R B (CounitAlgebra R A B)

Base scalars act through the coefficient algebra on the coefficient synonym.

instance TauCeti.Bialgebra.CounitAlgebra.instIsScalarTowerSemiring {R : Type u_4} {A : Type u_5} {B : Type u_6} [Semiring B] : IsScalarTower B (CounitAlgebra R A B) (CounitAlgebra R A B)

Coefficient scalars associate with the synonym's multiplication, inherited from B.

@[instance_reducible]

instance TauCeti.Bialgebra.CounitAlgebra.instRing {R : Type u_1} {A : Type u_2} {B : Type u_3} [Ring B] : Ring (CounitAlgebra R A B)

The counit-point coefficient synonym is a ring whenever B is.

Equations

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

@[instance_reducible]

instance TauCeti.Bialgebra.CounitAlgebra.instCommRing {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing B] : CommRing (CounitAlgebra R A B)

The counit-point coefficient synonym is a commutative ring whenever B is.

Equations

• TauCeti.Bialgebra.CounitAlgebra.instCommRing = { toRing := TauCeti.Bialgebra.CounitAlgebra.instRing, mul_comm := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.Bialgebra.CounitAlgebra.instAlgebra_1 (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : Algebra A (CounitAlgebra R A B)

Equations

• TauCeti.Bialgebra.CounitAlgebra.instAlgebra_1 R A B = ((Algebra.ofId R B).comp (Bialgebra.counitAlgHom R A)).toAlgebra' ⋯

instance TauCeti.Bialgebra.CounitAlgebra.instIsScalarTower_1 (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : IsScalarTower R A (CounitAlgebra R A B)

instance TauCeti.Bialgebra.CounitAlgebra.instSMulCommClass_1 (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : SMulCommClass B A (CounitAlgebra R A B)

Scalars of the coefficient algebra commute with the bialgebra scalar action, because the latter multiplies by a central element — the image of the counit in B.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.algebraMap_base (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] (r : R) : (algebraMap R (CounitAlgebra R A B)) r = (algebraMap R B) r

The base R-algebra map of the coefficient synonym agrees with that of B itself: the synonym changes only the A-algebra structure.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.algebraMap_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] (a : A) : (algebraMap A (CounitAlgebra R A B)) a = (algebraMap R B) (CoalgebraStruct.counit a)

theorem TauCeti.Bialgebra.CounitAlgebra.algEquivSelf_smul (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] (a : A) (z : CounitAlgebra R A B) : (algEquivSelf R A B) (a • z) = (algebraMap R B) (CoalgebraStruct.counit a) * (algEquivSelf R A B) z

The coordinate algebra acts on the coefficient ring through the counit.

@[instance_reducible]

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

Counit-valued derivations carry their pointwise B-module structure through the coefficient type synonym.

Equations

• TauCeti.instModuleDerivationCounitAlgebra = { toDistribMulAction := Derivation.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

theorem TauCeti.algEquivSelf_derivation_smul_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] (b : B) (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) (a : A) : (Bialgebra.CounitAlgebra.algEquivSelf R A B) ((b • d) a) = b * (Bialgebra.CounitAlgebra.algEquivSelf R A B) (d a)

Scalar multiplication of counit-valued derivations agrees with multiplication after identifying the coefficient type synonym with the original coefficient algebra.

theorem TauCeti.Bialgebra.CounitAlgebra.algEquivSelf_apply_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] (d : Derivation R A (CounitAlgebra R A B)) (a b : A) : (algEquivSelf R A B) (d (a * b)) = (algebraMap R B) (CoalgebraStruct.counit a) * (algEquivSelf R A B) (d b) + (algebraMap R B) (CoalgebraStruct.counit b) * (algEquivSelf R A B) (d a)

The Leibniz rule of a counit-valued derivation, read in the coefficient algebra.

theorem Derivation.apply_eq_zero_of_mem_span {R : Type u_1} {H : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [CommSemiring B] [Algebra R B] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H B)) {S : Set H} (hcounit : ∀ x ∈ S, CoalgebraStruct.counit x = 0) (hd : ∀ x ∈ S, d x = 0) {x : H} (hx : x ∈ Ideal.span S) : d x = 0

A counit-valued derivation which vanishes on a set of counit-zero elements vanishes on the ideal generated by that set.

noncomputable def TauCeti.Bialgebra.CounitAlgebra.mapAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) : CounitAlgebra R A B →ₐ[R] CounitAlgebra R A C

An algebra homomorphism of coefficients, transported to the counit coefficient algebras.

Equations

• TauCeti.Bialgebra.CounitAlgebra.mapAlgHom phi = (↑(TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R A C).symm).comp (phi.comp ↑(TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R A B))

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.algEquivSelf_map {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) (b : CounitAlgebra R A B) : (algEquivSelf R A C) (phi b) = phi ((algEquivSelf R A B) b)

Identifying counit coefficient algebras with their coefficient rings commutes with an algebra homomorphism of coefficients.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.mapAlgHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) (b : CounitAlgebra R A B) : (mapAlgHom phi) b = phi b

Transport of counit coefficient algebras acts pointwise by the original coefficient homomorphism.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.mapAlgHom_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring B] [Algebra R B] : mapAlgHom (AlgHom.id R B) = AlgHom.id R (CounitAlgebra R A B)

The identity coefficient homomorphism induces the identity homomorphism of counit coefficient algebras.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.mapAlgHom_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {D : Type u_5} [Semiring D] [Algebra R D] (psi : C →ₐ[R] D) (phi : B →ₐ[R] C) : mapAlgHom (psi.comp phi) = (mapAlgHom psi).comp (mapAlgHom phi)

Homomorphisms of counit coefficient algebras preserve composition.

noncomputable def TauCeti.Bialgebra.CounitAlgebra.map {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) : CounitAlgebra R A B →ₗ[A] CounitAlgebra R A C

An algebra map between coefficient algebras, regarded as a linear map for the A-module structures induced by the counit.

Equations

• TauCeti.Bialgebra.CounitAlgebra.map phi = { toFun := ⇑(TauCeti.Bialgebra.CounitAlgebra.mapAlgHom phi), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.map_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) (b : CounitAlgebra R A B) : (map phi) b = phi b

The linear coefficient map has the same underlying function as the coefficient algebra map.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.map_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : map (AlgHom.id R B) = LinearMap.id

The identity algebra homomorphism induces the identity coefficient map.

@[simp]

theorem TauCeti.Bialgebra.CounitAlgebra.map_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {D : Type u_5} [Semiring D] [Algebra R D] (psi : C →ₐ[R] D) (phi : B →ₐ[R] C) : map (psi.comp phi) = map psi ∘ₗ map phi

Coefficient maps preserve composition.

instance TauCeti.instSMulCommClassCounitAlgebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring B] : SMulCommClass B (Bialgebra.CounitAlgebra R A B) (Bialgebra.CounitAlgebra R A B)

Coefficient scalars commute with multiplication in the coefficient synonym.

@[instance_reducible]

instance TauCeti.instCommSemiringCounitAlgebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring B] : CommSemiring (Bialgebra.CounitAlgebra R A B)

Equations

• TauCeti.instCommSemiringCounitAlgebra R A B = { toSemiring := TauCeti.Bialgebra.CounitAlgebra.instSemiring R A B, mul_comm := ⋯ }

noncomputable def TauCeti.dualNumberReduction (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] : WithConv (A →ₐ[R] DualNumber (Bialgebra.CounitAlgebra R A B)) →* WithConv (A →ₐ[R] Bialgebra.CounitAlgebra R A B)

Reduction of dual-number points to their classical part, as a homomorphism of convolution monoids: postcomposition with the infinitesimal augmentation B[ε] → B. For a Hopf algebra its kernel is the tangent space at the identity.

Equations

• TauCeti.dualNumberReduction R A B = TauCeti.AlgHom.mapValue (TrivSqZeroExt.fstHom R (TauCeti.Bialgebra.CounitAlgebra R A B) (TauCeti.Bialgebra.CounitAlgebra R A B))

theorem TauCeti.dualNumberReduction_def (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] : dualNumberReduction R A B = AlgHom.mapValue (TrivSqZeroExt.fstHom R (Bialgebra.CounitAlgebra R A B) (Bialgebra.CounitAlgebra R A B))

dualNumberReduction is postcomposition with the classical-part projection.

@[simp]

theorem TauCeti.dualNumberReduction_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] (ψ : WithConv (A →ₐ[R] DualNumber (Bialgebra.CounitAlgebra R A B))) (x : A) : ((dualNumberReduction R A B) ψ).ofConv x = (TrivSqZeroExt.fstHom R (Bialgebra.CounitAlgebra R A B) (Bialgebra.CounitAlgebra R A B)) (ψ.ofConv x)

theorem TauCeti.Bialgebra.CounitAlgebra.toAlgHom_eq_one_ofConv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommSemiring B] [Algebra R B] : IsScalarTower.toAlgHom R A (CounitAlgebra R A B) = WithConv.ofConv 1

Where the convolution monoid exists — commutative B — the identity point through which CounitAlgebra is built is the convolution unit.

noncomputable def TauCeti.tangentKer (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : Subgroup (WithConv (A →ₐ[R] DualNumber (Bialgebra.CounitAlgebra R A B)))

The tangent subgroup: dual-number points of A lying over the identity point, as the kernel of the reduction inside the convolution group. Over commutative rings this is the additive group of the tangent space at the identity of the corresponding affine group scheme; the Lie bracket is second-order data and is not carried by this subgroup.

Equations

• TauCeti.tangentKer R A B = (TauCeti.dualNumberReduction R A B).ker

theorem TauCeti.tangentKer_def (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : tangentKer R A B = (dualNumberReduction R A B).ker

tangentKer is the kernel of the dual-number reduction.

@[simp]

theorem TauCeti.fst_apply_of_mem_tangentKer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] {ψ : WithConv (A →ₐ[R] DualNumber (Bialgebra.CounitAlgebra R A B))} (h : ψ ∈ tangentKer R A B) (x : A) : TrivSqZeroExt.fst (ψ.ofConv x) = (algebraMap R (Bialgebra.CounitAlgebra R A B)) (CoalgebraStruct.counit x)

The classical part of any tangent-kernel point is the identity point: pointwise, the first component of its value at x is algebraMap R _ (counit x).

noncomputable def TauCeti.derivationMulEquivTangentKer (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : Multiplicative (Derivation R A (Bialgebra.CounitAlgebra R A B)) ≃* ↥(tangentKer R A B)

The group of the tangent space at the identity: the kernel of the dual-number reduction is, additively, the derivations at the identity point. Convolution of dual-number points over the identity corresponds to addition of derivations.

Equations

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

@[simp]

theorem TauCeti.mem_tangentKer_iff (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] {ψ : WithConv (A →ₐ[R] DualNumber (Bialgebra.CounitAlgebra R A B))} : ψ ∈ tangentKer R A B ↔ (TrivSqZeroExt.fstHom R (Bialgebra.CounitAlgebra R A B) (Bialgebra.CounitAlgebra R A B)).comp ψ.ofConv = IsScalarTower.toAlgHom R A (Bialgebra.CounitAlgebra R A B)

Membership in the tangent subgroup: a dual-number point lies in tangentKer iff its classical part is the identity point of the tower.

theorem TauCeti.derivationMulEquivTangentKer_apply_fst {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (d : Multiplicative (Derivation R A (Bialgebra.CounitAlgebra R A B))) (a : A) : TrivSqZeroExt.fst ((↑((derivationMulEquivTangentKer R A B) d)).ofConv a) = (algebraMap A (Bialgebra.CounitAlgebra R A B)) a

@[simp]

theorem TauCeti.derivationMulEquivTangentKer_apply_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (d : Multiplicative (Derivation R A (Bialgebra.CounitAlgebra R A B))) (a : A) : TrivSqZeroExt.snd ((↑((derivationMulEquivTangentKer R A B) d)).ofConv a) = (Multiplicative.toAdd d) a

@[simp]

theorem TauCeti.derivationMulEquivTangentKer_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (ψ : ↥(tangentKer R A B)) (a : A) : (Multiplicative.toAdd ((derivationMulEquivTangentKer R A B).symm ψ)) a = TrivSqZeroExt.snd ((↑ψ).ofConv a)

@[instance_reducible]

noncomputable instance TauCeti.instCommGroupSubtypeWithConvAlgHomDualNumberCounitAlgebraMemSubgroupTangentKer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : CommGroup ↥(tangentKer R A B)

The tangent subgroup is abelian: first-order infinitesimal points commute, because multiplication corresponds to addition of derivations under derivationMulEquivTangentKer.

Equations

• TauCeti.instCommGroupSubtypeWithConvAlgHomDualNumberCounitAlgebraMemSubgroupTangentKer = { toGroup := (TauCeti.tangentKer R A B).toGroup, mul_comm := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.instModuleAdditiveSubtypeWithConvAlgHomDualNumberCounitAlgebraMemSubgroupTangentKer {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : Module B (Additive ↥(tangentKer R A B))

The natural B-module structure on the tangent kernel, written additively and transported from counit-valued derivations.

Equations

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

noncomputable def TauCeti.derivationLinearEquivTangentKer (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] : Derivation R A (Bialgebra.CounitAlgebra R A B) ≃ₗ[B] Additive ↥(tangentKer R A B)

The tangent kernel at the identity is linearly equivalent to the module of derivations at the counit point.

Equations

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

@[simp]

theorem TauCeti.derivationLinearEquivTangentKer_apply_toMul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) : Additive.toMul ((derivationLinearEquivTangentKer R A B) d) = (derivationMulEquivTangentKer R A B) (Multiplicative.ofAdd d)

Applying derivationLinearEquivTangentKer and removing the additive type tag recovers derivationMulEquivTangentKer.

@[simp]

theorem TauCeti.derivationLinearEquivTangentKer_symm_apply_toAdd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (ψ : Additive ↥(tangentKer R A B)) : (derivationLinearEquivTangentKer R A B).symm ψ = Multiplicative.toAdd ((derivationMulEquivTangentKer R A B).symm (Additive.toMul ψ))

Applying the inverse of derivationLinearEquivTangentKer recovers the derivation underlying the inverse of derivationMulEquivTangentKer.

theorem TauCeti.derivationLinearEquivTangentKer_apply_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (d : Derivation R A (Bialgebra.CounitAlgebra R A B)) (a : A) : TrivSqZeroExt.snd ((↑(Additive.toMul ((derivationLinearEquivTangentKer R A B) d))).ofConv a) = d a

The second component of the tangent point associated to a derivation is the value of that derivation.

theorem TauCeti.derivationLinearEquivTangentKer_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (ψ : Additive ↥(tangentKer R A B)) (a : A) : ((derivationLinearEquivTangentKer R A B).symm ψ) a = TrivSqZeroExt.snd ((↑(Additive.toMul ψ)).ofConv a)

The inverse linear equivalence evaluates a tangent point at a by taking its second component at a.

@[simp]

theorem TauCeti.tangentKer_smul_apply_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] (b : B) (ψ : Additive ↥(tangentKer R A B)) (a : A) : TrivSqZeroExt.snd ((↑(Additive.toMul (b • ψ))).ofConv a) = (Bialgebra.CounitAlgebra.algEquivSelf R A B).symm (b * (Bialgebra.CounitAlgebra.algEquivSelf R A B) (TrivSqZeroExt.snd ((↑(Additive.toMul ψ)).ofConv a)))

Scalar multiplication on the additive tangent kernel multiplies its second component, viewed in B through Bialgebra.CounitAlgebra.algEquivSelf.

@[simp]

theorem Derivation.toConv_coe_comp_mul' {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : WithConv.toConv (↑d ∘ₗ LinearMap.mul' R A) = TauCeti.LinearMap.mulTensor 1 (WithConv.toConv ↑d) + TauCeti.LinearMap.mulTensor (WithConv.toConv ↑d) 1

The Leibniz rule in convolution form: composing a counit-valued derivation with the multiplication of A is the exterior product against the convolution unit, on either side.