The tangent space at the identity

Aggregator for the tangent-level theory: the counit-valued derivations (Tangent.Basic), the points valued in the counit algebra (Tangent.CounitPoints), their description by the cotangent space (Tangent.Cotangent), finiteness at an identity of finite type (Tangent.FiniteType), tangent dimensions and their invariance under coefficient-field extension (Tangent.Dimension), the Krull-dimension bound and regularity criterion at the identity (Tangent.KrullDimension), functoriality in the bialgebra (Tangent.DerivationMap, Tangent.Map) and coefficient algebra (Tangent.Naturality), and the adjoint action of the points (Tangent.Adjoint), including equivariance of the differential (Tangent.Equivariance). The Lie-algebra structure lives in the Tangent.Lie aggregator.