A machine-checked solution to the Jacobians challenge

6.22. MappingDegree.Degree🔗

Jacobians.MappingDegree.Degree — source

RegularValueWitness

structure RegularValueWitness {X : Type u} {Y : Type v} (f : X → Y) where

RegularValueWitness.card

Cardinality of the chosen finite fibre, as a Finset.card.

def RegularValueWitness.card {X : Type u} {Y : Type v} {f : X → Y}
    (w : RegularValueWitness f) : ℕ

RegularValueWitness.card_eq_ncard

The witness card is the Set.ncard of its fibre.

lemma RegularValueWitness.card_eq_ncard {X : Type u} {Y : Type v} {f : X → Y}
    (w : RegularValueWitness f) : w.card = (f ⁻¹' {w.value}).ncard

RegularValueWitnessReg

A regular regular-value witness for f. Strengthens RegularValueWitness with a chart-pullback-derivative-nonzero certificate: for every preimage point x ∈ f ⁻¹' {value}, the derivative of the chart-pullback (chartAt ℂ value) ∘ f ∘ (chartAt ℂ x).symm at (chartAt ℂ x) x is nonzero.

This is the analytic content of "value is a regular value of f", inlined into the structure.

structure RegularValueWitnessReg
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (f : X → Y) where

card

Cardinality of the chosen finite fibre of a regular witness.

def card (w : RegularValueWitnessReg f) : ℕ

value

The chosen regular value.

def value (w : RegularValueWitnessReg f) : Y

fiber_finite

The fibre over the chosen regular value is finite.

def fiber_finite (w : RegularValueWitnessReg f) :
    (f ⁻¹' {w.toWitness.value}).Finite

RegularValueWitness.toRegular

Builder. Promote a plain RegularValueWitness to a regular one, given a chart-pullback-derivative-nonzero certificate at every preimage point.

def RegularValueWitness.toRegular
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y} (w : RegularValueWitness f)
    (h_reg : ∀ x ∈ f ⁻¹' {w.value},
      deriv ((chartAt ℂ w.value) ∘ f ∘ (chartAt ℂ x).symm)
        ((chartAt ℂ x) x) ≠ 0) :
    RegularValueWitnessReg f

degreeFiber

The degree of an analytic map f : X → Y between compact Riemann surfaces, as a fibre cardinality.

  • For constant f, returns 0 (matching the convention in challenge item 9 and degreeIndicator).

  • For non-constant f, returns the cardinality of *some* regular fibre, selected via Classical.choice on the existence of a RegularValueWitnessReg (a witness whose chosen value carries a chart-pullback-derivative-nonzero certificate at every preimage; this is the analytic content of "regular value"). If no such regular witness is classically available, falls back to 0.

The well-definedness — independence of the chosen witness — is the deep classical input that is not discharged here. See file docstring items (2)–(3) for what is deferred.

ZZ-RegFix correction. Earlier the Classical.choice was on Nonempty (RegularValueWitness f), which carries no regularity certificate; Classical.choice could pick a branch-point witness whose fibre cardinality is strictly smaller than the topological degree. Switching to RegularValueWitnessReg f bakes the analytic regularity in, so the choice is always at a regular value. Existence of a regular witness for non-constant analytic f is discharged unconditionally in Manifold/RegularValueExistsRegUnconditional.lean.

def degreeFiber {ω : WithTop ℕ∞}
    {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]
    (f : X → Y) (_hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) : ℕ

degreeFiber_eq_witness_card

When a *regular* regular-value witness *does* exist (non-constant case, Classical mode), the fibre-degree equals the cardinality of *some* such witness. The particular witness is Classical.choice-selected; independence of choice is the deep classical input. Because the choice is now over RegularValueWitnessReg f (whose is_regular is built in), the chosen witness is always at a regular value.

lemma degreeFiber_eq_witness_card {ω : WithTop ℕ∞}
    {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]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnc : ¬ IsConstantMap f) (h : Nonempty (RegularValueWitnessReg f)) :
    degreeFiber f hf = (Classical.choice h).card

fiber_finite_of_isDiscrete

A fibre of a continuous map into a T2 compact space is closed and hence compact; if additionally the fibre carries the discrete subspace topology, it is finite. This is the purely topological half of the identity-theorem argument.

lemma fiber_finite_of_isDiscrete
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf_cont : Continuous f) (y : Y)
    (h_disc : IsDiscrete (f ⁻¹' {y})) :
    (f ⁻¹' {y}).Finite

regular_value_exists_of_some_fiber_finite

Trivial reduction: a RegularValueWitness f is exactly an element of Y together with finiteness of its fibre. So existence is equivalent to ∃ y, (f ⁻¹' {y}).Finite.

lemma regular_value_exists_of_some_fiber_finite
    {X : Type u} {Y : Type v} {f : X → Y}
    (h : ∃ y : Y, (f ⁻¹' {y}).Finite) :
    Nonempty (RegularValueWitness f)

regular_value_exists_of_fibres_finite

Reduction of regular_value_exists_statement to fibres_finite_statement.

Given that *every* fibre is finite (the conclusion of fibres_finite_statement), and Y is non-empty (free from ConnectedSpace Y), pick any y : Y and package it as a witness.

lemma regular_value_exists_of_fibres_finite {ω : WithTop ℕ∞}
    {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_fib : ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f → ∀ y : Y, (f ⁻¹' {y}).Finite) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f → Nonempty (RegularValueWitness f)

FibreCardData

A fibre-cardinality function packaging the data classical covering-space theory provides. Recorded as a structure so downstream files have a single named target: discharging fibre_card_well_defined_statement reduces to producing one of these for every non-constant analytic f.

Fields:

  • card_of: the fibre-cardinality function on Y (or any superset of the regular-value set; we take all of Y for simplicity, since the value at a critical point is irrelevant for the witness-comparison argument).

  • card_of_witness: every RegularValueWitness w has card_of w.value = w.card. This is a definitional compatibility: it says card_of agrees with the true fibre cardinality at every point that *carries* a witness — exactly the points the well-definedness statement ranges over.

  • card_of_constant: card_of is constant when restricted to the witness values. This is the deep classical content (covering-space + connectedness of Y \ critical-values).

structure FibreCardData {X : Type u} {Y : Type v} (f : X → Y) where

fibre_card_eq_of_locallyConstant_subtype_reg

Sharper reduction (regular form): locally-constant fibre-cardinality on a preconnected subset. Same shape as the unrestricted fibre_card_eq_of_locallyConstant_subtype. The user supplies a regular- value subset R : Set Y and a proof h_supp that every regular witness's value lies in R.

lemma fibre_card_eq_of_locallyConstant_subtype_reg
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y}
    {R : Set Y}
    (card_of : Y → ℕ)
    (h_witness : ∀ w : RegularValueWitness f, card_of w.value = w.card)
    (h_supp : ∀ w : RegularValueWitnessReg f, w.toWitness.value ∈ R)
    (h_lc_sub : IsLocallyConstant (fun y : R => card_of y.val))
    (h_conn_sub : IsPreconnected (Set.univ : Set R))
    (w₁ w₂ : RegularValueWitnessReg f) :
    w₁.card = w₂.card