English
The vanishing ideal data assigns to a closed subset Z the largest ideal sheaf whose zero locus contains Z.
Русский
Данные vanishingIdeal сопоставляют закрытому подмножеству Z наибольший идеальный слой, чья нулевая локус содержит Z.
LaTeX
$$vanishingIdeal : Closeds X.carrier.carrier → IdealSheafData X$$
Lean4
/-- The vanishing ideal sheaf of a closed set,
which is the largest ideal sheaf whose support is equal to it.
The reduced induced scheme structure on the closed set is the quotient of this ideal. -/
@[simps! ideal coe_support]
nonrec def vanishingIdeal (Z : Closeds X) : IdealSheafData X :=
mkOfMemSupportIff (fun U ↦ vanishingIdeal (U.2.fromSpec.base ⁻¹' Z))
(fun U f ↦ by
let F := X.presheaf.map (homOfLE (X.basicOpen_le f)).op
apply le_antisymm
· rw [Ideal.map_le_iff_le_comap]
intro x hx
suffices ∀ p, (X.affineBasicOpen f).2.fromSpec.base p ∈ Z → F.hom x ∈ p.asIdeal by
simpa [PrimeSpectrum.mem_vanishingIdeal] using this
intro x hxZ
refine (PrimeSpectrum.mem_vanishingIdeal _ _).mp hx ((Spec.map (X.presheaf.map (homOfLE _).op)).base x) ?_
rwa [Set.mem_preimage, ← Scheme.comp_base_apply, IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]
· letI : Algebra Γ(X, U) Γ(X, X.affineBasicOpen f) := F.hom.toAlgebra
have : IsLocalization.Away f Γ(X, X.basicOpen f) := U.2.isLocalization_of_eq_basicOpen _ _ rfl
intro x hx
dsimp only at hx ⊢
have : Topology.IsOpenEmbedding (Spec.map F).base := localization_away_isOpenEmbedding Γ(X, X.basicOpen f) f
rw [← U.2.map_fromSpec (X.affineBasicOpen f).2 (homOfLE (X.basicOpen_le f)).op, Scheme.comp_base,
TopCat.coe_comp, Set.preimage_comp] at hx
generalize U.2.fromSpec.base ⁻¹' Z = Z' at hx ⊢
replace hx : x ∈ vanishingIdeal ((Spec.map F).base ⁻¹' Z') := hx
obtain ⟨I, hI, e⟩ := (isClosed_iff_zeroLocus_radical_ideal _).mp (isClosed_closure (s := Z'))
rw [← vanishingIdeal_closure, ← this.isOpenMap.preimage_closure_eq_closure_preimage this.continuous, e] at hx
rw [← vanishingIdeal_closure, e]
erw [preimage_comap_zeroLocus] at hx
rwa [← PrimeSpectrum.zeroLocus_span, ← Ideal.map, vanishingIdeal_zeroLocus_eq_radical, ←
RingHom.algebraMap_toAlgebra (X.presheaf.map _).hom, ← IsLocalization.map_radical (.powers f), ←
vanishingIdeal_zeroLocus_eq_radical] at hx)
Z
(fun U x hxU ↦ by
trans x ∈ X.zeroLocus (U := U.1) (vanishingIdeal (U.2.fromSpec.base.hom ⁻¹' Z)) ∩ U.1
· rw [← U.2.fromSpec_image_zeroLocus, zeroLocus_vanishingIdeal_eq_closure, ←
U.2.fromSpec.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage U.2.fromSpec.base.1.2,
Set.image_preimage_eq_inter_range, Z.isClosed.closure_eq, IsAffineOpen.range_fromSpec]
simp [hxU]
· simp [hxU])
