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