Documentation

Hironaka.Scheme.BlowUp.CoordinateSubspace.Charts

The model blow-up: 𝔸ⁿ_A along the coordinate subspace L = V(x_0, …, x_{r-1}) #

The blow-up of W = 𝔸ⁿ along the coordinate subspace Z = V(x_j : j ∈ J) is glued from the affine charts U_j = 𝔸ⁿ, j ∈ J, along transition maps, with the blow-up map given on U_j by the x_j-chart Ο€_j : x_i ↦ x_i x_j (i ∈ J βˆ– {j}), x_i ↦ x_i otherwise [Hau14, Definition 4.12]; KollΓ‘r's chart (60.2) is the case j = r [Kol07, Definition 60]. Hauser prints the transition maps as x_i ↦ x_i/x_j (i ∈ J βˆ– {j, β„“}), x_j ↦ 1/x_β„“, x_β„“ ↦ x_j x_β„“, x_i ↦ x_i (i βˆ‰ J); for the direction used here, the coordinates of U_β„“ as functions on D(x_β„“) βŠ† U_j, the first line reads x_i ↦ x_i/x_β„“ (HironakaExamples.BlowUp.CoordinateSubspace.Transition verifies this form). Here the blow-up of Spec R along I is Mathlib's Proj of the Rees algebra (affineBlowUp I) with the charts Spec R[I/a] ⟢ affineBlowUp I; R = A[x_0, …, x_{n-1}], I = (x_0, …, x_{r-1}) (centerIdeal), and Hironaka.Scheme.BlowUp.Model identifies R[I/x_j] with the polynomial ring A[x] (the variable x_i, i < r, i β‰  j, standing for x_i/x_j). This module defines

and proves the chart formulas: modelChart_Ο€ (over the base the chart is Spec Ο€_j), iSup_opensRange_modelChart (the charts cover), modelChart_preimage_modelChart (inside U_j the chart U_β„“ is D(x_β„“)), modelTransition_X. The sibling modules prove the smoothness of the model blow-up, the exceptional divisor in a chart and its identification with β„™^{r-1}_L, and the gluing identity; the charts are used for the Γ©tale-local structure of blow-ups of smooth centres (Hironaka.Scheme.Smooth.ChartEtale) and in the worked examples (HironakaExamples.Sequence.Remark33Charts).

source
@[reducible, inline]
abbrev AlgebraicGeometry.CoordinateSubspace.center (n r : β„•) :
Set (Fin n)

