quasiSeparatedSpace — Mathlib

English

A locally Noetherian scheme is quasi-separated; explicit verification via affine opens.

Русский

Локально Ноетерова схема квазираздельна; проверка через афинные открытые покрытия.

LaTeX

$$$[\text{IsLocallyNoetherian}(X)] \Rightarrow \text{QuasiSeparatedSpace}(X).$$$

Lean4

/-- A locally Noetherian scheme is quasi-separated. -/
@[stacks 01OY]
instance (priority := 100) quasiSeparatedSpace [IsLocallyNoetherian X] : QuasiSeparatedSpace X :=
  by
  apply (quasiSeparatedSpace_iff_affine X).mpr
  intro U V
  have hInd := U.2.fromSpec.isOpenEmbedding.isInducing
  apply (hInd.isCompact_preimage_iff ?_).mp
  · rw [← Set.preimage_inter_range, IsAffineOpen.range_fromSpec, Set.inter_comm]
    apply hInd.isCompact_preimage'
    · apply (noetherianSpace_set_iff _).mp
      · convert noetherianSpace_of_isAffineOpen U.1 U.2
        apply IsLocallyNoetherian.component_noetherian
      · exact Set.inter_subset_left
    · rw [IsAffineOpen.range_fromSpec]
      exact Set.inter_subset_left
  · rw [IsAffineOpen.range_fromSpec]
    exact Set.inter_subset_left

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