English
UniversallyOpen is a Zariski-local property at the source.
Русский
Универсально открытое свойство локально по источнику.
LaTeX
$$$\IsZariskiLocalAtSource(\mathsf{UniversallyOpen}).$$$
Lean4
/-- Let `R` be a ring, and `f i` a finite collection of elements of `R` generating the unit ideal.
If the localization of `R` at each `f i` is Noetherian, so is `R`.
We follow the proof given in [Har77], Proposition II.3.2 -/
theorem isNoetherianRing_of_away : IsNoetherianRing R :=
by
apply monotone_stabilizes_iff_noetherian.mp
intro I
let floc s := algebraMap R (Away (M := R) s)
let suitableN s := {n : ℕ | ∀ m : ℕ, n ≤ m → (Ideal.map (floc s) (I n)) = (Ideal.map (floc s) (I m))}
let minN s := sInf (suitableN s)
have hSuit : ∀ s : S, minN s ∈ suitableN s := by
intro s
apply Nat.sInf_mem
let f : ℕ →o Ideal (Away (M := R) s) :=
⟨fun n ↦ Ideal.map (floc s) (I n), fun _ _ h ↦ Ideal.map_mono (I.monotone h)⟩
exact monotone_stabilizes_iff_noetherian.mpr (hN s) f
let N := Finset.sup S minN
use N
have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop
intro n hn
rw [IsLocalization.ideal_eq_iInf_comap_map_away hS (I N), IsLocalization.ideal_eq_iInf_comap_map_away hS (I n),
iInf_subtype', iInf_subtype']
apply iInf_congr
intro s
congr 1
rw [← hSuit s N (hN s)]
exact hSuit s n <| Nat.le_trans (hN s) hn
