Tangent images on open submanifolds

Restriction to an open source preserves the tangent image at each point. Inclusion of an open target maps the tangent image by the canonical tangent-space equivalence. These identities let pointwise conditions on tangent images be checked in open submanifolds. Since the differential of the inclusion of an open subset is the identity of the model space, restricting a map to an open source, or following a map into an open target by the inclusion, does not change its differential applied to a tangent vector. Differentiability itself is local, so a map and its restriction to an open source have vanishing differentials at the same points, with no differentiability assumption.

@[simp]

theorem TauCeti.Manifold.mdifferentiableAt_comp_subtype_val_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens N} {f : N → M} {x : ↥U} : MDiffAt (f ∘ Subtype.val) x ↔ MDiffAt f ↑x

A map is differentiable at a point of an open subset exactly when its restriction to that subset is.

@[simp]

theorem TauCeti.Manifold.mdifferentiableAt_subtype_val_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens M} {f : N → ↥U} {x : N} : MDiffAt (Subtype.val ∘ f) x ↔ MDiffAt f x

A map into an open subset is differentiable at a point exactly when its composition with the inclusion is.

theorem TauCeti.Manifold.range_mfderiv_comp_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens N} {f : N → M} (x : ↥U) (hf : MDiffAt f ↑x) : (↑(mfderiv% (f ∘ Subtype.val) x)).range = (↑(mfderiv% f ↑x)).range

Restricting a differentiable map to an open source preserves its tangent image.

theorem TauCeti.Manifold.range_mfderiv_subtype_val_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens M} {f : N → ↥U} (x : N) (hf : MDiffAt f x) : (↑(mfderiv% (Subtype.val ∘ f) x)).range = Submodule.map (↑↑(tangentSpaceOpenEquiv (f x))) (↑(mfderiv% f x)).range

Inclusion of an open target transports the tangent image by the canonical tangent-space equivalence.

theorem TauCeti.Manifold.mfderiv_comp_subtype_val_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens N} {f : N → M} {x : ↥U} (v : TangentSpace J x) : (mfderiv% (f ∘ Subtype.val) x) v = (mfderiv% f ↑x) v

Restricting a map to an open source does not change its differential.

theorem TauCeti.Manifold.mfderiv_subtype_val_comp_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens M} {f : N → ↥U} {x : N} (v : TangentSpace J x) : (mfderiv% (Subtype.val ∘ f) x) v = (mfderiv% f x) v

Following a map into an open target by the inclusion does not change its differential.

@[simp]

theorem TauCeti.Manifold.mfderiv_comp_subtype_val_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {U : TopologicalSpace.Opens N} {f : N → M} {x : ↥U} : mfderiv% (f ∘ Subtype.val) x = 0 ↔ mfderiv% f ↑x = 0

The differential of a map vanishes at a point of an open subset exactly when the differential of its restriction to that subset does. No differentiability is assumed: where the map is not differentiable, neither is its restriction, and both differentials are zero by convention.