isProperMap_iff_isClosedMap_filter

English

A map f is proper if and only if it is continuous and the induced map on X × Filter X → Y × Filter X is closed.

Русский

Отображение пропорно тогда и только тогда, когда оно непрерывно и отображение на $X\\times\\mathcal{F}X\\to Y\\times\\mathcal{F}X$ замкнуто.

LaTeX

$$$IsProperMap(f) \\iff (Continuous(f) \\land IsClosedMap(Prod.map(f, id) : X \\times Filter X \\to Y \\times Filter X))$$$

Lean4

/-- A map `f : X → Y` is proper if and only if it is continuous and the map
`(Prod.map f id : X × Filter X → Y × Filter X)` is closed. This is stronger than
`isProperMap_iff_universally_closed` since it shows that there's only one space to check to get
properness, but in most cases it doesn't matter. -/
theorem isProperMap_iff_isClosedMap_filter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} : IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id : X × Filter X → Y × Filter X) :=
  by
  constructor <;> intro H
  · exact ⟨H.continuous, H.universally_closed _⟩
  · rw [isProperMap_iff_ultrafilter]
      -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.

    refine
      ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
        -- In `X × Filter X`, consider the closed set `F := closure {(x, ℱ) | ℱ = pure x}`

    let F : Set (X × Filter X) :=
      closure
        {xℱ | xℱ.2 = pure xℱ.1}
          -- Since `f × id` is closed, the set `(f × id) '' F` is also closed.

    have := H.2 F isClosed_closure
    have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
      -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
        -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
        -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
        -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
        -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.
      this.mem_of_tendsto (hy.prodMk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
          -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.

    rcases this with
      ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
        -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
          -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is a ultrafilter,
          -- it is enough to show that `Uᶜ` is not in `𝒰`.

    refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
    rw [mem_closure_iff_nhds] at hx
    rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOf_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
    exact hz' hz

Похожие утверждения