Stalks along a coproduct of open immersions

The local cover g : X' → X of [Kol07, Theorem 105] (the globalization of blow-up sequences: the run of the order reduction BO_{n,1} is assembled from runs on the pieces of an open cover through the coproduct of the inclusions) is a coproduct of open immersions (openImmersionCoprods), so its stalk maps are isomorphisms, and so are those of its stage lifts along a blow-up sequence (base change, isPullback_pullbackStageHom). A stalkwise identity of pulled-back ideal sheaves descends along such a map (stalkIdeal_comap), and the reduced ideal of the closure of a point specializing to q agrees at q with the pullback of the reduced ideal of the closure of its image when that pullback's support has the point as a generic point (a minimal prime over a prime is that prime). Bookkeeping for the descent of the local form of the ideal along the local cover (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedClaimCover, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Cover).

theorem Hironaka.Resolution.openImmersionCoprods.isIso_stalkMap {X Y : AlgebraicGeometry.Scheme} {g : Y ⟶ X} (hg : AlgebraicGeometry.openImmersionCoprods g) (y : ↥Y) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap g y)

The stalk maps of a coproduct of open immersions are isomorphisms: at y = ι i u, the stalk map of the open immersion ι i ≫ g factors through that of the open immersion ι i.

theorem Hironaka.Resolution.openImmersionCoprods_pullbackStageHom {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {g : Y ⟶ X} (hg : AlgebraicGeometry.openImmersionCoprods g) (i : Fin (S.length + 1)) : AlgebraicGeometry.openImmersionCoprods (S.pullbackStageHom g i)

The stage lifts of a coproduct of open immersions along a blow-up sequence are coproducts of open immersions (the class is stable under base change, and the stage lifts are base changes).

theorem Hironaka.Resolution.stalkIdeal_eq_of_comap_eq_of_isIso_stalkMap {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) {A B : X.IdealSheafData} {q : ↥Y} [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap φ q)] (h : (A.comap φ).stalkIdeal q = (B.comap φ).stalkIdeal q) : A.stalkIdeal (φ q) = B.stalkIdeal (φ q)

A stalkwise identity of two pull-backs descends along a morphism whose stalk map at the point is an isomorphism.

theorem Hironaka.Resolution.isPrime_stalkIdeal_vanishingIdeal_closure {X : AlgebraicGeometry.Scheme} {η x : ↥X} (hηx : η ⤳ x) : ((AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x).IsPrime

The stalk of the reduced ideal of the closure of η at a point x it specializes to is prime: it is a minimal prime over itself (stalkIdeal_vanishingIdeal_mem_minimalPrimes).

theorem Hironaka.Resolution.stalkIdeal_comap_vanishingIdeal_closure_eq {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) {ζ q : ↥Y} (hζq : ζ ⤳ q) [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap φ q)] (hgen : ζ ∈ ((AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {φ ζ})).comap φ).support.genericPoints) : ((AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {φ ζ})).comap φ).stalkIdeal q = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {ζ})).stalkIdeal q

The stalk at q of the pull-back of the reduced ideal of closure {φ ζ} along φ with an isomorphic stalk map at q is the stalk of the reduced ideal of closure {ζ}, provided ζ is a generic point of the pull-back's support: the latter is a minimal prime over the former, which is prime (the image of a prime under an isomorphism).