English
For a polynomial f ∈ R[X], x ∈ Spec(R) satisfies x ∈ comap C '' basicOpen f if and only if there exists an index i with f.coeff i not in x.asIdeal.
Русский
Для многочлена f ∈ R[X] и точки x ∈ Spec(R) выполняется: x ∈ comap C '' basicOpen f тогда и только тогда, когда существует индекс i с f.coeff i ∉ x.asIdeal.
LaTeX
$$$x \\in \\mathrm{comap}\\ C '' \\mathrm{basicOpen}(f) \\iff \\exists i, f.coeff i \\notin x.asIdeal$$$
Lean4
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A`. -/
theorem mem_image_comap_basicOpen (f : A) (x) :
x ∈ comap (algebraMap R A) '' basicOpen f ↔ ¬IsNilpotent (algebraMap A (A ⊗[R] x.asIdeal.ResidueField) f) :=
by
have e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ (Ideal.span ∅ : Ideal A)) ⊗[R] x.asIdeal.ResidueField :=
by
refine Algebra.TensorProduct.congr ?f AlgEquiv.refl
rw [Ideal.span_empty]
exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }
rw [← IsNilpotent.map_iff e.injective, AlgEquiv.commutes, ← mem_image_comap_zeroLocus_sdiff f ∅ x, zeroLocus_empty, ←
Set.compl_eq_univ_diff, basicOpen_eq_zeroLocus_compl]
