Affine blow-ups and their gluing datum

For an ideal I of a commutative ring R, the blow-up of Spec R along the closed subscheme Spec (R/I) is Proj of the graded Rees algebra ⨁ₙ Iⁿ tⁿ, with the morphism to Spec R induced by the inclusion R → Rees(I) in degree zero [Hau14, Definition 4.7]; [TSPA, Tags 01OF and 0804], restricted to an affine base: affineBlowUp I and affineBlowUp.π I. The map π is Proj.toSpecZero followed by Spec.map of the degree-zero identification R ≅ (Rees I)₀ (reesAlgebra.gradingZeroEquiv), written as the hom of the corresponding isomorphism of CommRingCat so that Mathlib's instances see an isomorphism; Spec.map reverses the direction.

For φ : R → S with I S = J, the graded map Rees(I) → Rees(J) induces, through Mathlib's Proj.map, the morphism of affine blow-ups affineBlowUp.mapOfEq φ : affineBlowUp J ⟶ affineBlowUp I over Spec.map φ (the functoriality of Proj in the graded ring, [TSPA, Tags 01OF and 01LH]); affineBlowUp.mapHom is the same morphism for a morphism of CommRingCat. It is functorial, from Proj.map_id and Proj.map_comp, and lies over Spec.map φ, from Proj.map_toSpecZero and the degree-zero identifications R ≅ (Rees I)₀, S ≅ (Rees J)₀.

The blow-up of a scheme X along an ideal sheaf I is Proj_X (⨁ₙ Iⁿ), obtained by gluing the affine blow-ups Proj Rees(I(U)) over the affine opens U of X along the canonical isomorphisms π⁻¹(U) ≅ Proj Rees(I(U)); the relative gluing lemma [TSPA, Tag 01LH] performs this from a functor on the affine opens and pullback squares over the inclusions, in Mathlib's form Scheme.Cover.RelativeGluingData over the directed cover X.directedAffineCover of all affine opens. The functor is affineBlowUpFunctor I : U ↦ affineBlowUp (I.ideal U), with transition map for U ≤ V the morphism of affine blow-ups induced by the restriction Γ(X, V) → Γ(X, U), along which I(U) = I(V) Γ(U) (Mathlib's IdealSheafData.map_ideal); affineBlowUpNatTrans I has the components affineBlowUp.π ≫ U.isoSpec.inv : affineBlowUp (I.ideal U) ⟶ U. Given a proof h that its naturality squares are pullbacks, relativeGluingDataOf I h is the gluing datum and blowUpOf I h with blowUpOf.π I h the glued scheme over X.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineBlowUp {R : Type u} [CommRing R] (I : Ideal R) : Scheme

The affine blow-up of Spec R along I: Proj of the graded Rees algebra ⨁ₙ Iⁿ tⁿ [Hau14, Definition 4.7]; [TSPA, Tags 01OF and 0804]. An abbrev, so that Mathlib's instances on Proj (separatedness, the chart cover, …) apply to it directly.

Equations

• AlgebraicGeometry.affineBlowUp I = AlgebraicGeometry.Proj (reesAlgebra.grading I)

noncomputable def AlgebraicGeometry.affineBlowUp.π {R : Type u} [CommRing R] (I : Ideal R) : affineBlowUp I ⟶ Spec ↧R

The blow-up map π : affineBlowUp I ⟶ Spec R, induced by the natural ring homomorphism R → Rees(I) [Hau14, Definition 4.7]: Proj.toSpecZero followed by Spec of the degree-zero identification R ≅ (Rees I)₀.

Equations

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

noncomputable def AlgebraicGeometry.affineBlowUp.mapOfEq {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hJ : Ideal.map φ I = J) : affineBlowUp J ⟶ affineBlowUp I

The morphism of affine blow-ups affineBlowUp J ⟶ affineBlowUp I induced by φ : R →+* S with I.map φ = J: Proj.map of the graded map Rees(I) → Rees(J) [TSPA, Tag 01OF].

Equations

• AlgebraicGeometry.affineBlowUp.mapOfEq φ hJ = AlgebraicGeometry.Proj.map (reesAlgebra.mapOfLe φ ⋯) ⋯

