instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion

English

Any open immersion Z → X with X locally Noetherian is quasi-compact.

Русский

Любое открытое вложение Z→X, где X локально Ноетерова, является квази-компактным.

LaTeX

$$$[\text{IsOpenImmersion}(f)] \land [\text{IsLocallyNoetherian}(X)] \Rightarrow \text{QuasiCompact}(f).$$$

Lean4

/-- Any open immersion `Z ⟶ X` with `X` locally Noetherian is quasi-compact. -/
@[stacks 01OX]
instance (priority := 100) {Z : Scheme} [IsLocallyNoetherian X] {f : Z ⟶ X} [IsOpenImmersion f] : QuasiCompact f :=
  by
  apply (quasiCompact_iff_forall_affine f).mpr
  intro U hU
  rw [Opens.map_coe, ← Set.preimage_inter_range]
  apply f.isOpenEmbedding.isInducing.isCompact_preimage'
  · apply (noetherianSpace_set_iff _).mp
    · convert noetherianSpace_of_isAffineOpen U hU
      apply IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
    · exact Set.inter_subset_left
  · exact Set.inter_subset_right

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