6.10. MappingDegree.ChartOverlapPropagationDischarge🔗

Jacobians.MappingDegree.ChartOverlapPropagationDischarge — source

locallyConstLocus

The locally-constant locus of a map f : X → Y at a value y₀: the set of points x such that f is eventually equal to y₀ near x.

def locallyConstLocus {X : Type u} [TopologicalSpace X] {Y : Type v}
    (f : X → Y) (y₀ : Y) : Set X

isOpen_locallyConstLocus

The locally-constant locus is open: by definition, every point of the locus admits a neighborhood on which f ≡ y₀, and that neighborhood is contained in the locus.

lemma isOpen_locallyConstLocus {X : Type u} [TopologicalSpace X] {Y : Type v}
    (f : X → Y) (y₀ : Y) : IsOpen (locallyConstLocus f y₀)

locallyConstLocus_apply

A point of the locally-constant locus indeed has f x = y₀. This uses Filter.Eventually.self_of_nhds.

lemma locallyConstLocus_apply {X : Type u} [TopologicalSpace X] {Y : Type v}
    {f : X → Y} {y₀ : Y} {x : X} (hx : x ∈ locallyConstLocus f y₀) :
    f x = y₀

mem_locallyConstLocus_of_isOpen

Membership criterion via an open set: if V is open, contains x, and f ≡ y₀ on V, then x ∈ locallyConstLocus f y₀.

lemma mem_locallyConstLocus_of_isOpen {X : Type u} [TopologicalSpace X] {Y : Type v}
    {f : X → Y} {y₀ : Y} {V : Set X} (hV : IsOpen V) {x : X} (hx : x ∈ V)
    (hconst : ∀ x' ∈ V, f x' = y₀) :
    x ∈ locallyConstLocus f y₀

ClopennessOfLocallyConstHypothesis

Clopen-ness of the locally-constant locus. For every C^ω map f : X → Y and every y₀ : Y, the locally-constant locus {x | ∀ᶠ x' in 𝓝 x, f x' = y₀} is closed.

Combined with the open-ness lemma above, this is the residual analytic-continuation content deferred by the path-walking argument: along a path γ : [0,1] → X from any boundary point of the locus, finitely many overlapping charts let one chain AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq to extend the local constancy across the boundary, contradicting boundary-ness.

Isolating only the closedness as a hypothesis lets the connected-clopen step (open-ness + nonempty + connectedness ⇒ universe) be derived in plain topology without invoking analyticity.

def ClopennessOfLocallyConstHypothesis
    (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (Y : Type v) [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] : Prop

chartOverlapPropagation_of_clopennessOfLocallyConst

Discharge of ChartOverlapPropagationHypothesis from ClopennessOfLocallyConstHypothesis. The locally-constant locus is open by definition, closed by the residual hypothesis, contains x₀ (via the open V-witness), so by connectedness of X it is all of X. Hence f x = y₀ for every x : X.

theorem chartOverlapPropagation_of_clopennessOfLocallyConst
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (H : ClopennessOfLocallyConstHypothesis X Y) :
    ChartOverlapPropagationHypothesis X Y

chartPullbackNotEventuallyConst_of_clopennessOfLocallyConst

Chart-pullback non-eventual-constancy from clopen-ness of the locally-constant locus.

theorem chartPullbackNotEventuallyConst_of_clopennessOfLocallyConst
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (H : ClopennessOfLocallyConstHypothesis X Y) :
    ChartPullbackNotEventuallyConstHypothesis X Y

fibres_finite_statement_holds_of_clopennessOfLocallyConst

Finite fibres from clopen-ness of the locally-constant locus.

theorem fibres_finite_statement_holds_of_clopennessOfLocallyConst
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (H : ClopennessOfLocallyConstHypothesis X Y) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
        ∀ y : Y, (f ⁻¹' {y}).Finite