The glued blow-up of an affine scheme is the affine blow-up

The blow-up blowUp I is glued from the affine blow-ups affineBlowUp (I.ideal U) over the affine opens U of X [TSPA, Tag 01OF], the component blowUp.ι I U being an open immersion with image π⁻¹(U). For X = Spec R and U = ⊤ the component is therefore an isomorphism onto the whole blow-up, and its source affineBlowUp (I.ideal ⊤) is the affine blow-up of J itself through the ring isomorphism R ≅ Γ(Spec R, ⊤) (affineBlowUp.mapOfEq). This module packages the composite as blowUpSpecIso J : blowUp (specIdealSheaf J) ≅ affineBlowUp J, over Spec R (blowUpSpecIso_hom_π), together with the transport of inverse images along it — the identification through which the charts of the blow-up of an affine scheme (such as the charts of B_0 𝔸⁴ in Kollár's worked example [Kol07, Example 106]) are read off the affine blow-up [TSPA, Tag 0804]; [Hau14, Theorem 4.19].

@[reducible, inline]

noncomputable abbrev Hironaka.BlowUp.topAffineOpen {R : Type u} [CommRing R] : ↑(AlgebraicGeometry.Spec ↧R).affineOpens

⊤ as an affine open of Spec R.

Equations

• Hironaka.BlowUp.topAffineOpen = ⟨⊤, ⋯⟩

theorem Hironaka.BlowUp.ΓSpecIso_inv_hom_comp_hom_hom {R : Type u} [CommRing R] : (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).hom) = RingHom.id ↑((AlgebraicGeometry.Spec ↧R).presheaf.obj (Opposite.op ⊤))

Γ(Spec R, ⊤) → R → Γ(Spec R, ⊤) is the identity (the two halves of ΓSpecIso).

theorem Hironaka.BlowUp.ΓSpecIso_hom_hom_comp_inv_hom {R : Type u} [CommRing R] : (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).hom).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) = RingHom.id R

R → Γ(Spec R, ⊤) → R is the identity.

theorem Hironaka.BlowUp.map_eq_ideal_topAffineOpen {R : Type u} [CommRing R] (J : Ideal R) : Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) J = (AlgebraicGeometry.specIdealSheaf J).ideal topAffineOpen

The sections of specIdealSheaf J over ⊤ are the image of J in Γ(Spec R, ⊤).

theorem Hironaka.BlowUp.ideal_topAffineOpen_map_eq {R : Type u} [CommRing R] (J : Ideal R) : Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).hom) ((AlgebraicGeometry.specIdealSheaf J).ideal topAffineOpen) = J

The image of those sections back in R is J.

instance Hironaka.BlowUp.isIso_ι_topAffineOpen {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.IdealSheafData.blowUp.ι (AlgebraicGeometry.specIdealSheaf J) topAffineOpen)

Over X = Spec R the component ι ⊤ of the gluing is an isomorphism — an open immersion whose image π⁻¹(⊤) is everything [TSPA, Tag 0804].

noncomputable def Hironaka.BlowUp.blowUpSpecIso {R : Type u} [CommRing R] (J : Ideal R) : (AlgebraicGeometry.specIdealSheaf J).blowUp ≅ AlgebraicGeometry.affineBlowUp J

The glued blow-up of Spec R along the ideal sheaf of J is the affine blow-up of J [TSPA, Tags 01OF and 0804]: the inverse of the component ι ⊤ followed by the affine blow-up's functoriality along R ≅ Γ(Spec R, ⊤).

Equations

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

theorem Hironaka.BlowUp.Spec_map_ΓSpecIso_inv_eq_isoSpec_inv {R : Type u} [CommRing R] : AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv = (AlgebraicGeometry.Spec ↧R).isoSpec.inv

Spec of ΓSpecIso⁻¹ is the inverse of the canonical Spec R ≅ Spec Γ(Spec R, ⊤).

theorem Hironaka.BlowUp.blowUpSpecIso_hom_π {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.CategoryStruct.comp (blowUpSpecIso J).hom (AlgebraicGeometry.affineBlowUp.π J) = (AlgebraicGeometry.specIdealSheaf J).blowUpπ

The identification lies over Spec R.

theorem Hironaka.BlowUp.blowUpSpecIso_inv_π {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.CategoryStruct.comp (blowUpSpecIso J).inv (AlgebraicGeometry.specIdealSheaf J).blowUpπ = AlgebraicGeometry.affineBlowUp.π J

The inverse identification lies over Spec R.

theorem Hironaka.BlowUp.comap_comap_blowUpSpecIso_inv {R : Type u} [CommRing R] (J : Ideal R) (K : (AlgebraicGeometry.Spec ↧R).IdealSheafData) : (K.comap (AlgebraicGeometry.specIdealSheaf J).blowUpπ).comap (blowUpSpecIso J).inv = K.comap (AlgebraicGeometry.affineBlowUp.π J)

Inverse images of ideal sheaves of Spec R along the blow-up, transported to the affine blow-up.