Documentation

Hironaka.Scheme.BlowUp.AffineBlowUp.Universal.Existence

Existence of the lift: the universal property of the affine blow-up #

An admissible f : Y ⟶ Spec R — one along which I becomes invertible — lifts uniquely to the affine blow-up [Hau14, Theorem 4.18 (a)]; [TSPA, Tag 0806]: the affine blow-up is final among the schemes over Spec R on which I becomes invertible [Hau14, Definition 4.4].

Existence: exists_affineOpen_generator covers Y by affine opens V_y ∋ y on each of which I·Γ(Y, V_y) is generated by the nonzerodivisor f♯a_y, so liftOn f V_y a_y gives local lifts over f; on an overlap V_y ∩ V_{y'} (an open subscheme of Y, admissible by isInvertible_comap_comp_of_isOpenImmersion, and not necessarily affine) the two local lifts agree by the uniqueness theorem affineBlowUp.hom_ext, so they glue (Scheme.OpenCover.glueMorphisms) to lift f hf : Y ⟶ affineBlowUp I with lift f hf ≫ π = f. Uniqueness is affineBlowUp.hom_ext; together, existsUnique_lift.

source
theorem AlgebraicGeometry.isInvertible_comap_comp_of_isOpenImmersion {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) {Z : Scheme} (j : Z ⟶ Y) [IsOpenImmersion j] :
((specIdealSheaf I).comap (CategoryTheory.CategoryStruct.comp j f)).IsInvertible

Admissibility restricts along open immersions: if f : Y ⟶ Spec R is admissible for I, so is j ≫ f for every open immersion j : Z ⟶ Y.

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

Existence [Hau14, Theorem 4.18 (a)]; [TSPA, Tag 0806]: an admissible f : Y ⟶ Spec R lifts to the affine blow-up.

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

The universal property of the affine blow-up [Hau14, Definition 4.4 and Theorem 4.18]; [TSPA, Tag 0806]: an admissible f : Y ⟶ Spec R has exactly one lift.

source
noncomputable def AlgebraicGeometry.affineBlowUp.lift {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) :
Y ⟶ affineBlowUp I

The lift of an admissible f : Y ⟶ Spec R to the affine blow-up.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.affineBlowUp.lift_π {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) :
    CategoryTheory.CategoryStruct.comp (lift I f hf) (π I) = f
    source
    @[simp]
    theorem AlgebraicGeometry.affineBlowUp.lift_π_assoc {R : Type u} [CommRing R] (I : Ideal R) {Y : Scheme} (f : Y ⟶ Spec ↧R) (hf : ((specIdealSheaf I).comap f).IsInvertible) {Z : Scheme} (h : Spec ↧R ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (lift I f hf) (CategoryTheory.CategoryStruct.comp (π I) h) = CategoryTheory.CategoryStruct.comp f h
    source
    theorem AlgebraicGeometry.affineBlowUp.eq_lift {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) :
    g = lift I f hf

    Any lift is the lift.