Documentation

Hironaka.Algebra.Proj.BaseChange

Base change of projective space: ℙ^{r-1}_S = Spec S ×_{Spec R} ℙ^{r-1}_R #

For a ring map R → S and the polynomial ring R[u_0, …, u_{r-1}] with its standard grading, the square

Proj S[u] ⟶ Spec S
   |           |
Proj R[u] ⟶ Spec R

with Proj S[u] ⟶ Proj R[u] Mathlib's Proj.map of the coefficient map and the vertical maps Proj.toSpecZero followed by Spec of R → (R[u])₀, is cartesian [TSPA, Tag 01MX]. Mathlib does not provide this; it is the input for identifying the exceptional divisor of a smooth blow-up with a projective bundle over the centre.

Why it holds. Both Proj R[u] and its base change are covered by the standard charts D₊(u_j), and Proj.map respects them (Proj.awayι_comp_map); over D₊(u_j) the square is Spec of the ring square R → S, R → (R[u]_{u_j})₀, S → (S[u]_{u_j})₀, (R[u]_{u_j})₀ → (S[u]_{u_j})₀, which is a pushout because both charts are polynomial rings in the u_i/u_j (AlgebraicGeometry.Proj.isPushout_away, by dehomogenization). A square of schemes that is cartesian over an open cover of one corner is cartesian (Mathlib's Scheme.isPullback_of_openCover).

Main declarations #

source
noncomputable def AlgebraicGeometry.Proj.projToSpec (σ : Type) (R : Type u) [CommRing R] :
Proj (MvPolynomial.homogeneousSubmodule σ R) ⟶ Spec ↧R

The structure morphism ℙ_R = Proj R[u] ⟶ Spec R: Proj.toSpecZero followed by Spec of the constants R → (R[u])₀.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AlgebraicGeometry.Proj.irrelevant_le_span_range_X (σ : Type) (R : Type u) [CommRing R] :
    (HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule σ R)).toIdeal ≤ Ideal.span (Set.range MvPolynomial.X)

    The irrelevant ideal of R[u] is generated by the variables.

    source
    theorem AlgebraicGeometry.Proj.awayι_projToSpec (σ : Type) (R : Type u) [CommRing R] (f : MvPolynomial σ R) (hf : f ∈ MvPolynomial.homogeneousSubmodule σ R 1) :
    CategoryTheory.CategoryStruct.comp (awayι (MvPolynomial.homogeneousSubmodule σ R) f hf ⋯) (projToSpec σ R) = Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) f)))

    The standard chart Spec (R[u]_{u_j})₀ ⟶ ℙ_R followed by the structure morphism is Spec of R → (R[u]_{u_j})₀.

    source
    noncomputable def AlgebraicGeometry.Proj.standardCover (σ : Type) (R : Type u) [CommRing R] :
    (Proj (MvPolynomial.homogeneousSubmodule σ R)).AffineOpenCover

    The affine open cover of ℙ_R by the standard charts D₊(u_j).

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Proj.irrelevant_le_map_gradedMap (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
      HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule σ S) ≤ HomogeneousIdeal.map (gradedMap R S) (HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule σ R))

      The hypothesis of Proj.map: the irrelevant ideal of S[u] is generated by the images of the variables of R[u].

      source
      noncomputable def AlgebraicGeometry.Proj.projMap (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
      Proj (MvPolynomial.homogeneousSubmodule σ S) ⟶ Proj (MvPolynomial.homogeneousSubmodule σ R)

      Proj of the coefficient map: ℙ_S ⟶ ℙ_R.

      Equations
      Instances For
        source
        theorem AlgebraicGeometry.Proj.projMap_projToSpec (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
        CategoryTheory.CategoryStruct.comp (projMap σ R S) (projToSpec σ R) = CategoryTheory.CategoryStruct.comp (projToSpec σ S) (Spec.map (CommRingCat.ofHom (algebraMap R S)))

        The base-change square commutes.

        source
        theorem AlgebraicGeometry.Proj.isPullback_awayι_projMap (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (j : σ) :
        CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map (gradedMap R S) (MvPolynomial.X j)))) (awayι (MvPolynomial.homogeneousSubmodule σ S) ((gradedMap R S) (MvPolynomial.X j)) ⋯ ⋯) (awayι (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j) ⋯ ⋯) (projMap σ R S)

        The chart square of ℙ_S ⟶ ℙ_R over D₊(u_j).

        source
        theorem AlgebraicGeometry.Proj.isPullback_Spec_away (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (j : σ) :
        CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (algebraMap S (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ S) ((gradedMap R S) (MvPolynomial.X j)))))) (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map (gradedMap R S) (MvPolynomial.X j)))) (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R (HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j)))))

        Over the chart D₊(u_j) the base-change square is Spec of the pushout of rings AlgebraicGeometry.Proj.isPushout_away.

        source
        theorem AlgebraicGeometry.Proj.isPullback_projMap_aux (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] (j : σ) {W' : Scheme} {a : W' ⟶ Proj (MvPolynomial.homogeneousSubmodule σ S)} {b : W' ⟶ Spec ↧(HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j))} (hab : CategoryTheory.IsPullback a b (projMap σ R S) (awayι (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j) ⋯ ⋯)) :
        CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp a (projToSpec σ S)) b (Spec.map (CommRingCat.ofHom (algebraMap R S))) (CategoryTheory.CategoryStruct.comp (awayι (MvPolynomial.homogeneousSubmodule σ R) (MvPolynomial.X j) ⋯ ⋯) (projToSpec σ R))

        The base-change square over the chart D₊(u_j): any pullback of ℙ_S ⟶ ℙ_R along the chart, composed with the structure map, is a pullback of Spec S ⟶ Spec R along the chart's structure map — the square isPullback_Spec_away transported along the identification of the two pullbacks of the chart square.

        source
        theorem AlgebraicGeometry.Proj.isPullback_projMap (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
        CategoryTheory.IsPullback (projToSpec σ S) (projMap σ R S) (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)

        Base change of projective space [TSPA, Tag 01MX], for R[u_0, …, u_{r-1}]: the square ℙ_S ⟶ Spec S, ℙ_S ⟶ ℙ_R, Spec S ⟶ Spec R, ℙ_R ⟶ Spec R is cartesian. It is cartesian over each standard chart D₊(u_j) of ℙ_R (isPullback_projMap_aux at the canonical pullback), hence cartesian (Mathlib's Scheme.isPullback_of_openCover).

        source
        noncomputable def AlgebraicGeometry.Proj.projBaseChangeIso (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
        Proj (MvPolynomial.homogeneousSubmodule σ S) ≅ CategoryTheory.Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)

        ℙ_S ≅ Spec S ×_{Spec R} ℙ_R, compatibly with the projections (projBaseChangeIso_hom_fst, projBaseChangeIso_hom_snd).

        Equations
        Instances For
          source
          @[simp]
          theorem AlgebraicGeometry.Proj.projBaseChangeIso_hom_fst (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
          CategoryTheory.CategoryStruct.comp (projBaseChangeIso σ R S).hom (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)) = projToSpec σ S
          source
          @[simp]
          theorem AlgebraicGeometry.Proj.projBaseChangeIso_hom_fst_assoc (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] {Z : Scheme} (h : Spec ↧S ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (projBaseChangeIso σ R S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)) h) = CategoryTheory.CategoryStruct.comp (projToSpec σ S) h
          source
          @[simp]
          theorem AlgebraicGeometry.Proj.projBaseChangeIso_hom_snd (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] :
          CategoryTheory.CategoryStruct.comp (projBaseChangeIso σ R S).hom (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)) = projMap σ R S
          source
          @[simp]
          theorem AlgebraicGeometry.Proj.projBaseChangeIso_hom_snd_assoc (σ : Type) (R : Type u) [CommRing R] (S : Type u) [CommRing S] [Algebra R S] {Z : Scheme} (h : Proj (MvPolynomial.homogeneousSubmodule σ R) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (projBaseChangeIso σ R S).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (projToSpec σ R)) h) = CategoryTheory.CategoryStruct.comp (projMap σ R S) h