mem_image_comap_zeroLocus_sdiff — Mathlib

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 _))

Похожие утверждения