Transverse intersections of flattened sets

Let S₁ and S₂ be subsets of a finite-dimensional space which are flattened, near a common point y, by forward C^n charts (n ≥ 1) whose inverses are differentiable at the images of y. They meet transversally at y when their tangent spaces at y span the whole space. The tangent spaces are taken intrinsically, as the spans of Mathlib's tangent cones tangentConeAt; by TauCeti.IsSliceChart.span_tangentConeAt_eq_comap this agrees with the tangent space read off either chart.

This file proves that a transverse intersection is again an embedded C^n submanifold near y, whose tangent space is the intersection of the two tangent spaces: there is a C^n chart with C^n inverse flattening S₁ ∩ S₂ onto that intersection of subspaces, and the span of the tangent cone of S₁ ∩ S₂ at y is that intersection. Its dimension is therefore dim T₁ + dim T₂ - dim E.

The most common second set is a regular level set g⁻¹ {0}, whose tangent space is ker g'; cutting by it is transverse when the tangent space of the first set and ker g' span the whole space.

Main results

• TauCeti.exists_isSliceChart_inter_of_span_tangentConeAt_sup_eq_top: a transverse intersection of two flattened sets is flattened onto the intersection of their tangent spaces.
• TauCeti.span_tangentConeAt_inter_of_span_tangentConeAt_sup_eq_top: the tangent space of a transverse intersection is the intersection of the two tangent spaces.
• TauCeti.span_tangentConeAt_preimage_zero: the tangent space of a regular level set g⁻¹ {0} is the kernel of the derivative of g.
• TauCeti.exists_isSliceChart_inter_preimage_zero and TauCeti.span_tangentConeAt_inter_preimage_zero: the same two statements for the cut of a flattened set by a transverse regular level set.

References

• V. Guillemin and A. Pollack, Differential Topology, Prentice-Hall, 1974, Chapter 1, §5.

theorem TauCeti.exists_isSliceChart_inter_of_span_tangentConeAt_sup_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : WithTop ℕ∞} (hn : n ≠ 0) {S₁ S₂ : Set E} {L₁ L₂ : Submodule 𝕜 E} {e₁ e₂ : OpenPartialHomeomorph E E} {y : E} (h₁ : IsSliceChart e₁ (↑L₁) S₁) (h₂ : IsSliceChart e₂ (↑L₂) S₂) (hy₁ : y ∈ e₁.source) (hy₂ : y ∈ e₂.source) (hyS₁ : y ∈ S₁) (hyS₂ : y ∈ S₂) (hc₁ : ∀ z ∈ e₁.source, ContDiffAt 𝕜 n (↑e₁) z) (hc₂ : ∀ z ∈ e₂.source, ContDiffAt 𝕜 n (↑e₂) z) (hs₁ : DifferentiableAt 𝕜 (↑e₁.symm) (↑e₁ y)) (hs₂ : DifferentiableAt 𝕜 (↑e₂.symm) (↑e₂ y)) (htr : Submodule.span 𝕜 (tangentConeAt 𝕜 S₁ y) ⊔ Submodule.span 𝕜 (tangentConeAt 𝕜 S₂ y) = ⊤) : ∃ (e : OpenPartialHomeomorph E E), y ∈ e.source ∧ (∀ z ∈ e.source, ContDiffAt 𝕜 n (↑e) z) ∧ (∀ z ∈ e.target, ContDiffAt 𝕜 n (↑e.symm) z) ∧ IsSliceChart e (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 S₁ y) ⊓ Submodule.span 𝕜 (tangentConeAt 𝕜 S₂ y))) (S₁ ∩ S₂)

A transverse intersection of embedded submanifolds is an embedded submanifold. Let C^n charts e₁ and e₂ (n ≠ 0), with inverses differentiable at the images of y, flatten S₁ and S₂ onto linear subspaces near a common point y. If the tangent spaces of S₁ and S₂ at y span the whole space, then a C^n chart with C^n inverse flattens S₁ ∩ S₂ near y onto the intersection of those tangent spaces.

theorem TauCeti.span_tangentConeAt_inter_of_span_tangentConeAt_sup_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : WithTop ℕ∞} (hn : n ≠ 0) {S₁ S₂ : Set E} {L₁ L₂ : Submodule 𝕜 E} {e₁ e₂ : OpenPartialHomeomorph E E} {y : E} (h₁ : IsSliceChart e₁ (↑L₁) S₁) (h₂ : IsSliceChart e₂ (↑L₂) S₂) (hy₁ : y ∈ e₁.source) (hy₂ : y ∈ e₂.source) (hyS₁ : y ∈ S₁) (hyS₂ : y ∈ S₂) (hc₁ : ∀ z ∈ e₁.source, ContDiffAt 𝕜 n (↑e₁) z) (hc₂ : ∀ z ∈ e₂.source, ContDiffAt 𝕜 n (↑e₂) z) (hs₁ : DifferentiableAt 𝕜 (↑e₁.symm) (↑e₁ y)) (hs₂ : DifferentiableAt 𝕜 (↑e₂.symm) (↑e₂ y)) (htr : Submodule.span 𝕜 (tangentConeAt 𝕜 S₁ y) ⊔ Submodule.span 𝕜 (tangentConeAt 𝕜 S₂ y) = ⊤) : Submodule.span 𝕜 (tangentConeAt 𝕜 (S₁ ∩ S₂) y) = Submodule.span 𝕜 (tangentConeAt 𝕜 S₁ y) ⊓ Submodule.span 𝕜 (tangentConeAt 𝕜 S₂ y)

