English
If X is locally Noetherian, then X is germ-injective.
Русский
Если X локально ноetherian, то X germ-injective.
LaTeX
$$$[\text{IsLocallyNoetherian } X] \Rightarrow X.IsGermInjective$$$
Lean4
instance (priority := 100) [IsLocallyNoetherian X] : X.IsGermInjective :=
by
suffices ∀ (R : CommRingCat.{u}) (_ : IsNoetherianRing R), (Spec R).IsGermInjective
by
refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
have := isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i)
infer_instance
refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_
let J := RingHom.ker <| algebraMap R (Localization.AtPrime I)
have hJ (x) : x ∈ J ↔ ∃ y : I.primeCompl, y * x = 0 := IsLocalization.map_eq_zero_iff I.primeCompl _ x
choose f hf using fun x ↦ (hJ x).mp
obtain ⟨s, hs⟩ := (isNoetherianRing_iff_ideal_fg R).mp ‹_› J
have hs' : (s : Set R) ⊆ J := hs ▸ Ideal.subset_span
refine ⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩
rw [pow_one, mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton]
refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)
rw [← hs, Ideal.span_le]
intro i hi
rw [SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, smul_eq_mul, mul_comm, ← smul_eq_mul, ←
Submodule.mem_annihilator_span_singleton, Submonoid.coe_finset_prod]
refine Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_
rw [Submodule.mem_annihilator_span_singleton, smul_eq_mul]
exact hf i _
