Documentation

TauCeti.AlgebraicGeometry.Blowup.Submodule.Basic

The blowup of a submodule #

Let B be a C-algebra, F ⊆ B a set and J = span C F the C-submodule of B it spans. The graded ring R(J) = ⨁ₙ Jⁿ Tⁿ ⊆ B[T], with J⁰ the image of C, is TauCeti.coeffSubalgebra of the powers n ↦ Jⁿ, and it is generated over C by the elements f T with f ∈ F. Its Proj

Y = Proj R(J) ⟶ Spec C

is the blowup of the submodule J; the ring theory of R(J) and of its charts is in TauCeti/RingTheory/GradedAlgebra/SubmoduleBlowup.lean. When B = C and J is an ideal, R(J) is the Rees algebra (reesAlgebra_eq_coeffSubalgebra) and Y is the blowup of Spec C along V(J). For a general ring map C → B, this is the scheme used in Huber's proof that a complete Huber ring B with a noetherian ring of definition C is sheafy, applied to generators F of the unit ideal of B that define a standard rational covering of Spa B.

The construction of Y needs no hypothesis on F, and the standard opens D₊(f T), f ∈ F, cover it. If F is finite, Y is proper over Spec C, and noetherian when C is. If F generates the unit ideal of B, then the image of the irrelevant ideal of R(J) under evaluation at T = 1 generates the unit ideal of B, and so evaluation defines a morphism Spec B ⟶ Y over Spec C; the standard open D₊(f T) pulls back to the basic open D(f), and this morphism is affine.

