The constructions in Definition [fcap-001R]--Example [fcap-001V] start with a
smooth homomorphism. Their tangent map, bracket law, functor laws, and
exponential naturality therefore do not require a theorem that upgrades a
continuous homomorphism to a smooth one. The generic theorem does not invoke
the closed-subgroup theorem; that theorem belongs to the later specialization
to concrete matrix subgroups. This is the dependency split recorded in
TauCetiRoadmap
PR 224.
The exponential input is separate from the tangent and bracket input.
Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a
matrix or general-linear group; using it inside a particular closed matrix
subgroup additionally requires the subgroup's Lie structure. Liu describes
the local exponential and BCH coordinates, while Isaev--Rubakov give the
matrix Campbell--Hausdorff calculation.
Tau Ceti's generic interface now defines the Lie map of a bundled smooth
monoid morphism between finite-dimensional real Lie groups
lieMap. It proves the identity and composition laws
lieMap_id, lieMap_comp, and exponential
naturality map_lieExp. These declarations act on
left-invariant derivations and require the corresponding smooth Lie-group
structures.
The generic interface does not by itself identify the differential of
\(\operatorname {Spin}(Q)\to SO(Q)\) inside the vector-generated Clifford carrier. The
closed-subgroup realization, tangent calculation, and quadratic-lift
comparison are supplied in Proposition [fcap-0037].
Thus the generic Lie functor and the Clifford calculation retain distinct
hypotheses and meet only after the actual group structure has been
established.