The index set {0, …, r-1} of the coordinates cutting out the center L.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.centerIdeal (A : Type u) [CommRing A] (n r : β„•) :
    Ideal (MvPolynomial (Fin n) A)

    The ideal (x_0, …, x_{r-1}) of the coordinate subspace L βŠ† 𝔸ⁿ_A.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.CoordinateSubspace.X_mem_centerIdeal (A : Type u) [CommRing A] (n r : β„•) {j : Fin n} (hj : ↑j < r) :
      MvPolynomial.X j ∈ centerIdeal A n r
      source
      @[reducible, inline]
      noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.modelBlowUp (A : Type u) [CommRing A] (n r : β„•) :
      Scheme

      The model blow-up B_L 𝔸ⁿ_A [Hau14, Definition 4.12], the affine blow-up of Spec A[x_0, …, x_{n-1}] along (x_0, …, x_{r-1}).

      Equations
      Instances For
        source
        noncomputable def AlgebraicGeometry.CoordinateSubspace.chartRingIso (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) :
        ↧β†₯(affineBlowUpAlgebra (centerIdeal A n r) (MvPolynomial.X j)) β‰… ↧(MvPolynomial (Fin n) A)

        The identification A[x][L/x_j] ≃ A[x] of Hironaka.Scheme.BlowUp.Model (x_i ↦ x_i/x_j for i < r, i β‰  j) as an isomorphism of CommRingCat.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def AlgebraicGeometry.CoordinateSubspace.modelChart (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) (hj : ↑j < r) :
          Spec ↧(MvPolynomial (Fin n) A) ⟢ modelBlowUp A n r

          The x_j-chart U_j = 𝔸ⁿ of the model blow-up [Hau14, Definition 4.12]; [Kol07, Definition 60, (60.2)]: Spec A[x] ⟢ B_L 𝔸ⁿ_A, the chart of x_j of affineBlowUp composed with Spec of the identification A[x][L/x_j] ≃ A[x] (x_i, i < r, i β‰  j, standing for x_i/x_j).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance AlgebraicGeometry.CoordinateSubspace.isOpenImmersion_modelChart (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) (hj : ↑j < r) :
            IsOpenImmersion (modelChart A n r j hj)

            The chart U_j is an open immersion (Spec of an isomorphism followed by a chart of affineBlowUp). An instance, so that the images (modelChart …).opensRange of the charts are available.

            source
            noncomputable def AlgebraicGeometry.CoordinateSubspace.modelTransition (A : Type u) [CommRing A] (n r : β„•) (j β„“ : Fin n) :
            MvPolynomial (Fin n) A →ₐ[A] Localization.Away (MvPolynomial.X β„“)

            The transition map from the coordinates of the chart U_β„“ to the functions on the overlap D(x_β„“) βŠ† U_j [Hau14, Definition 4.12] (whose printed first line x_i ↦ x_i/x_j is the form for the opposite direction): x_i ↦ x_i/x_β„“ (i < r, i β‰  j, β„“), x_j ↦ 1/x_β„“, x_β„“ ↦ x_j x_β„“, x_i ↦ x_i (i β‰₯ r).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem AlgebraicGeometry.CoordinateSubspace.centerIdeal_le_comap_chartSubst (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) :
              centerIdeal A n r ≀ Ideal.comap (affineBlowUpAlgebra.chartSubst A (center n r) j).toRingHom (Ideal.span {MvPolynomial.X j})

              The chart map Ο€_j [Hau14, Definition 4.12] sends the centre ideal into (x_j): x_i ↦ x_i x_j for i < r, i β‰  j, and x_j ↦ x_j. (So the exceptional divisor of the chart maps to L.)

              The chart map and the cover #

              source
              theorem AlgebraicGeometry.CoordinateSubspace.chartSubst_X (A : Type u) [CommRing A] (n r : β„•) (j i : Fin n) :
              (affineBlowUpAlgebra.chartSubst A (center n r) j) (MvPolynomial.X i) = if ↑i < r ∧ i β‰  j then MvPolynomial.X i * MvPolynomial.X j else MvPolynomial.X i

              The chart map Ο€_j [Hau14, Definition 4.12] is x_i ↦ x_i x_j for i < r, i β‰  j, and x_i ↦ x_i otherwise.

              source
              theorem AlgebraicGeometry.CoordinateSubspace.chartRingIso_hom_comp_algebraMap (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) :
              (CommRingCat.Hom.hom (chartRingIso A n r j).hom).comp (algebraMap (MvPolynomial (Fin n) A) β†₯(affineBlowUpAlgebra (centerIdeal A n r) (MvPolynomial.X j))) = (affineBlowUpAlgebra.chartSubst A (center n r) j).toRingHom

              Read through chartRingIso: the identification A[x][L/x_j] ≃ A[x] composed with the inclusion A[x] β†’ A[x][L/x_j] is Hauser's chart map Ο€_j.

              source
              theorem AlgebraicGeometry.CoordinateSubspace.modelChart_Ο€ (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) (hj : ↑j < r) :
              CategoryTheory.CategoryStruct.comp (modelChart A n r j hj) (affineBlowUp.Ο€ (centerIdeal A n r)) = Spec.map (CommRingCat.ofHom (affineBlowUpAlgebra.chartSubst A (center n r) j).toRingHom)

              Over the base the chart U_j is Spec of the chart map Ο€_j [Hau14, Definition 4.12]; [Kol07, Definition 60, (60.2)].

              source
              theorem AlgebraicGeometry.CoordinateSubspace.opensRange_modelChart (A : Type u) [CommRing A] (n r : β„•) (j : Fin n) (hj : ↑j < r) :
              Scheme.Hom.opensRange (modelChart A n r j hj) = Scheme.Hom.opensRange (affineBlowUp.chart (centerIdeal A n r) ⟨MvPolynomial.X j, β‹―βŸ©)

              The image of the chart U_j is the image of the chart of x_j of affineBlowUp.

              source
              theorem AlgebraicGeometry.CoordinateSubspace.iSup_opensRange_modelChart (A : Type u) [CommRing A] (n r : β„•) :
              ⨆ (j : Fin n), ⨆ (hj : ↑j < r), Scheme.Hom.opensRange (modelChart A n r j hj) = ⊀

              The charts U_j, j < r, cover the model blow-up [Hau14, Definition 4.12] β€” the variables x_j, j < r, generate the centre ideal, and the charts of a generating set cover the affine blow-up.

              Overlaps and the transition map on generators #

              source
              theorem AlgebraicGeometry.CoordinateSubspace.ratio_eq_frac (A : Type u) [CommRing A] (n r : β„•) (j β„“ : Fin n) (hj : ↑j < r) (hβ„“ : ↑ℓ < r) :
              affineBlowUpAlgebra.ratio (centerIdeal A n r) ⟨MvPolynomial.X j, β‹―βŸ© ⟨MvPolynomial.X β„“, β‹―βŸ© = affineBlowUpAlgebra.frac β‹―

              The ratio x_β„“/x_j ∈ A[x][L/x_j] of the affine blow-up is the fraction x_β„“/x_j of the affine blow-up algebra.

              source
              theorem AlgebraicGeometry.CoordinateSubspace.chartRingIso_hom_ratio (A : Type u) [CommRing A] (n r : β„•) (j β„“ : Fin n) (hj : ↑j < r) (hβ„“ : ↑ℓ < r) (hjβ„“ : j β‰  β„“) :
              (CommRingCat.Hom.hom (chartRingIso A n r j).hom) (affineBlowUpAlgebra.ratio (centerIdeal A n r) ⟨MvPolynomial.X j, β‹―βŸ© ⟨MvPolynomial.X β„“, β‹―βŸ©) = MvPolynomial.X β„“

              Under the identification A[x][L/x_j] ≃ A[x], the ratio x_β„“/x_j is the variable x_β„“ (β„“ β‰  j).

              source
              theorem AlgebraicGeometry.CoordinateSubspace.modelChart_preimage_modelChart (A : Type u) [CommRing A] (n r : β„•) (j β„“ : Fin n) (hj : ↑j < r) (hβ„“ : ↑ℓ < r) (hjβ„“ : j β‰  β„“) :
              (TopologicalSpace.Opens.map (modelChart A n r j hj).base).obj (Scheme.Hom.opensRange (modelChart A n r β„“ hβ„“)) = PrimeSpectrum.basicOpen (MvPolynomial.X β„“)

              Inside the chart U_j, the chart U_β„“ (β„“ β‰  j) is the basic open D(x_β„“) [Hau14, Definition 4.13].

              source
              theorem AlgebraicGeometry.CoordinateSubspace.modelTransition_X (A : Type u) [CommRing A] (n r : β„•) (j β„“ i : Fin n) :
              (modelTransition A n r j β„“) (MvPolynomial.X i) = if i = β„“ then (algebraMap (MvPolynomial (Fin n) A) (Localization.Away (MvPolynomial.X β„“))) (MvPolynomial.X j * MvPolynomial.X β„“) else if i = j then IsLocalization.Away.invSelf (MvPolynomial.X β„“) else if ↑i < r then (algebraMap (MvPolynomial (Fin n) A) (Localization.Away (MvPolynomial.X β„“))) (MvPolynomial.X i) * IsLocalization.Away.invSelf (MvPolynomial.X β„“) else (algebraMap (MvPolynomial (Fin n) A) (Localization.Away (MvPolynomial.X β„“))) (MvPolynomial.X i)

              The transition map on the generators [Hau14, Definition 4.12].