instIsDominantToImageOfQuasiCompact

English

If f is quasi-compact, then f.toImage is dominant; the image is dense in Y.

Русский

Если f квазикомпактен, то f.toImage является доминантным; образ плотен в Y.

LaTeX

$$$\text{IsDominant}(f.toImage)$, при [QuasiCompact f]$$

Lean4

instance [QuasiCompact f] : IsDominant f.toImage where
  denseRange := by
    rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image, ← Set.univ_subset_iff, ←
      Set.image_subset_iff, Set.image_univ, IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp, ←
      TopCat.coe_comp, ← Scheme.comp_base, f.toImage_imageι]

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