6.21. MappingDegree.CriticalValuesFiniteGeneral🔗

Jacobians.MappingDegree.CriticalValuesFiniteGeneral — source

criticalSetGeneral

General critical set of f : X → Y. Topological proxy for "fails to be a local biholomorphism": the points where f is not locally injective. For a non-constant analytic map between complex 1-manifolds, this coincides with the classical chart-pullback-derivative-vanishing notion via the local branched-cover normal form.

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

criticalValuesGeneral

General critical values of f : X → Y.

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

regularSetGeneral

General regular set. Points where f is locally injective. By construction the complement of criticalSetGeneral f.

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

regularSetGeneral_eq_compl_criticalSetGeneral

The general regular set is the set-theoretic complement of the general critical set.

lemma regularSetGeneral_eq_compl_criticalSetGeneral
    {X : Type u} {Y : Type v} (f : X → Y)
    [TopologicalSpace X] :
    regularSetGeneral f = (criticalSetGeneral f)ᶜ

criticalSetGeneral_eq_compl_regularSetGeneral

The general critical set is the set-theoretic complement of the general regular set.

lemma criticalSetGeneral_eq_compl_regularSetGeneral
    {X : Type u} {Y : Type v} (f : X → Y)
    [TopologicalSpace X] :
    criticalSetGeneral f = (regularSetGeneral f)ᶜ

isOpen_regularSetGeneral

The general regular set is open: any neighbourhood U witnessing local injectivity at x can be shrunk to an open V ⊆ U with x ∈ V, on which InjOn f V (restriction of InjOn f U), and V is a neighbourhood of every one of its points.

theorem isOpen_regularSetGeneral
    {X : Type u} {Y : Type v} (f : X → Y)
    [TopologicalSpace X] :
    IsOpen (regularSetGeneral f)

isClosed_criticalSetGeneral

The general critical set is closed.

theorem isClosed_criticalSetGeneral
    {X : Type u} {Y : Type v} (f : X → Y)
    [TopologicalSpace X] :
    IsClosed (criticalSetGeneral f)

criticalChartPullbackData_general

Per-point chart-pullback data (general).

For (f : X → Y) (hf : ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ) ω f) non-constant, at every x : X, build a CriticalChartPullbackData f (criticalSetGeneral f) x whose F' is the derivative of the literal chart pullback of f through chartAt ℂ x and chartAt ℂ (f x).

noncomputable def criticalChartPullbackData_general
    {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 : ¬ Jacobians.Discharge.IsConstantMap f)
    (x : X) :
    Jacobians.Discharge.ContMDiff.Degree.CriticalChartPullbackData
      f (criticalSetGeneral f) x

criticalSet_finite_general

CV-Gen headline. Critical set is finite for any non-constant analytic f : X → Y between two compact connected charted spaces over ℂ.

theorem criticalSet_finite_general
    {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 : ¬ Jacobians.Discharge.IsConstantMap f) :
    (criticalSetGeneral f).Finite

criticalValues_finite_general

CV-Gen corollary. Critical values are finite under the same hypotheses.

theorem criticalValues_finite_general
    {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 : ¬ Jacobians.Discharge.IsConstantMap f) :
    (criticalValuesGeneral f).Finite