English
If f: X → Y is an open immersion and X,Y are irreducible, then the image of the generic point of X under f.base equals the generic point of Y.
Русский
Если f: X → Y является открытым погружением и X, Y непрерывны, то образ общего точки X через f.base равен общей точке Y.
LaTeX
$$$f.\mathrm{base}(\text{genericPoint}(X))=\text{genericPoint}(Y).$$$
Lean4
theorem genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] [hX : IrreducibleSpace X]
[IrreducibleSpace Y] : f.base (genericPoint X) = genericPoint Y :=
by
apply ((genericPoint_spec Y).eq _).symm
convert (genericPoint_spec X).image (show Continuous f.base by fun_prop)
symm
rw [← Set.univ_subset_iff]
convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.isOpen_range _
· rw [Set.univ_inter, Set.image_univ]
· apply PreirreducibleSpace.isPreirreducible_univ (X := Y)
· exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
