English
Let A be an R-algebra and I an ideal generated by s ⊆ A. For x ∈ Spec(R), the image of Z(I) ∩ D(f) under the map is not contained in the nilradical; equivalently, f is not nilpotent on κ(p) ⊗ A/(I).
Русский
Пусть A — R-алгебра, I — идеал, порождённый s ⊆ A. Для p ∈ Spec(R) образ Z(I) ∩ D(f) не содержит нилрадикал; эквивалентно, f не нильпотент в κ(p) ⊗ A/(I).
LaTeX
$$$x \\in \\mathrm{comap}(\\mathrm{algebraMap}\\ R A)''(Z(I) \\cap D(f)) \\iff \\neg \\mathrm{IsNilpotent}(\\text{algebraMap}_A ((A/\\langle s\\rangle) \\otimes_R \\kappa(x)) f)$$$
Lean4
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `Z(I) ∩ D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A ⧸ I`. -/
theorem mem_image_comap_zeroLocus_sdiff (f : A) (s : Set A) (x) :
x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus { f }) ↔
¬IsNilpotent (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField) f) :=
by
constructor
· rintro ⟨q, ⟨hqg, hqf⟩, rfl⟩ H
simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf
have hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField) := by
rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
let F : (A ⧸ Ideal.span s) ⊗[R] (q.asIdeal.comap (algebraMap R A)).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A _) hs)
(Ideal.ResidueField.mapₐ _ _ rfl) fun _ _ ↦ .all _ _
have := H.map F
rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] at this
exact hqf this
· intro H
rw [← mem_nilradical, nilradical_eq_sInf, Ideal.mem_sInf] at H
simp only [Set.mem_setOf_eq, Algebra.TensorProduct.algebraMap_apply, Ideal.Quotient.algebraMap_eq, not_forall] at H
obtain ⟨q, hq, hfq⟩ := H
have : ∀ a ∈ s, Ideal.Quotient.mk (Ideal.span s) a ⊗ₜ[R] 1 ∈ q := fun a ha ↦ by
simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]
refine ⟨comap (algebraMap A _) ⟨q, hq⟩, ⟨by simpa [Set.subset_def], by simpa⟩, ?_⟩
rw [← comap_comp_apply, ← IsScalarTower.algebraMap_eq, ← Algebra.TensorProduct.includeRight.comp_algebraMap,
comap_comp_apply, Subsingleton.elim (α := PrimeSpectrum x.asIdeal.ResidueField) (comap _ _) ⊥]
ext a
exact congr(a ∈ $(Ideal.ker_algebraMap_residueField _))