English
If f and g ∈ R[X] with g monic, then there exists a finite set t ⊆ R such that a specific image-comap relation holds between zero loci of g and f, analogous to a finite description of the image of Z(I) ∩ D(f).
Русский
Пусть f, g ∈ R[X] и g монический. Тогда существует конечный набор t ⊆ R, так что изображение-комап зависимость между нулевыми локусами g и f выполняется, описывая конечное представление образа Z(I) ∩ D(f).
LaTeX
$$$\\exists t: \\mathrm{Finset}\\ R,\\; \\mathrm{comap}\\ C '' (Z(g) \\setminus Z(f)) = (Z(t))^c$$$
Lean4
/-- Let `A` be an `R`-algebra. If `A ⧸ I` is finite free over `R`,
then the image of `Z(I) ∩ D(f) ⊆ Spec S` in `Spec R` is compact open. -/
theorem exists_image_comap_of_finite_of_free (f : A) (s : Set A) [Module.Finite R (A ⧸ Ideal.span s)]
[Module.Free R (A ⧸ Ideal.span s)] :
∃ t : Finset R, comap (algebraMap R A) '' (zeroLocus s \ zeroLocus { f }) = (zeroLocus t)ᶜ := by
classical
use
(Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
(Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
ext x
rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
isNilpotent_tensor_residueField_iff]
simp [Set.subset_def]
