English
There exists a plausible characterization of Spec as IsGermInjective in terms of prime spectrum and localizations.
Русский
Существует характеристика Spec через IsGermInjective в терминах PrimeSpectrum и локализаций.
LaTeX
$$$\text{Spec IsGermInjective}$$$
Lean4
protected theorem Spec
(H : ∀ I : Ideal R, I.IsPrime → ∃ f : R, f ∉ I ∧ ∀ (x y : R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0) :
(Spec R).IsGermInjective := by
refine fun p ↦ ⟨?_⟩
obtain ⟨f, hf, H⟩ := H p.asIdeal p.2
refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
· rw [← basicOpen_eq_of_affine]
exact (isAffineOpen_top (Spec R)).basicOpen _
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
intro x hx
obtain ⟨x, s, rfl⟩ :=
IsLocalization.mk'_surjective (S := ((Spec.structureSheaf R).val.obj (.op <| PrimeSpectrum.basicOpen f)))
(.powers f) x
rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem, RingHom.mem_ker,
RingHom.algebraMap_toAlgebra] at hx
swap;
·
exact
@isUnit_of_invertible _ _ _
(@IsLocalization.invertible_mk'_one ..)
-- There is an `Opposite.unop (Opposite.op _)` in `hx` which doesn't seem removable using
-- `simp`/`rw`.
erw [StructureSheaf.germ_toOpen] at hx
obtain ⟨⟨y, hy⟩, hy'⟩ :=
(IsLocalization.map_eq_zero_iff p.asIdeal.primeCompl ((Spec.structureSheaf R).presheaf.stalk p) _).mp hx
obtain ⟨n, hn⟩ := H x y hy' hy
refine (@IsLocalization.mk'_eq_zero_iff ..).mpr ?_
exact ⟨⟨_, n, rfl⟩, hn⟩
