6.8. MappingDegree.ChartLocalDetour🔗

Jacobians.MappingDegree.ChartLocalDetour — source

joinedIn_symm_image_of_target

Generic chart-side detour pull-back. If φ : X → Y is an open partial homeomorphism and two chart images φ p₀, φ q₀ are joined inside φ.target ∩ T (for some T : Set Y) with p₀, q₀ ∈ φ.source, then p₀ and q₀ themselves are joined inside φ.source ∩ φ ⁻¹' T. The path is the chart-pullback φ.symm ∘ γ of any chart-side path; correctness of the target set uses the standard identity φ.symm '' (φ.target ∩ T) = φ.source ∩ φ ⁻¹' T.

theorem joinedIn_symm_image_of_target
    (φ : _root_.OpenPartialHomeomorph X Y) (T : Set Y) {p₀ q₀ : X}
    (hp : p₀ ∈ φ.source) (hq : q₀ ∈ φ.source)
    (hjoin : JoinedIn (φ.target ∩ T) (φ p₀) (φ q₀)) :
    JoinedIn (φ.source ∩ φ ⁻¹' T) p₀ q₀

chart_local_detour_of_pathConnected_complement

Chart-local detour, finite obstruction. If φ : X → Y is an open partial homeomorphism, C : Set X is finite, and the chart-image complement φ.target \ φ '' (φ.source ∩ C) is path-connected, then any two points p, q ∈ φ.source with p ∉ C, q ∉ C are joined inside Cᶜ ∩ φ.source (i.e. by a path entirely in φ.source avoiding C).

theorem chart_local_detour_of_pathConnected_complement
    (φ : _root_.OpenPartialHomeomorph X Y) {C : Set X} (_hC_fin : C.Finite)
    (hPC : IsPathConnected (φ.target \ φ '' (φ.source ∩ C)))
    {p q : X} (hp : p ∈ φ.source) (hq : q ∈ φ.source)
    (hp_notin : p ∉ C) (hq_notin : q ∉ C) :
    JoinedIn (Cᶜ ∩ φ.source : Set X) p q