6.47. MappingDegree.RegularSubsetPreconnected🔗

Jacobians.MappingDegree.RegularSubsetPreconnected — source

isPreconnected_univ_subtype_of_isPreconnected_set_general

Subtype-preconnectedness from ambient preconnectedness. If S : Set Y is preconnected as an ambient set, then the universe of the subtype ↥S is preconnected. This is the literal shape consumed by fibre_card_eq_of_locallyConstant_subtype_reg.

lemma isPreconnected_univ_subtype_of_isPreconnected_set_general
    {Y : Type u} [TopologicalSpace Y]
    {S : Set Y} (h : IsPreconnected S) :
    IsPreconnected (Set.univ : Set S)

regularSubset_isPreconnected_subtype_of_compl

Subtype preconnectedness of Cᶜ, given ambient preconnectedness of Cᶜ. Bare wrapper around the subtype-from-ambient bridge, specialised to the complement form Cᶜ that is the literal output of Y \ f(criticalSet f).

theorem regularSubset_isPreconnected_subtype_of_compl
    {Y : Type u} [TopologicalSpace Y]
    (C : Set Y)
    (h_amb : IsPreconnected (Cᶜ : Set Y)) :
    IsPreconnected (Set.univ : Set ((Cᶜ : Set Y)))

regularSubset_isPreconnected_of_finite_complement_hypothesis

Headline structural theorem (parameterised on the topological hypothesis). Given that the complement of any finite set in Y is preconnected (the standard "connected complex 1-manifold minus finitely many points stays connected" fact), the regular subset (f(criticalSet f))ᶜ is preconnected as a subtype, in the exact form FibreCardOnRegularSubset consumes.

The hypothesis h_topo is the clean topological boundary: for compact connected complex 1-manifolds (equivalently real 2-manifolds), this is known classically; we name it here so the downstream consumer can compose against it without bringing the chart-by-chart construction into this file.

theorem regularSubset_isPreconnected_of_finite_complement_hypothesis
    {Y : Type u} [TopologicalSpace Y]
    (h_topo : ∀ C : Set Y, C.Finite → IsPreconnected (Cᶜ : Set Y))
    (C : Set Y) (hC_fin : C.Finite) :
    IsPreconnected (Set.univ : Set ((Cᶜ : Set Y)))