Admissible morphisms to Spec R and the local lifts to the affine blow-up

Vocabulary for the universal property of the affine blow-up B = affineBlowUp I of Spec R along I [Hau14, Definition 4.4 and Theorem 4.18]; [TSPA, Tag 0806]:

• specIdealSheaf I — the ideal sheaf of I on Spec R (the spelling ofIdealTop (I.map (ΓSpecIso R).inv.hom) used throughout Hironaka.BlowUp, as an abbrev). A morphism f : Y ⟶ Spec R is admissible for I when (specIdealSheaf I).comap f is invertible (IdealSheafData.IsInvertible), that is, when the inverse image of Z is an effective Cartier divisor on Y.
• sectionsHom f V : R →+* Γ(Y, V) — the ring map on sections induced by f over an open V (f♯ composed with ΓSpecIso), with ideal_comap_specIdealSheaf: the ideal of the inverse image sheaf on an affine V is I extended along it.
• liftOn f V a hβa hI : (V : Scheme) ⟶ affineBlowUp I — the local lift of Hauser's proof [Hau14, Theorem 4.18, proof (d)]: for an affine open V and a ∈ I such that (I·𝒪_Y)(V) is generated by the nonzerodivisor f♯a, the composite V ≅ Spec Γ(V) → Spec R[I/a] → affineBlowUp I through the ring map δ : R[I/a] → Γ(V) extending f♯ (affineBlowUpAlgebra.lift), which lies over f (liftOn_π).

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.specIdealSheaf {R : Type u} [CommRing R] (I : Ideal R) : (Spec ↧R).IdealSheafData

The ideal sheaf of I ⊆ R on Spec R (the global sections of Spec R are R through ΓSpecIso).

Equations

• AlgebraicGeometry.specIdealSheaf I = AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) I)

noncomputable def AlgebraicGeometry.sectionsHom {R : Type u} [CommRing R] {Y : Scheme} (f : Y ⟶ Spec ↧R) (V : Y.Opens) : R →+* ↑(Y.presheaf.obj (Opposite.op V))

The ring map R → Γ(Y, V) induced by f : Y ⟶ Spec R on the sections over an open V (f♯ on V ⊆ f⁻¹(Spec R), composed with R ≅ Γ(Spec R, ⊤)).

Equations

• AlgebraicGeometry.sectionsHom f V = (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ V ⋯)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)

theorem AlgebraicGeometry.specIdealSheaf_ideal_top {R : Type u} [CommRing R] (I : Ideal R) : (specIdealSheaf I).ideal ⟨⊤, ⋯⟩ = Ideal.map (CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) I

theorem AlgebraicGeometry.ideal_comap_specIdealSheaf {R : Type u} [CommRing R] {Y : Scheme} (I : Ideal R) (f : Y ⟶ Spec ↧R) (V : ↑Y.affineOpens) : ((specIdealSheaf I).comap f).ideal V = Ideal.map (sectionsHom f ↑V) I

The ideal of (I·𝒪_Y) on an affine open V ⊆ Y is the extension of I along sectionsHom f V.

noncomputable def AlgebraicGeometry.liftOn {R : Type u} [CommRing R] {Y : Scheme} (I : Ideal R) (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}) : ↑↑V ⟶ affineBlowUp I

The local lift on an affine piece [Hau14, Theorem 4.18, proof (d)]; [TSPA, Tag 0806]. For an affine open V ⊆ Y and a ∈ I whose image f♯a is a nonzerodivisor generating (I·𝒪_Y)(V), the ring map δ : R[I/a] → Γ(Y, V) extending f♯ (affineBlowUpAlgebra.lift) gives V ≅ Spec Γ(Y, V) ⟶ Spec R[I/a] ⟶ affineBlowUp I through the chart of a.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.liftOn_eq {R : Type u} [CommRing R] {Y : Scheme} (I : Ideal R) (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}) : liftOn I f V a hβa hI = CategoryTheory.CategoryStruct.comp (IsAffineOpen.isoSpec ⋯).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (affineBlowUpAlgebra.lift (sectionsHom f ↑V) ⋯ hβa hI))) (affineBlowUp.chart I a))

The local lift lands in the chart of a.

theorem AlgebraicGeometry.isoSpec_hom_specMap_sectionsHom {R : Type u} [CommRing R] {Y : Scheme} (f : Y ⟶ Spec ↧R) (V : ↑Y.affineOpens) : CategoryTheory.CategoryStruct.comp (IsAffineOpen.isoSpec ⋯).hom (Spec.map (CommRingCat.ofHom (sectionsHom f ↑V))) = CategoryTheory.CategoryStruct.comp (↑V).ι f

The morphism Spec Γ(Y, V) ⟶ Spec R induced by f is Spec of sectionsHom f V.

theorem AlgebraicGeometry.liftOn_π {R : Type u} [CommRing R] {Y : Scheme} (I : Ideal R) (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}) : CategoryTheory.CategoryStruct.comp (liftOn I f V a hβa hI) (affineBlowUp.π I) = CategoryTheory.CategoryStruct.comp (↑V).ι f

The local lift lies over f: liftOn ≫ π = V.ι ≫ f (from affineBlowUp.chart_π and affineBlowUpAlgebra.lift_comp_algebraMap).