Tangent-bundle concepts (flat case). More...
Concepts | |
| concept | dedekind::geometry::IsTangentBundle |
| A flat-case (element-wise) tangent-bundle carrier over a base scalar: a pair (point, tangent vector) with ring-shaped arithmetic. | |
Detailed Description
Tangent-bundle concepts (flat case).
@partition :tangent
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
tangent__Scope_And_Extension
Hosts the flat-case (element-wise) tangent-bundle concept, sitting next to the trivial-case TangentVector / CotangentVector aliases in :linear_map. The non-flat manifold-bundle structure (charts, atlases, fibre bundles, transition maps, smoothness) is tracked under issue~#185 and will land alongside this partition when the manifold abstraction matures, naturally pulling in dedekind.topology (manifold-as-topological-space) and dedekind.geometry (smooth structure).
tangent__Coherence
The canonical witness for IsTangentBundle is Dual<F> in dedekind.analysis:dual — forward-mode automatic differentiation on Dual<F> is exactly arithmetic in the tangent-bundle ring T(Spec F) (Hartshorne, Algebraic Geometry, Ex. II.2.8; Eisenbud, Commutative Algebra, §16.5). The witness static_assert(IsTangentBundle<Dual<F>>) is co-located with the Dual definition in :analysis (downstream of :geometry), not here, so that :tangent stays a pure concept partition and downstream carriers can register themselves without depending on each other.
- Note
- "Tangent vectors are infinitesimal arrows." — Folk lemma, attributed to many authors; the formalisation runs through Hartshorne (above) and Mac Lane, Categories for the Working Mathematician, Springer GTM 5 (2nd ed. 1971), §VII.
