Uniqueness of lifts to the affine blow-up

• affineBlowUp.hom_ext_chart [Hau14, Theorem 4.18, proof (d)] ("by construction, γ is unique with this property"): on an affine open V ⊆ Y on which f♯a is a nonzerodivisor generating I·Γ(Y, V), two morphisms V ⟶ Spec R[I/a] over V ⟶ Y ⟶ Spec R are equal — they are Spec of ring maps R[I/a] → Γ(Y, V) extending f♯, and such a map is unique (affineBlowUpAlgebra.lift_unique).
• affineBlowUp.hom_ext [Hau14, Theorem 4.18, proof (a)]; [TSPA, Tag 0806]: two lifts g, g' of an admissible f : Y ⟶ Spec R are equal, for every scheme Y. For y ∈ Y, exists_affineOpen_generator gives an affine V ∋ y and a ∈ I with (I·𝒪_Y)(V) = (f♯a), f♯a a nonzerodivisor; then a generates the stalk of I·𝒪_Y at every point of V, so by affineBlowUp.mem_chart_of_generates both g and g' map V into the chart of a, and their restrictions factor through the open immersion chart a as morphisms V ⟶ Spec R[I/a] over V ⟶ Spec R, equal by the first item. Conclude with Scheme.hom_ext_of_forall. The sources' argument (scheme-theoretic density of Y ∖ D and separatedness) is replaced by this chartwise one, which needs no reducedness of Y.

theorem AlgebraicGeometry.exists_affineOpen_generator {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) (y : ↥Y) : ∃ (V : ↑Y.affineOpens), y ∈ ↑V ∧ ∃ (a : ↥I), (sectionsHom f ↑V) ↑a ∈ nonZeroDivisors ↑(Y.presheaf.obj (Opposite.op ↑V)) ∧ Ideal.map (sectionsHom f ↑V) I = Ideal.span {(sectionsHom f ↑V) ↑a}

For f : Y ⟶ Spec R admissible for I and y ∈ Y, there are an affine open V ∋ y and a ∈ I such that f♯a = sectionsHom f V a is a nonzerodivisor of Γ(Y, V) generating I·Γ(Y, V) (exists_affineOpen_generator_of_isInvertible for the base Spec R).

theorem AlgebraicGeometry.stalkIdeal_comap_specIdealSheaf_eq_span {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (V : ↑Y.affineOpens) (a : ↥I) (hI : Ideal.map (sectionsHom f ↑V) I = Ideal.span {(sectionsHom f ↑V) ↑a}) {z : ↥Y} (hz : z ∈ ↑V) : ((specIdealSheaf I).comap f).stalkIdeal z = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f z)) ((CategoryTheory.ConcreteCategory.hom ((Spec ↧R).presheaf.germ ⊤ (f z) ⋯)) ((CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) ↑a))}

If f♯a generates I·Γ(Y, V), the image of a generates the stalk of I·𝒪_Y at every point of V.

theorem AlgebraicGeometry.affineBlowUp.hom_ext_chart {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (V : ↑Y.affineOpens) (a : ↥I) (hβa : (sectionsHom f ↑V) ↑a ∈ nonZeroDivisors ↑(Y.presheaf.obj (Opposite.op ↑V))) (hI : Ideal.map (sectionsHom f ↑V) I = Ideal.span {(sectionsHom f ↑V) ↑a}) (u u' : ↑↑V ⟶ Spec ↧↥(affineBlowUpAlgebra I ↑a)) (hu : CategoryTheory.CategoryStruct.comp u (Spec.map (CommRingCat.ofHom (algebraMap R ↥(affineBlowUpAlgebra I ↑a)))) = CategoryTheory.CategoryStruct.comp (↑V).ι f) (hu' : CategoryTheory.CategoryStruct.comp u' (Spec.map (CommRingCat.ofHom (algebraMap R ↥(affineBlowUpAlgebra I ↑a)))) = CategoryTheory.CategoryStruct.comp (↑V).ι f) : u = u'

Local uniqueness [Hau14, Theorem 4.18, proof (d)]: on an affine open V ⊆ Y on which f♯a is a nonzerodivisor generating I·Γ(Y, V), two morphisms V ⟶ Spec R[I/a] over V ⟶ Y ⟶ Spec R are equal (from affineBlowUpAlgebra.lift_unique).

theorem AlgebraicGeometry.affineBlowUp.hom_ext {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) (g g' : Y ⟶ affineBlowUp I) (e : CategoryTheory.CategoryStruct.comp g (π I) = f) (e' : CategoryTheory.CategoryStruct.comp g' (π I) = f) : g = g'

Uniqueness of the lift [Hau14, Theorem 4.18, proof (a) and (d)]; [TSPA, Tag 0806]: two lifts of an admissible f : Y ⟶ Spec R to the affine blow-up are equal, for every scheme Y.