English
A locally Noetherian scheme remains locally Noetherian after open immersion; in particular, an open immersion from X to Y with Y locally Noetherian implies X is locally Noetherian.
Русский
Локально Ноетерова схема сохраняет локальную Ноetherianность при открытом вложении; в частности, если есть открытое вложение X↪Y и Y локально Ноетерова, то X тоже локально Ноетерова.
LaTeX
$$$[\text{IsOpenImmersion}(f)] \land [\text{IsLocallyNoetherian}(Y)] \Rightarrow \text{IsLocallyNoetherian}(X).$$$
Lean4
theorem isLocallyNoetherian_of_isOpenImmersion {Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] [IsLocallyNoetherian Y] :
IsLocallyNoetherian X := by
refine ⟨fun U => ?_⟩
let V : Y.affineOpens := ⟨f ''ᵁ U, IsAffineOpen.image_of_isOpenImmersion U.prop _⟩
suffices Γ(X, U) ≅ Γ(Y, V) by
convert isNoetherianRing_of_ringEquiv (R := Γ(Y, V)) _
· apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
exact this.symm
· exact IsLocallyNoetherian.component_noetherian V
rw [← Scheme.Hom.preimage_image_eq f U]
trans
· apply IsOpenImmersion.ΓIso
· suffices Scheme.Hom.opensRange f ⊓ V = V by rw [this]
rw [← Opens.coe_inj]
rw [Opens.coe_inf, Scheme.Hom.coe_opensRange, IsOpenMap.coe_functor_obj, Set.inter_eq_right, Set.image_subset_iff,
Set.preimage_range]
exact Set.subset_univ _
