Tangent images of graphs and product maps

Under the canonical identification of product tangent spaces, the tangent image of x ↦ (f x, g x) is the range of df × dg, that of x ↦ (x, f x) is the linear graph of df, and the tangent image of a product map f × g at (x, y) is the product of the tangent images of f at x and of g at y. These are the bridges between linear criteria for graphs and products of subspaces and geometric conditions on embedded graphs and products of submanifolds, including Lagrangian ones. The calculations use Mathlib's product derivatives, LinearMap.graph_eq_range_prod and LinearMap.range_prodMap. The coordinates of the differential of a graph are computed by mfderiv_graph_fst_apply and mfderiv_graph_snd_apply.

@[simp]

theorem TauCeti.Manifold.mfderiv_graph_fst_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {x : M} (hf : MDiffAt f x) (v : TangentSpace I x) : (((mfderiv% fun (y : M) => (y, f y)) x) v).1 = v

The differential of the graph y ↦ (y, f y) has first coordinate v.

@[simp]

theorem TauCeti.Manifold.mfderiv_graph_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {x : M} (v : TangentSpace I x) : (((mfderiv% fun (y : M) => (y, f y)) x) v).2 = (mfderiv% f x) v

The differential of the graph y ↦ (y, f y) has second coordinate df v.

theorem TauCeti.Manifold.map_range_mfderiv_prodMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} [TopologicalSpace N] [ChartedSpace H' N] {E' : Type u_8} {H'' : Type u_9} {N' : Type u_10} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H''] {J' : ModelWithCorners 𝕜 E' H''} [TopologicalSpace N'] [ChartedSpace H'' N'] {f : M → N} {g : M → N'} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g x) : Submodule.map (↑↑(tangentSpaceProdEquiv (f x, g x))) (↑((mfderiv% fun (y : M) => (f y, g y)) x)).range = ((↑(mfderiv% f x)).prod ↑(mfderiv% g x)).range

The tangent image of a map y ↦ (f y, g y) into a product, read in the product tangent spaces, is the range of the product of the differentials of its two coordinates.

@[simp]

theorem TauCeti.Manifold.map_range_mfderiv_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {x : M} (hf : MDiffAt f x) : Submodule.map (↑↑(tangentSpaceProdEquiv (x, f x))) (↑((mfderiv% fun (y : M) => (y, f y)) x)).range = (↑(mfderiv% f x)).graph

The tangent image of a graph, read in the product tangent spaces, is the graph of the original map's differential.

@[simp]

theorem TauCeti.Manifold.map_range_mfderiv_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} [TopologicalSpace N] [ChartedSpace H' N] {E' : Type u_8} {F' : Type u_9} {G : Type u_10} {G' : Type u_11} {M' : Type u_12} {N' : Type u_13} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace G] {I' : ModelWithCorners 𝕜 E' G} [TopologicalSpace M'] [ChartedSpace G M'] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M'} {g : N → N'} {p : M × N} (hf : MDiffAt f p.1) (hg : MDiffAt g p.2) : Submodule.map (↑↑(tangentSpaceProdEquiv (Prod.map f g p))) (↑(mfderiv% (Prod.map f g) p)).range = (↑(mfderiv% f p.1)).range.prod (↑(mfderiv% g p.2)).range

The tangent image of a product of differentiable maps, read in the product tangent spaces, is the product of the tangent images of the factors.