6.27. MappingDegree.FibresFiniteAssembly🔗

Jacobians.MappingDegree.FibresFiniteAssembly — source

ConnectivityGlobalizationHypothesis

def ConnectivityGlobalizationHypothesis
    (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

fibres_finite_of_connectivity_hypothesis

Full assembly: fibres_finite_statement from the connectivity- globalization hypothesis. Given ConnectivityGlobalizationHypothesis X Y, the classical statement fibres_finite_statement X Y holds.

theorem fibres_finite_of_connectivity_hypothesis
    {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 : ConnectivityGlobalizationHypothesis X Y) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
        ∀ y : Y, (f ⁻¹' {y}).Finite

fibres_finite_statement_holds_of_connectivity

Conditional discharge. fibres_finite_statement X Y holds whenever the connectivity-globalization hypothesis holds. Equivalent to fibres_finite_of_connectivity_hypothesis but stated as a one-line implication for ergonomic downstream use.

theorem fibres_finite_statement_holds_of_connectivity
    {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] :
    ConnectivityGlobalizationHypothesis X Y →
      ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
        ¬ Jacobians.Discharge.IsConstantMap f →
          ∀ y : Y, (f ⁻¹' {y}).Finite