Derivatives of maps that factor through a projection #
A map g ∘ Prod.fst on a product M × N depends on the first factor only, and its derivative at
p is the derivative of g at p.1 applied to the first component of a tangent vector; similarly
for g ∘ Prod.snd. No differentiability hypothesis is needed: when g is not differentiable at
p.1, neither is g ∘ Prod.fst at p, since g is recovered from it by composing with
x ↦ (x, p.2), so both derivatives vanish.
These are the chain-rule identities used to differentiate functions of one factor along vector fields on a product manifold.
Main results #
TauCeti.mfderiv_comp_fstandTauCeti.mfderiv_comp_snd: the derivative of a map that factors through a projection.TauCeti.mfderiv_snd_apply: the derivative of the second projection takes the second component of a tangent vector.TauCeti.mvfderiv_comp_fst_applyandTauCeti.mvfderiv_comp_snd_apply: the same for vector-valued functions, applied to a tangent vector.TauCeti.mvfderiv_comp_fst_mul_comp_snd_apply: the product rule for a function of the first factor times a function of the second factor.TauCeti.mvfderiv_comp_snd_apply_eq_smul_deriv: for a scalar second factor, the same in terms of the one-variable derivativederiv.TauCeti.mvfderiv_curry_right: the derivative of a slice with fixed first coordinate.HasDerivAt.mvfderiv_comp_fst_apply: the derivative of a function of the scalar coordinate of𝕜 × N.TauCeti.mfderiv_prodMap_comp_prodMkLeftandTauCeti.mfderiv_prodMap_comp_prodMkRight: composing the differential ofProd.map f gwith a slice inclusion commutes with the differential on the varied factor.MDifferentiableAt.hasLeftInverse_mfderiv_fst_prod_iff: the differential of a parameter-preserving map splits exactly when the differential of its slice splits.TauCeti.mfderiv_swap: the derivative of the exchange of factors exchanges the components.MDifferentiableAt.mfderiv_fst_applyandMDifferentiableAt.mfderiv_snd_apply: the differential of a coordinate of a map into a product.MDifferentiableAt.mfderiv_snd_eq_mfderiv_fst_of_fiberProduct: the derivative of a fibre-product condition(f y).2 = (g y).1.
The derivative of g ∘ Prod.fst at p is the derivative of g at p.1 applied to the first
component. No differentiability is needed: both sides vanish when g is not differentiable.
The derivative of g ∘ Prod.snd at p is the derivative of g at p.2 applied to the second
component. No differentiability is needed: both sides vanish when g is not differentiable.
The derivative of the second projection sends a tangent vector on a product to its second component.
The derivative of the exchange of factors Prod.swap : M × N → N × M exchanges the two
components of a tangent vector.
The derivative of a vector-valued function of the first factor, read on a product.
The derivative of a vector-valued function of the second factor, read on a product.
Product rule on a product. The derivative of (x, y) ↦ g x * h y sends a tangent vector
(u, w) at p to dg(u) * h p.2 + g p.1 * dh(w).
The derivative of a vector-valued function of a scalar second factor, read on a product: the
scalar component v.2 of a tangent vector is sent to v.2 • g'(p.2).
The derivative of a slice with fixed first coordinate is the product derivative composed with the inclusion of the second tangent factor.
The derivative of a function of the scalar coordinate of 𝕜 × N, with derivative g' at
p.1, sends a tangent vector (s, v) at p to s • g'.
Composing the differential of Prod.map f g at (x, y) with the differential of the
horizontal slice inclusion x' ↦ (x', y) equals the differential of x' ↦ (x', g y) composed with
df_x. Differentiability is needed only for g at y: when f is not differentiable at x,
neither is Prod.map f g at (x, y), so both sides vanish.
Composing the differential of Prod.map f g at (x, y) with the differential of the
vertical slice inclusion y' ↦ (x, y') equals the differential of y' ↦ (f x, y') composed with
dg_y. Differentiability is needed only for f at x: when g is not differentiable at y,
neither is Prod.map f g at (x, y), so both sides vanish.
The differential of a parameter-preserving map has a continuous linear left inverse if and only if the differential of its slice at the fixed parameter does. This holds for manifolds with corners and infinite-dimensional models.
The differential of the first coordinate of a map into a product is the first coordinate of its differential.
The differential of the second coordinate of a map into a product is the second coordinate of its differential.
Differentiating a fibre-product condition: if the second coordinate of f agrees everywhere
with the first coordinate of g, then so do the corresponding coordinates of their
differentials.