quasiCompact_over_affine_iff — Mathlib

English

Let f: X → Y be a morphism of schemes and assume that Y is affine. Then f is quasi-compact if and only if X is a compact topological space.

Русский

Пусть f: X → Y — морфизм схем и Y афинна. Тогда f квази-компактен тогда и только тогда, когда X компактен как топологическое пространство.

LaTeX

$$$[IsAffine\\ Y]\\;\\Longrightarrow\\; (\\QuasiCompact f \\iff \\CompactSpace X)$$$

Lean4

theorem quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] : QuasiCompact f ↔ CompactSpace X := by
  rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

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