A lift lands in the chart of every stalk generator

Let f : Y ⟶ Spec R be admissible for I (the inverse image ideal sheaf I·𝒪_Y is invertible), g : Y ⟶ B = affineBlowUp I a lift of f (g ≫ π = f), y ∈ Y, and a ∈ I an element whose image generates the stalk (I·𝒪_Y)_y. Then g y lies in the chart of a.

This is the step that makes the local patches of Hauser's proof agree on overlaps [Hau14, Theorem 4.18, proof (a) and (c)] and that the last sentences of [TSPA, Tag 0806] rely on, made explicit; it is what fails without admissibility: the inclusion of the origin into 𝔸² is not admissible for the ideal (x, y), and its lifts to the blow-up of the origin are the points of the exceptional line.

The argument. The point g y lies in the chart of some b, where the exceptional ideal has stalk (b) (the criterion affineBlowUp.mem_chart_iff) and a = b · u with u the transport of a/b (affineBlowUp.exists_factor_of_mem_chart). Pulling back along the local homomorphism g♯_y : 𝒪_{B, g y} → 𝒪_{Y, y}: the stalk (I·𝒪_Y)_y is the image of the stalk of the exceptional ideal (stalkIdeal_comap), so it is (f♯b); by hypothesis it is (f♯a); and by admissibility it is generated by a nonzerodivisor, so f♯b is a nonzerodivisor (mem_nonZeroDivisors_of_span_eq_span). From f♯a = f♯b · g♯u and (f♯a) = (f♯b), cancellation (isUnit_of_span_mul_eq_span) makes g♯u a unit; a local homomorphism reflects units (isUnit_map_iff), so u is a unit at g y, and g y lies in the chart of a.

theorem AlgebraicGeometry.stalkIdeal_comap_of_comp_π {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (g : Y ⟶ affineBlowUp I) (hg : CategoryTheory.CategoryStruct.comp g (affineBlowUp.π I) = f) (y : ↥Y) : ((specIdealSheaf I).comap f).stalkIdeal y = Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap g y)) ((affineBlowUp.exceptionalIdeal I).stalkIdeal (g y))

For a lift g of f, the stalk of I·𝒪_Y at y is the image of the stalk of the exceptional ideal at g y under the stalk map of g.

theorem AlgebraicGeometry.stalkMap_comp_π_germ {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (g : Y ⟶ affineBlowUp I) (hg : CategoryTheory.CategoryStruct.comp g (affineBlowUp.π I) = f) (y : ↥Y) (r : R) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap g y)) ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap (affineBlowUp.π I) (g y))) ((CategoryTheory.ConcreteCategory.hom ((Spec ↧R).presheaf.germ ⊤ ((affineBlowUp.π I) (g y)) ⋯)) ((CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) r))) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f y)) ((CategoryTheory.ConcreteCategory.hom ((Spec ↧R).presheaf.germ ⊤ (f y) ⋯)) ((CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) r))

The image of r ∈ R in 𝒪_{Y, y} under a lift g of f factors through 𝒪_{B, g y}.

theorem AlgebraicGeometry.affineBlowUp.mem_chart_of_generates {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) (g : Y ⟶ affineBlowUp I) (hg : CategoryTheory.CategoryStruct.comp g (π I) = f) (y : ↥Y) (a : ↥I) (ha : ((specIdealSheaf I).comap f).stalkIdeal y = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f y)) ((CategoryTheory.ConcreteCategory.hom ((Spec ↧R).presheaf.germ ⊤ (f y) ⋯)) ((CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) ↑a))}) : g y ∈ Scheme.Hom.opensRange (chart I a)

A lift lands in the chart of every stalk generator: a lift g of an admissible f : Y ⟶ Spec R sends y into the chart of every a ∈ I whose image generates the stalk of I·𝒪_Y at y. The step behind the agreement of the local patches in [Hau14, Theorem 4.18, proof (a)]; not stated there in this form.