isOpenMap_over — Mathlib

English

Let S be a scheme and n any type. The projection from affine n-space over S to S induces an open map on underlying topological spaces.

Русский

Пусть S — схема, а n — множества. Проекция пространства аффинного n-размера над S на S образует открытое отображение на основе топологий.

LaTeX

$$$IsOpenMap\big(\mathbb{A}(n;S) \downarrow S\xrightarrow{\ base} S\big)$$$

Lean4

theorem isOpenMap_over : IsOpenMap (𝔸(n; S) ↘ S).base :=
  by
  change topologically @IsOpenMap _
  wlog hS : ∃ R, S = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover (P := topologically @IsOpenMap) S.affineCover).mpr ?_
    intro i
    have := this (n := n) (S.affineCover.X i) ⟨_, rfl⟩
    rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this
  obtain ⟨R, rfl⟩ := hS
  rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap) (SpecIso n R).inv, SpecIso_inv_over]
  exact MvPolynomial.isOpenMap_comap_C

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