Tautological one-form on a cotangent bundle

Assume ${\mathrm{A}\mathrm{C}}_{\omega }$. For a smooth $n$-manifold $Q$, Assuming countable choice, the cotangent bundle has a canonical smooth 2n-manifold structure supplies the smooth cotangent manifold $T^{\ast }Q$ and its induced cotangent charts. Let $\pi :T^{\ast }Q\to Q$ be the set-theoretic bundle projection. In every induced chart it is the coordinate projection, so it is smooth. The tautological one-form $\lambda \in {\mathrm{\Omega }}^1(T^{\ast }Q)$ is

${\lambda }_{(q,p)}(\xi )=p(d{\pi }_{(q,p)}\xi ),p\in T_q^{\ast }Q\mathrm{.}$

Indeed, in an induced cotangent chart write $p={\sum }_i{p}_{i}d{q}^i$ and $\xi ={\sum }_i{a}^i{\mathrm{\partial }}_{q^i}+{\sum }_i{b}_i{\mathrm{\partial }}_{p_i}$. Then

${\lambda }_{(q,p)}(\xi )={\sum }_i{p}_i{a}^i,\text{so}\lambda ={\sum }_i{p}_{i}d{q}^i,$

which proves that the definition is smooth and independent of any local choice because its pointwise formula uses only $p$ and $d\pi$.

The library's canonical cotangent two-form is, by convention,

${\omega }_{\mathrm{c}\mathrm{a}\mathrm{n}}=-d\lambda ,$

where $d$ is the exterior derivative supplied by Existence and uniqueness of the exterior derivative.

The countable-choice assumption is used exactly to obtain the smooth manifold structure on $T^{\ast }Q$ from the cited supplier; the evaluation and coordinate formulas themselves make no further choice. For $n=0$ the unique one-form and two-form are both zero; the same formulas cover the empty manifold and there is no endpoint, denominator, or biconditional issue. Here ${\mathrm{A}\mathrm{C}}_{\omega }$ is countable choice.