Tangent cones of sets flattened by a differentiable chart

A set S that some chart e flattens onto a closed linear subspace L (in the sense of TauCeti.IsSliceChart) has, at each of its points y, a tangent cone which is a linear subspace: it is the preimage of L under the derivative of e at y. This identifies Mathlib's intrinsic tangentConeAt with the tangent space read off any flattening chart, so a condition stated with tangent cones, such as the transversality of two submanifolds, does not depend on the charts used to verify it.

Main results

• OpenPartialHomeomorph.isInvertible_fderiv: a chart that is differentiable at a point, with inverse differentiable at the image point, has an invertible derivative there.
• TauCeti.IsSliceChart.tangentConeAt_eq_preimage: the tangent cone of a set flattened onto a closed subspace is the preimage of that subspace under the derivative of the chart.
• TauCeti.IsSliceChart.span_tangentConeAt_eq_comap: hence the span of the tangent cone is that preimage, viewed as a subspace, and it has the dimension of the model subspace (TauCeti.IsSliceChart.finrank_span_tangentConeAt).

theorem OpenPartialHomeomorph.isInvertible_fderiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {y : E} (hy : y ∈ e.source) (he : DifferentiableAt 𝕜 (↑e) y) (hes : DifferentiableAt 𝕜 (↑e.symm) (↑e y)) : (fderiv 𝕜 (↑e) y).IsInvertible

A chart which is differentiable at a point of its source, and whose inverse is differentiable at the image point, has an invertible derivative there.

theorem OpenPartialHomeomorph.exists_hasFDerivAt_of_chart {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {y : E} (hy : y ∈ e.source) (he : DifferentiableAt 𝕜 (↑e) y) (hes : DifferentiableAt 𝕜 (↑e.symm) (↑e y)) : ∃ (A : E ≃L[𝕜] F), HasFDerivAt (↑e) (↑A) y

A chart which is differentiable at a point of its source, and whose inverse is differentiable at the image point, has a derivative represented by a continuous linear equivalence.

theorem TauCeti.IsSliceChart.tangentConeAt_eq_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} {L : Submodule 𝕜 F} {S : Set E} {y : E} {A : E ≃L[𝕜] F} (h : IsSliceChart e (↑L) S) (hL : IsClosed ↑L) (hy : y ∈ e.source) (hyS : y ∈ S) (hA : HasFDerivAt (↑e) (↑A) y) : tangentConeAt 𝕜 S y = ⇑A ⁻¹' ↑L

The tangent cone of a flattened set. If the chart e flattens S onto a closed linear subspace L and has invertible derivative A at a point y of S, then the tangent cone of S at y is A⁻¹ L.

theorem TauCeti.IsSliceChart.span_tangentConeAt_eq_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} {L : Submodule 𝕜 F} {S : Set E} {y : E} {A : E ≃L[𝕜] F} (h : IsSliceChart e (↑L) S) (hL : IsClosed ↑L) (hy : y ∈ e.source) (hyS : y ∈ S) (hA : HasFDerivAt (↑e) (↑A) y) : Submodule.span 𝕜 (tangentConeAt 𝕜 S y) = Submodule.comap (↑↑A) L

The span of the tangent cone of a set flattened onto a closed subspace L, at a point where the chart has invertible derivative A, is the subspace A⁻¹ L.

theorem TauCeti.IsSliceChart.finrank_span_tangentConeAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : OpenPartialHomeomorph E F} {L : Submodule 𝕜 F} {S : Set E} {y : E} {A : E ≃L[𝕜] F} (h : IsSliceChart e (↑L) S) (hL : IsClosed ↑L) (hy : y ∈ e.source) (hyS : y ∈ S) (hA : HasFDerivAt (↑e) (↑A) y) : Module.finrank 𝕜 ↥(Submodule.span 𝕜 (tangentConeAt 𝕜 S y)) = Module.finrank 𝕜 ↥L

The tangent space of a set flattened onto a closed subspace L, at a point where the chart has invertible derivative, has the dimension of L.