of_forall_source_exists — Mathlib

English

If for every point there exists a source piece giving an open immersion, then f is an open immersion.

Русский

Если для каждого точки существует источник, дающий открытое вложение, то f есть открытое вложение.

LaTeX

$$$ (\forall x, \exists i, IsOpenImmersion(i \circ f)) \Rightarrow IsOpenImmersion f $$$

Lean4

theorem of_forall_source_exists (f : X ⟶ Y) (hf : Function.Injective f.base)
    (hX : ∀ x, ∃ (U : Scheme) (i : U ⟶ X) (_ : IsOpenImmersion i), x ∈ i.opensRange ∧ IsOpenImmersion (i ≫ f)) :
    IsOpenImmersion f := by
  choose U i _ hxi hi using hX
  let 𝒰 : X.OpenCover := ⟨⟨X, U, i⟩, ⟨by simpa using show ∀ x, ∃ j y, (i j).base y = x from (⟨_, hxi ·⟩), by simpa⟩⟩
  exact IsOpenImmersion.of_openCover_source f 𝒰 hf hi

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