The affine charts of Y are explicit. For a nonempty finite subset S ⊆ F with product t, the element t T^{#S} = ∏_{f' ∈ S} f' T has degree #S, and the standard open D₊(t T^{#S}) is the spectrum of the chart ring C[F/S]: the C-subalgebra of the localization B_t generated by the fractions f/f' with f ∈ F and f' ∈ S. The fraction x/(t T^{#S})ⁿ of the homogeneous localization, with x = b T^{n #S}, corresponds to b/tⁿ, and the generator f/f' to (f T)/(f' T). In Huber's proof, the rings C[F/f'] are the rings of definition of the rational localizations B(F/f'). The charts follow the ideal case affineBlowupι_toSpecZero in TauCeti/AlgebraicGeometry/Blowup/AffineCharts.lean: the chart is Proj.basicOpenIsoSpec followed by the spectrum of the ring isomorphism awayEquivFractionSubalgebra.

If F generates the unit ideal of B, the blowup changes nothing where Spec B and Spec C agree: over every open U ⊆ Spec C over which Spec B ⟶ Spec C restricts to an isomorphism, so does Y ⟶ Spec C. Over a basic open D(h) ⊆ U the map C_h → B_h is bijective, so some a = hᴺ lies in J, the part of Y over D(h) lies in the standard open D₊(a T), and over D(h) the chart Spec R(J)_(a T) ⟶ Spec C is Spec of the isomorphism C_h ≅ (R(J)_(a T))_h. In Huber's proof C is a ring of definition of B with ideal of definition I, and U is the complement of V(I): the non-open primes of C.

Main definitions #

Main results #

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.AlgebraicGeometry.submoduleBlowup (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
AlgebraicGeometry.Scheme

The blowup of a submodule. The scheme Proj R(J) of the graded ring R(J) = ⨁ₙ Jⁿ Tⁿ of the submodule J = span C F of the C-algebra B.

Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.toSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
    submoduleBlowup C F ⟶ AlgebraicGeometry.Spec ↧C

    The structure morphism Proj R(J) ⟶ Spec C: the projection to the spectrum of the degree zero part of R(J), followed by the spectrum of the structure map of C.

    Instances For
      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.toSpec_def (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
      toSpec C F = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero (gradedRing C F)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C ↥(gradedRing C F 0))))

      The structure morphism is Proj.toSpecZero followed by Spec R(J)₀ ⟶ Spec C.

      source
      @[instance_reducible]
      noncomputable instance TauCeti.AlgebraicGeometry.submoduleBlowup.instOver (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
      (submoduleBlowup C F).Over (AlgebraicGeometry.Spec ↧C)

      The submodule blowup is a scheme over its coefficient ring through toSpec.

      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.over_eq_toSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
      submoduleBlowup C F ↘ AlgebraicGeometry.Spec ↧C = toSpec C F

      The structure morphism of the submodule blowup is toSpec.

      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.toSpec_preimage_basicOpen (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) (h : C) :
      (TopologicalSpace.Opens.map (toSpec C F).base).obj (PrimeSpectrum.basicOpen h) = AlgebraicGeometry.Proj.basicOpen (gradedRing C F) ((algebraMap C ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)) h)

      The inverse image of the basic open D(h) of Spec C in the blowup is the standard open D₊(h) of the degree-zero image of h.

      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.iSup_basicOpen_eq_top (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
      ⨆ (f : ↑F), AlgebraicGeometry.Proj.basicOpen (gradedRing C F) (monomialDegreeOne C ⋯) = ⊤

      The standard opens D₊(f T) cover the blowup.

      source
      instance TauCeti.AlgebraicGeometry.submoduleBlowup.instIsClosedImmersionMapOfHomSubtypePolynomialMemSubalgebraCoeffSubalgebraHPowSubmoduleNatSpanGradedRingOfNatAlgebraMap (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) :
      AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C ↥(gradedRing C F 0))))

      The second factor Spec R(J)₀ ⟶ Spec C of the structure morphism is a closed immersion.

      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : F.Finite) :
      AlgebraicGeometry.IsProper (toSpec C F)

      The blowup of a finitely generated submodule is proper. If F is finite, the structure morphism Proj R(J) ⟶ Spec C is proper.

      source
      theorem TauCeti.AlgebraicGeometry.submoduleBlowup.isNoetherian (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : F.Finite) [IsNoetherianRing C] :
      AlgebraicGeometry.IsNoetherian (submoduleBlowup C F)

      If C is noetherian and F is finite, the blowup Proj R(J) is a noetherian scheme.

      source
      noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.fromSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) :
      AlgebraicGeometry.Spec ↧B ⟶ submoduleBlowup C F

      The morphism Spec B ⟶ Proj R(J) defined by evaluation at T = 1, when F generates the unit ideal of B.

      Instances For
        source
        theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fromSpec_def (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) (h : Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧B).inv).comp (coeffSubalgebra.evalOne fun (n : ℕ) => Submodule.span C F ^ n).toRingHom) (HomogeneousIdeal.irrelevant (gradedRing C F)).toIdeal = ⊤) :
        fromSpec C hF = AlgebraicGeometry.Proj.fromOfGlobalSections (gradedRing C F) ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧B).inv).comp (coeffSubalgebra.evalOne fun (n : ℕ) => Submodule.span C F ^ n).toRingHom) h

        Spec B ⟶ Proj R(J) is the morphism to Proj defined by evaluation at T = 1, as a map to the global sections of Spec B.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fromSpec_toSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) :
        CategoryTheory.CategoryStruct.comp (fromSpec C hF) (toSpec C F) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C B))

        The morphism Spec B ⟶ Proj R(J) is a morphism over Spec C: followed by the structure morphism of the blowup, it is the spectrum of the structure map C → B.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fromSpec_toSpec_assoc (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧C ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (fromSpec C hF) (CategoryTheory.CategoryStruct.comp (toSpec C F) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C B))) h

        The morphism Spec B ⟶ Proj R(J) is a morphism over Spec C: followed by the structure morphism of the blowup, it is the spectrum of the structure map C → B.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fromSpec_preimage_basicOpen (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) {f : B} (hf : f ∈ F) :
        (TopologicalSpace.Opens.map (fromSpec C hF).base).obj (AlgebraicGeometry.Proj.basicOpen (gradedRing C F) (monomialDegreeOne C hf)) = PrimeSpectrum.basicOpen f

        The standard open D₊(f T) of Proj R(J) pulls back to the basic open D(f) of Spec B.

        source
        instance TauCeti.AlgebraicGeometry.submoduleBlowup.isAffineHom_fromSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) :
        AlgebraicGeometry.IsAffineHom (fromSpec C hF)

        The morphism Spec B ⟶ Proj R(J) is affine: the standard opens D₊(f T) are affine, and so are their preimages D(f).

        source
        noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {S : Finset B} (L : Type u) [CommRing L] [Algebra C L] [Algebra B L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) (hS₀ : S.Nonempty) :
        ↑(AlgebraicGeometry.Proj.basicOpen (gradedRing C F) (monomialProd C hS)) ≅ AlgebraicGeometry.Spec ↧↥(fractionSubalgebra C F S L)

        The affine charts of the blowup of a submodule. For a nonempty finite subset S ⊆ F with product t, the standard open D₊(t T^{#S}) of Proj R(J) is isomorphic to Spec C[F/S], the spectrum of the C-subalgebra of B_t generated by the fractions f/f' with f ∈ F and f' ∈ S. It is Mathlib's Proj.basicOpenIsoSpec followed by the spectrum of awayEquivFractionSubalgebra.

        Instances For
          source
          theorem TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec_inv_comp (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {S : Finset B} (L : Type u) [CommRing L] [Algebra C L] [Algebra B L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) (hS₀ : S.Nonempty) :
          CategoryTheory.CategoryStruct.comp (basicOpenIsoSpec C L hS hS₀).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (gradedRing C F) (monomialProd C hS)).ι (toSpec C F)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C ↥(fractionSubalgebra C F S L)))

          The chart Spec C[F/S] ≅ D₊(t T^{#S}) ⊆ Proj R(J) is a morphism over Spec C: followed by the structure morphism of the blowup, it is the spectrum of the structure map C → C[F/S].

          source
          theorem TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec_inv_comp_assoc (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {S : Finset B} (L : Type u) [CommRing L] [Algebra C L] [Algebra B L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) (hS₀ : S.Nonempty) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧C ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (basicOpenIsoSpec C L hS hS₀).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen (gradedRing C F) (monomialProd C hS)).ι (CategoryTheory.CategoryStruct.comp (toSpec C F) h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C ↥(fractionSubalgebra C F S L)))) h

          The chart Spec C[F/S] ≅ D₊(t T^{#S}) ⊆ Proj R(J) is a morphism over Spec C: followed by the structure morphism of the blowup, it is the spectrum of the structure map C → C[F/S].

          source
          theorem TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec_hom_generator (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {S : Finset B} (L : Type u) [CommRing L] [Algebra C L] [Algebra B L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] [DecidableEq B] (hS : ↑S ⊆ F) (hS₀ : S.Nonempty) {f f' : B} (hf : f ∈ F) (hf' : f' ∈ S) {z : L} (hz : (algebraMap B L) f' * z = (algebraMap B L) f) :
          (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso ↧↥(fractionSubalgebra C F S L)).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (basicOpenIsoSpec C L hS hS₀).hom) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Proj.basicOpenIsoSpec (gradedRing C F) (monomialProd C hS) ⋯ ⋯).inv) (AlgebraicGeometry.Scheme.ΓSpecIso ↧(HomogeneousLocalization.Away (gradedRing C F) (monomialProd C hS))).hom)))) ⟨z, ⋯⟩ = HomogeneousLocalization.Away.mk (gradedRing C F) ⋯ 1 (monomialDegreeOne C hf * monomialProd C ⋯) ⋯

          The chart sends f/f' to (f T)/(f' T). For f ∈ F and f' ∈ S, pulling the generator f/f' of C[F/S] back along the chart, and identifying the sections of D₊(t T^{#S}) with R(J)_(t T^{#S}) through Proj.basicOpenIsoSpec, gives the homogeneous fraction (f T)/(f' T), written over the denominator t T^{#S} = ∏_{g ∈ S} g T as ((f T) ∏_{g ∈ S, g ≠ f'} g T)/(t T^{#S}). Together with basicOpenIsoSpec_inv_comp, this determines the chart.

          source
          theorem TauCeti.AlgebraicGeometry.submoduleBlowup.isIso_toSpec_restrict (C : Type u) {B : Type u} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) {U : (AlgebraicGeometry.Spec ↧C).Opens} (hU : CategoryTheory.IsIso (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap C B)) ∣_ U)) :
          CategoryTheory.IsIso (toSpec C F ∣_ U)

          The blowup of a submodule is an isomorphism away from the centre. Let F generate the unit ideal of B, and let U be an open subset of Spec C over which Spec B ⟶ Spec C restricts to an isomorphism. Then the blowup Proj R(J) ⟶ Spec C also restricts to an isomorphism over U.

          For instance, if B is a Huber ring, C a ring of definition with ideal of definition I and U = Spec C ∖ V(I), this applies by Subring.isIso_morphismRestrict_nonOpenPrimes. The hypothesis on F cannot be dropped: for C = B = k[x, y] and F = {x, y} the blowup of the origin is not an isomorphism, although Spec B ⟶ Spec C is the identity.