isLocallyNoetherian_iff_of_affine_openCover

English

A scheme is locally Noetherian if its open cover by affine opens has Noetherian local sections on each piece.

Русский

Схема локально Ноетерова, если каждая часть афинного открытия имеет Ноетериновские секции глобальных функций.

LaTeX

$$$\text{IsLocallyNoetherian}(X) \iff \forall i, \text{IsNoetherianRing}(\Gamma(X, (\mathcal{U}.X_i)\top)).$$$

Lean4

/-- A version of `isLocallyNoetherian_iff_of_iSup_eq_top` using `Scheme.OpenCover`. -/
theorem isLocallyNoetherian_iff_of_affine_openCover (𝒰 : Scheme.OpenCover.{v, u} X) [∀ i, IsAffine (𝒰.X i)] :
    IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing Γ(𝒰.X i, ⊤) :=
  by
  constructor
  · intro h i
    let U := Scheme.Hom.opensRange (𝒰.f i)
    have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩
    apply isNoetherianRing_of_ringEquiv (R := Γ(X, U))
    apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
    exact (IsOpenImmersion.ΓIsoTop (𝒰.f i)).symm
  · intro hCNoeth
    let fS i : X.affineOpens := ⟨Scheme.Hom.opensRange (𝒰.f i), isAffineOpen_opensRange _⟩
    apply isLocallyNoetherian_of_affine_cover (S := fS)
    · rw [← Scheme.OpenCover.iSup_opensRange 𝒰]
    intro i
    apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.X i, ⊤))
    apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
    exact IsOpenImmersion.ΓIsoTop (𝒰.f i)

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