A machine-checked solution to the Jacobians challenge

6.4. MappingDegree.AnalyticContinuationGlobalization🔗

Jacobians.MappingDegree.AnalyticContinuationGlobalization — source

eqOn_const_of_preconnected_of_eventuallyEq

Identity theorem against a constant. If F : ℂ → ℂ is analytic on a preconnected open set U and is eventually equal to c at some z₀ ∈ U, then F = c everywhere on U. This is mathlib's AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq against g := fun _ => c.

lemma eqOn_const_of_preconnected_of_eventuallyEq
    {F : ℂ → ℂ} {U : Set ℂ} {z₀ : ℂ} {c : ℂ}
    (hF : AnalyticOnNhd ℂ F U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U)
    (hev : ∀ᶠ z in 𝓝 z₀, F z = c) :
    EqOn F (fun _ => c) U

not_eventually_const_of_not_constOn

Contrapositive: not eventually constant from a witness of non-constancy. If F is analytic on a preconnected open set U, takes a value other than c at some point z₁ ∈ U, and z₀ ∈ U, then F is not eventually c at z₀.

lemma not_eventually_const_of_not_constOn
    {F : ℂ → ℂ} {U : Set ℂ} {z₀ z₁ : ℂ} {c : ℂ}
    (hF : AnalyticOnNhd ℂ F U) (hU : IsPreconnected U)
    (h₀ : z₀ ∈ U) (h₁ : z₁ ∈ U) (h_ne : F z₁ ≠ c) :
    ¬ ∀ᶠ z in 𝓝 z₀, F z = c

ChartNonConstWitness

Chart-pullback witness of non-constancy. Encapsulates the data needed to apply not_eventually_const_of_not_constOn to a chart pullback F of a map f : X → Y:

  • U : Set ℂ — preconnected open set (the chart domain in ℂ),

  • F : ℂ → ℂ — the chart pullback,

  • c : ℂ — the chart image of the target value y₀,

  • hFA — F is analytic on U,

  • hU_pc — U is preconnected,

  • z₁ ∈ U — a witness point inside the chart where the pullback differs from c.

z₁ plays the role of "non-constancy is observed inside this chart". The existence of such a z₁ is the in-chart version of ¬ IsConstantMap f.

structure ChartNonConstWitness where

FibreChartNonConstAssignment

Composition contract. A "chart non-constancy witness assignment" is a function that to every fibre point x ∈ f ⁻¹' {y₀} associates a chart non-constancy witness whose chart domain U contains the chart image of x. This is the precise local datum needed to satisfy ChartPullbackData.hFne.

structure FibreChartNonConstAssignment {X : Type u} [TopologicalSpace X]
    {Y : Type v} (f : X → Y) (y₀ : Y) where