English
If X is compact and f: X → Y with Y affine has appTop injective, then f is dominant.
Русский
Если X компактно, а f: X → Y на аффинной Y инъективен на глобальных секциях, то f доминантен.
LaTeX
$$$[CompactSpace X] \\Rightarrow (\\text{Injective}(f.appTop) \\Rightarrow IsDominant f)$$$
Lean4
/-- If `f : X ⟶ Y` is a morphism of schemes with quasi-compact source and affine target,
`f` induces an injection on global sections, then `f` is dominant. -/
theorem isDominant_of_of_appTop_injective [CompactSpace X] (hfinj : Function.Injective (f.appTop)) : IsDominant f :=
by
have : QuasiCompact f := HasAffineProperty.iff_of_isAffine.mpr ‹_›
have : f.ker = ⊥ :=
Scheme.IdealSheafData.ext_of_isAffine
(by simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot])
exact
⟨by
simpa only [Scheme.Hom.support_ker, Scheme.IdealSheafData.support_bot, Closeds.coe_top,
← dense_iff_closure_eq] using (congr((↑($this).support : Set Y)) :)⟩
