Adaptedness of a chart: Z ∩ U = g⁻¹(L) from the stalk

Let Z be an ideal sheaf on X, x ∈ X, v_0, …, v_{n-1} sections of an affine open V ∋ x with coordinate morphism g = toAffineSpace f U v : U ⟶ 𝔸ⁿ_k, and L = V(t_0, …, t_{r-1}) ⊆ 𝔸ⁿ_k the coordinate subspace. The main theorem, exists_comap_eq_comap_coordinateSubspace, is the local statement behind Kollár's "Z = (z_{j_1} = ⋯ = z_{j_s} = 0) in some open neighborhood of x" [Kol07, Definition 24, (4)]: if the stalk Z_x is generated by the germs of v_0, …, v_{r-1}, then on a basic open U = D(s) ∋ x of V the ideal sheaf Z ∩ U is the pullback g⁻¹(L). Not stated as such in the sources; the argument:

• exists_mem_map_eq_map_of_localization: two finitely generated ideals of S with the same localization at a prime 𝔭 agree after localizing away from one s ∉ 𝔭 (each generator of one has a multiple in the other; take the product of the multipliers). Applied to Z(V) and (v_0, …, v_{r-1}), whose localizations at x agree by hypothesis (Z_x = Z(V)·𝒪_{X,x}), this gives Z(U) = (v_0, …, v_{r-1}) Γ(U) on U = D(s) (Z(U) = Z(V) Γ(U) is Mathlib's IdealSheafData.map_ideal).
• The two ideal sheaves on U are then compared stalk by stalk (ext_stalkIdeal): at u ∈ U both stalks are generated by the germs of the v_i, i < r; for Z ∩ U because Z(U) is, for g⁻¹(L) because the stalk of L at g(u) is generated by the t_i and g^*(t_i) = v_i (toAffineSpace_appTop_X).

This is the adaptedness clause of EtaleCoordinatesAdapted (EtaleCoordinatesDefs.lean), which Hironaka/Scheme/Smooth/EtaleCoordinatesAdapted.lean establishes at the closed points of a smooth center.

theorem AlgebraicGeometry.exists_mem_mul_mem_of_algebraMap_mem_map {S T : Type u} [CommRing S] [CommRing T] [Algebra S T] (M : Submonoid S) [IsLocalization M T] (Q : Ideal S) {a : S} (ha : (algebraMap S T) a ∈ Ideal.map (algebraMap S T) Q) : ∃ s ∈ M, s * a ∈ Q

If a lies in Q after localizing at M, some multiple s * a, s ∈ M, lies in Q.

theorem AlgebraicGeometry.exists_mem_map_eq_map_of_localization {S T : Type u} [CommRing S] [CommRing T] [Algebra S T] (M : Submonoid S) [IsLocalization M T] (I Q : Ideal S) (hI : I.FG) (hQ : Q.FG) (h : Ideal.map (algebraMap S T) I = Ideal.map (algebraMap S T) Q) : ∃ s ∈ M, ∀ (S' : Type u) [inst : CommRing S'] [inst_1 : Algebra S S'] [IsLocalization.Away s S'], Ideal.map (algebraMap S S') I = Ideal.map (algebraMap S S') Q

Finitely generated ideals with the same localization at M agree after localizing away from a single element s ∈ M.

theorem AlgebraicGeometry.toAffineSpace_appTop_X {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} (U : X.Opens) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (toAffineSpace f U v))) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial (Fin n) k)).inv) (MvPolynomial.X i)) = (CategoryTheory.ConcreteCategory.hom U.topIso.inv) (v i)

The coordinate morphism pulls the coordinate function t_i of 𝔸ⁿ_k back to v i.

theorem AlgebraicGeometry.toAffineSpace_app_top_X {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} (U : X.Opens) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) (i : Fin n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (toAffineSpace f U v) ⊤)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial (Fin n) k)).inv) (MvPolynomial.X i)) = (CategoryTheory.ConcreteCategory.hom U.topIso.inv) (v i)

toAffineSpace_appTop_X with app ⊤ in place of appTop (the form produced by Scheme.Hom.germ_stalkMap_apply).

theorem AlgebraicGeometry.stalkIdeal_coordinateSubspace {k : Type u} [Field k] {n : ℕ} (r : ℕ) (y : ↥(Spec ↧(MvPolynomial (Fin n) k))) : (coordinateSubspace k n r).stalkIdeal y = Ideal.span ((fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom ((Spec ↧(MvPolynomial (Fin n) k)).presheaf.germ ⊤ y ⋯)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial (Fin n) k)).inv) (MvPolynomial.X i))) '' {i : Fin n | ↑i < r})

The stalk of the coordinate subspace L = V(t_0, …, t_{r-1}) at a point of 𝔸ⁿ_k is generated by the germs of t_0, …, t_{r-1}.

theorem AlgebraicGeometry.exists_comap_eq_comap_coordinateSubspace {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) {x : ↥X} (V : ↑X.affineOpens) (hxV : x ∈ ↑V) (v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑V))) (hZ : Z.stalkIdeal x = Ideal.span ((fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑V) x hxV)) (v i)) '' {i : Fin n | ↑i < r})) : ∃ (U : ↑X.affineOpens) (_ : x ∈ ↑U) (hUV : ↑U ≤ ↑V), Z.comap (↑U).ι = (coordinateSubspace k n r).comap (toAffineSpace f ↑U fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hUV).op)) (v i))

If the stalk of Z at x is generated by the germs of the first r coordinates v_0, …, v_{r-1} (sections of an affine open V ∋ x), then on a smaller affine open U ∋ x the ideal sheaf Z ∩ U is the pullback of the coordinate subspace V(t_0, …, t_{r-1}) under the coordinate morphism U ⟶ 𝔸ⁿ_k: the local form of [Kol07, Definition 24, (4)].