theorem AlgebraicGeometry.affineBlowUp.mapOfEq_id {R : Type u} [CommRing R] (I : Ideal R) (hJ : Ideal.map (RingHom.id R) I = I) : mapOfEq (RingHom.id R) hJ = CategoryTheory.CategoryStruct.id (affineBlowUp I)

Functoriality, identity: the identity ring map induces the identity of the affine blow-up (from Proj.map_id).

theorem AlgebraicGeometry.affineBlowUp.mapOfEq_eq_id {R : Type u} [CommRing R] {φ : R →+* R} (hφ : φ = RingHom.id R) (I : Ideal R) (hJ : Ideal.map φ I = I) : mapOfEq φ hJ = CategoryTheory.CategoryStruct.id (affineBlowUp I)

theorem AlgebraicGeometry.affineBlowUp.mapOfEq_comp {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {I : Ideal R} {J : Ideal S} {K : Ideal T} (φ : R →+* S) (ψ : S →+* T) (hJ : Ideal.map φ I = J) (hK : Ideal.map ψ J = K) (hK' : Ideal.map (ψ.comp φ) I = K) : mapOfEq (ψ.comp φ) hK' = CategoryTheory.CategoryStruct.comp (mapOfEq ψ hK) (mapOfEq φ hJ)

Functoriality, composites (from Proj.map_comp).

theorem AlgebraicGeometry.affineBlowUp.mapOfEq_eq_comp {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {I : Ideal R} {J : Ideal S} {K : Ideal T} {φ : R →+* S} {ψ : S →+* T} {χ : R →+* T} (hχ : χ = ψ.comp φ) (hJ : Ideal.map φ I = J) (hK : Ideal.map ψ J = K) (hK' : Ideal.map χ I = K) : mapOfEq χ hK' = CategoryTheory.CategoryStruct.comp (mapOfEq ψ hK) (mapOfEq φ hJ)

theorem AlgebraicGeometry.affineBlowUp.mapOfEq_π {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hJ : Ideal.map φ I = J) : CategoryTheory.CategoryStruct.comp (mapOfEq φ hJ) (π I) = CategoryTheory.CategoryStruct.comp (π J) (Spec.map (CommRingCat.ofHom φ))

Over the base: mapOfEq φ lies over Spec.map φ — the blow-up map is induced by R → Rees(I) [Hau14, Definition 4.7], naturally in R; from Proj.map_toSpecZero and the degree-zero identifications reesAlgebra.gradingZeroEquiv.

The same morphisms for morphisms of CommRingCat

Applying affineBlowUp.mapOfEq to a restriction map Γ(X, V) ⟶ Γ(X, U) of a scheme through its underlying ring map makes Lean unify the ring instances on the carrier ↑Γ(X, U) obtained by two different routes, which unfolds the presheaf and times out; passing the rings as objects of CommRingCat avoids it. The gluing functor affineBlowUpFunctor below uses these forms.

noncomputable def AlgebraicGeometry.affineBlowUp.mapHom {R S : CommRingCat} {I : Ideal ↑R} {J : Ideal ↑S} (φ : R ⟶ S) (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = J) : affineBlowUp J ⟶ affineBlowUp I

affineBlowUp.mapOfEq for a morphism φ : R ⟶ S of CommRingCat.

Equations

• AlgebraicGeometry.affineBlowUp.mapHom φ hJ = AlgebraicGeometry.affineBlowUp.mapOfEq (CommRingCat.Hom.hom φ) hJ

theorem AlgebraicGeometry.affineBlowUp.mapHom_eq_id {R : CommRingCat} {φ : R ⟶ R} (hφ : φ = CategoryTheory.CategoryStruct.id R) (I : Ideal ↑R) (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = I) : mapHom φ hJ = CategoryTheory.CategoryStruct.id (affineBlowUp I)

theorem AlgebraicGeometry.affineBlowUp.mapHom_eq_comp {R S T : CommRingCat} {I : Ideal ↑R} {J : Ideal ↑S} {K : Ideal ↑T} {φ : R ⟶ S} {ψ : S ⟶ T} {χ : R ⟶ T} (hχ : χ = CategoryTheory.CategoryStruct.comp φ ψ) (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = J) (hK : Ideal.map (CommRingCat.Hom.hom ψ) J = K) (hK' : Ideal.map (CommRingCat.Hom.hom χ) I = K) : mapHom χ hK' = CategoryTheory.CategoryStruct.comp (mapHom ψ hK) (mapHom φ hJ)

theorem AlgebraicGeometry.affineBlowUp.mapHom_π {R S : CommRingCat} {I : Ideal ↑R} {J : Ideal ↑S} (φ : R ⟶ S) (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = J) : CategoryTheory.CategoryStruct.comp (mapHom φ hJ) (π I) = CategoryTheory.CategoryStruct.comp (π J) (Spec.map φ)

Over the base, for a morphism of CommRingCat: mapHom φ lies over Spec.map φ.

theorem AlgebraicGeometry.affineBlowUp.mapHom_π_assoc {R S : CommRingCat} {I : Ideal ↑R} {J : Ideal ↑S} (φ : R ⟶ S) (hJ : Ideal.map (CommRingCat.Hom.hom φ) I = J) {Z : Scheme} (h : Spec ↧↑R ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapHom φ hJ) (CategoryTheory.CategoryStruct.comp (π I) h) = CategoryTheory.CategoryStruct.comp (π J) (CategoryTheory.CategoryStruct.comp (Spec.map φ) h)

Over the base, for a morphism of CommRingCat: mapHom φ lies over Spec.map φ.

theorem AlgebraicGeometry.affineOpens_isAffineOpen {X : Scheme} (U : ↑X.affineOpens) : IsAffineOpen ↑U

The affineness of an affine open, as a term whose type is syntactically IsAffineOpen U.1 (the membership U.2 : U.1 ∈ X.affineOpens unfolds to it only at default transparency, which breaks the motives of rw).

noncomputable def AlgebraicGeometry.affineBlowUpFunctor {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.Functor (↑X.affineOpens) Scheme

The functor of affine blow-ups on the affine opens of X, U ↦ affineBlowUp (I.ideal U), with transition map for U ≤ V the morphism induced by the restriction Γ(X, V) → Γ(X, U), along which I(U) = I(V) Γ(U) (IdealSheafData.map_ideal) [TSPA, Tags 01OF and 01LH].

Equations

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

noncomputable def AlgebraicGeometry.affineBlowUpNatTrans {X : Scheme} (I : X.IdealSheafData) : affineBlowUpFunctor I ⟶ Scheme.Cover.functorOfLocallyDirected X.directedAffineCover

The structure maps affineBlowUp (I.ideal U) ⟶ U, π followed by U ≅ Spec Γ(X, U), as a natural transformation to the directed affine cover's diagram [TSPA, Tag 01LH].

Equations

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

noncomputable def AlgebraicGeometry.relativeGluingDataOf {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) : Scheme.Cover.RelativeGluingData X.directedAffineCover

The relative gluing datum of the affine blow-ups over the directed affine cover [TSPA, Tag 01LH], given the pullback squares h.

Equations

• AlgebraicGeometry.relativeGluingDataOf I h = { functor := AlgebraicGeometry.affineBlowUpFunctor I, natTrans := AlgebraicGeometry.affineBlowUpNatTrans I, equifibered := h }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.blowUpOf {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) : Scheme

The blow-up of X along I, glued from the affine blow-ups over the affine opens [TSPA, Tags 01OF and 01LH], given the pullback squares h.

Equations

• AlgebraicGeometry.blowUpOf I h = (AlgebraicGeometry.relativeGluingDataOf I h).glued

noncomputable def AlgebraicGeometry.blowUpOf.π {X : Scheme} (I : X.IdealSheafData) (h : CategoryTheory.NatTrans.Equifibered (affineBlowUpNatTrans I)) : blowUpOf I h ⟶ X

The blow-up map blowUpOf I h ⟶ X.

Equations

• AlgebraicGeometry.blowUpOf.π I h = (AlgebraicGeometry.relativeGluingDataOf I h).toBase