Continuously homotopic smooth maps can be inserted directly into the differential form homotopy operator

Given: $M$ is a point, $N=\mathbb{R}$, and $H(t)=\mathrm{\mid }t-1\mathrm{/}2\mathrm{\mid }$ on $[0,1]$.

Integration along the unit interval for a differential form: Let $\omega \in {\mathrm{\Omega }}^k(M\times [0,1])$ be smooth up to the endpoints. For $k\ge 1$, its interval integral is the $(k-1)$-form $K\omega ={\int }_0^1{\beta }_{t}dt$, where $\omega ={\alpha }_t+dt\wedge {\beta }_t$ and both families are tangential to $M$. Set $K=0$ on degree zero and on zero terms. Use the product structure of prop-products-of-smooth-manifolds-have-a-canonical-product-smooth-structure, restricted from $M\times \mathbb{R}$. The families are intrinsically ${\alpha }_t=i_t^{\ast }\omega$ and ${\beta }_t=i_t^{\ast }({\iota }_{{\mathrm{\partial }}_t}\omega )$, using def-interior-product-of-a-form-by-a-vector-field; evaluation on tangential tuples and on $({\mathrm{\partial }}_t,v_1,\dots ,v_{k-1})$ proves existence and uniqueness of the decomposition. The integral is in the fixed finite-dimensional fibre ${\bigwedge }^{k-1}{T}_x^{\ast }M$. Coefficients have smooth local extensions across endpoints. thm-differentiation-under-the-integral-sign-on-a-compact-rectangle supplies parameter differentiation; coordinate independence and full smoothness are proved in lem-the-interval-homotopy-operator-is-coordinate-independent.

De rham homotopy formula for a smooth homotopy: If $F:M\times [0,1]\to N$ is smooth up to the endpoints and $F_t(x)=F(x,t)$, then $F_1^{\ast }-F_0^{\ast }=d(K{F}^{\ast })+(K{F}^{\ast })d$.