The tangent space of a transverse intersection. Under the hypotheses of TauCeti.exists_isSliceChart_inter_of_span_tangentConeAt_sup_eq_top, the tangent space of S₁ ∩ S₂ at y, taken intrinsically as the span of its tangent cone, is the intersection of the tangent spaces of S₁ and S₂ at y.

theorem TauCeti.span_tangentConeAt_preimage_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (hn : n ≠ 0) {g : E → F} {g' : E →L[𝕜] F} {y : E} (hg : HasStrictFDerivAt g g' y) (hg' : (↑g').range = ⊤) (hy : g y = 0) {U : Set E} (hU : IsOpen U) (hyU : y ∈ U) (hC : ∀ z ∈ U, ContDiffAt 𝕜 n g z) : Submodule.span 𝕜 (tangentConeAt 𝕜 (g ⁻¹' {0}) y) = (↑g').ker

The tangent space of a regular level set. If g is C^n (n ≠ 0) on an open set around a zero y, with surjective strict derivative g' at y, then the tangent space of the zero set of g at y, taken intrinsically as the span of its tangent cone, is ker g'.

theorem TauCeti.exists_isSliceChart_inter_preimage_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (hn : n ≠ 0) {S : Set E} {L : Submodule 𝕜 E} {e₁ : OpenPartialHomeomorph E E} {y : E} (h₁ : IsSliceChart e₁ (↑L) S) (hy₁ : y ∈ e₁.source) (hyS : y ∈ S) (hc₁ : ∀ z ∈ e₁.source, ContDiffAt 𝕜 n (↑e₁) z) (hs₁ : DifferentiableAt 𝕜 (↑e₁.symm) (↑e₁ y)) {g : E → F} {g' : E →L[𝕜] F} (hg : HasStrictFDerivAt g g' y) (hg' : (↑g').range = ⊤) (hgy : g y = 0) {U : Set E} (hU : IsOpen U) (hyU : y ∈ U) (hC : ∀ z ∈ U, ContDiffAt 𝕜 n g z) (htr : Submodule.span 𝕜 (tangentConeAt 𝕜 S y) ⊔ (↑g').ker = ⊤) : ∃ (e : OpenPartialHomeomorph E E), y ∈ e.source ∧ (∀ z ∈ e.source, ContDiffAt 𝕜 n (↑e) z) ∧ (∀ z ∈ e.target, ContDiffAt 𝕜 n (↑e.symm) z) ∧ IsSliceChart e (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 S y) ⊓ (↑g').ker)) (S ∩ g ⁻¹' {0})

Cutting by a transverse regular level set. Let a C^n chart e₁ (n ≠ 0), whose inverse is differentiable at e₁ y, flatten S onto a linear subspace near y ∈ S, and let g be C^n on an open set around y, with g y = 0 and surjective strict derivative g' at y. If the tangent space of S at y and ker g' span the whole space, then a C^n chart with C^n inverse flattens S ∩ g⁻¹ {0} near y onto the intersection of the tangent space of S with ker g'.

theorem TauCeti.span_tangentConeAt_inter_preimage_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (hn : n ≠ 0) {S : Set E} {L : Submodule 𝕜 E} {e₁ : OpenPartialHomeomorph E E} {y : E} (h₁ : IsSliceChart e₁ (↑L) S) (hy₁ : y ∈ e₁.source) (hyS : y ∈ S) (hc₁ : ∀ z ∈ e₁.source, ContDiffAt 𝕜 n (↑e₁) z) (hs₁ : DifferentiableAt 𝕜 (↑e₁.symm) (↑e₁ y)) {g : E → F} {g' : E →L[𝕜] F} (hg : HasStrictFDerivAt g g' y) (hg' : (↑g').range = ⊤) (hgy : g y = 0) {U : Set E} (hU : IsOpen U) (hyU : y ∈ U) (hC : ∀ z ∈ U, ContDiffAt 𝕜 n g z) (htr : Submodule.span 𝕜 (tangentConeAt 𝕜 S y) ⊔ (↑g').ker = ⊤) : Submodule.span 𝕜 (tangentConeAt 𝕜 (S ∩ g ⁻¹' {0}) y) = Submodule.span 𝕜 (tangentConeAt 𝕜 S y) ⊓ (↑g').ker

The tangent space of a cut by a transverse regular level set. Under the hypotheses of TauCeti.exists_isSliceChart_inter_preimage_zero, the tangent space of S ∩ g⁻¹ {0} at y is the intersection of the tangent space of S at y with ker g'.