quasiCompact_of_isIso — Mathlib

English

If f is an isomorphism of schemes, then f is quasi-compact.

Русский

Если f — изоморфизм схем, то он квази-компактен.

LaTeX

$$$[IsIso f] \Rightarrow QuasiCompact(f)$$$

Lean4

instance (priority := 900) quasiCompact_of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : QuasiCompact f :=
  by
  constructor
  intro U _ hU'
  convert hU'.image (inv f.base).hom.continuous_toFun using 1
  rw [Set.image_eq_preimage_of_inverse]
  · delta Function.LeftInverse
    exact IsIso.inv_hom_id_apply f.base
  · exact IsIso.hom_inv_id_apply f.base

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