English
An element s lies in an ideal I of Γ(X,U) if and only if its germs map into I at every point x ∈ U via the germ maps.
Русский
Элемент s принадлежит идеалу I в Γ(X,U) тогда и только тогда, когда его ях Germs отображаются в I на каждой точке x ∈ U через гёрм-отображения.
LaTeX
$$$s\in I \iff \forall x\in X,\forall h\in U, X.presheaf.germ U x h s \in I.map( X.presheaf.germ U x h).hom$$$
Lean4
theorem mem_ideal_iff {s : Γ(X, U)} {I : Ideal Γ(X, U)} :
s ∈ I ↔ ∀ (x : X) (h : x ∈ U), X.presheaf.germ U x h s ∈ I.map (X.presheaf.germ U x h).hom :=
by
refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩
letI (x : _) : Algebra Γ(X, U) (X.presheaf.stalk (hU.fromSpec.base x)) :=
TopCat.Presheaf.algebra_section_stalk X.presheaf _
have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv.base _).2
refine
Submodule.mem_of_localization_maximal (fun P hP ↦ X.presheaf.stalk (hU.fromSpec.base ⟨P, hP.isPrime⟩))
(fun P hP ↦ Algebra.linearMap _ _) _ _ ?_
intro P hP
rw [Ideal.localized₀_eq_restrictScalars_map]
exact H _ _
