The graded ring of the blowup of a submodule and its charts

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 is the blowup of the submodule J, TauCeti.AlgebraicGeometry.submoduleBlowup in TauCeti/AlgebraicGeometry/Blowup/Submodule/Basic.lean. This file contains the ring theory of the blowup, which needs no scheme theory; the declarations live in the namespace of that scheme. The surjective graded map presentation from the symmetric algebra on the free coordinates F sends each coordinate to f T; it uses SymmetricAlgebra.gradedLift and supplies the closed projective embedding of the blowup.

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.

For a finite subset S ⊆ F with product t, the element t T^{#S} = ∏_{f' ∈ S} f' T has degree #S, and the homogeneous localization R(J)_(t T^{#S}) is isomorphic to 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})ⁿ, with x = b T^{n #S}, corresponds to b/tⁿ, and the generator f/f' to (f T)/(f' T). When S is nonempty, R(J)_(t T^{#S}) is the coordinate ring of the standard open D₊(t T^{#S}) of the blowup, so C[F/S] is the coordinate ring of an affine chart. In Huber's proof, the rings C[F/f'] are the rings of definition of the rational localizations B(F/f').

The construction of the isomorphism follows the ideal case reesAlgebra.awayEquivAffineBlowup in TauCeti/RingTheory/ReesAlgebra/AffineBlowup.lean, which is C = B with J an ideal and #S = 1: it is the lift of evaluation at T = 1 through HomogeneousLocalization.Away.lift. The description mem_fractionSubalgebra_iff of the elements of C[F/S] parallels Ideal.mem_affineBlowup_iff in TauCeti/RingTheory/Ideal/AffineBlowup.lean.

Main definitions

• TauCeti.AlgebraicGeometry.submoduleBlowup.gradedRing C F: the graded ring R(J).
• TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOneOfMemSpan C ha: the element a T of R(J), for a ∈ J.
• TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOne C hf: the element f T of R(J), for f ∈ F.
• TauCeti.AlgebraicGeometry.submoduleBlowup.presentation C F: the surjection from the symmetric algebra on the free module with basis F to R(J).
• TauCeti.AlgebraicGeometry.submoduleBlowup.fractionSubalgebra C F S L: the chart ring C[F/S], inside a B-algebra L.
• TauCeti.AlgebraicGeometry.submoduleBlowup.monomialProd C hS: the element t T^{#S} of R(J), for a finite subset S ⊆ F with product t.
• TauCeti.AlgebraicGeometry.submoduleBlowup.awayEquivFractionSubalgebra C L hS: the isomorphism R(J)_(t T^{#S}) ≃ₐ[C] C[F/S], for a localization L of B away from t.

Main results

• TauCeti.AlgebraicGeometry.submoduleBlowup.adjoin_monomialDegreeOne_eq_top: R(J) is generated over its degree zero part by the elements f T.
• TauCeti.AlgebraicGeometry.submoduleBlowup.map_evalOne_irrelevant: if F generates the unit ideal of B, so does the image of the irrelevant ideal of R(J) under evaluation at T = 1.
• TauCeti.AlgebraicGeometry.submoduleBlowup.exists_algebraMap_pow_mem_span_of_span_eq_top: if F generates the unit ideal of B and C_h → B_h is surjective, then some power of h lies in J.
• TauCeti.AlgebraicGeometry.submoduleBlowup.mem_fractionSubalgebra_iff: the elements of C[F/S] are the fractions y/tⁿ with y ∈ J^{n #S}.
• TauCeti.AlgebraicGeometry.submoduleBlowup.awayEquivFractionSubalgebra_symm_apply_of_mul_eq: the generator f/f' of C[F/S] corresponds to the homogeneous fraction (f T)/(f' T).

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, proof of Theorem 2.5, Case I, (1.1) and (1.2)(i),(ii).
• The Stacks Project, Section Blowing up, in particular Lemma 0804 for the affine charts.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.submoduleBlowup.gradedRing (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) : ℕ → Submodule C ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)

The graded ring R(J) = ⨁ₙ Jⁿ Tⁿ ⊆ B[T] of the submodule J = span C F of the C-algebra B, graded by the power of T. Its degree n piece consists of the monomials b Tⁿ with b ∈ Jⁿ.

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOneOfMemSpan (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {a : B} (ha : a ∈ Submodule.span C F) : ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)

The element a T of degree one of R(J), for a ∈ J.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.coe_monomialDegreeOneOfMemSpan (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {a : B} (ha : a ∈ Submodule.span C F) : ↑(monomialDegreeOneOfMemSpan C ha) = (Polynomial.monomial 1) a

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOneOfMemSpan_mem_gradedRing (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {a : B} (ha : a ∈ Submodule.span C F) : monomialDegreeOneOfMemSpan C ha ∈ gradedRing C F 1

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOne (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {f : B} (hf : f ∈ F) : ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)

The element f T of degree one of R(J), for f ∈ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.coe_monomialDegreeOne (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {f : B} (hf : f ∈ F) : ↑(monomialDegreeOne C hf) = (Polynomial.monomial 1) f

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOne_mem_gradedRing (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {f : B} (hf : f ∈ F) : monomialDegreeOne C hf ∈ gradedRing C F 1

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.adjoin_monomialDegreeOne_eq_top (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) : Algebra.adjoin (↥(gradedRing C F 0)) (Set.range fun (f : ↑F) => monomialDegreeOne C ⋯) = ⊤

R(J) is generated over its degree zero part by the elements f T with f ∈ F.

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.presentation (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] (F : Set B) : SymmetricAlgebra.homogeneousSubmodule C (↑F →₀ C) →+*ᵍ gradedRing C F

The graded presentation of R(J) by the symmetric algebra on the free module with basis F. The coordinate indexed by f ∈ F maps to f T. No finiteness or unit-ideal hypothesis is needed.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.presentation_ι_single (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (f : ↑F) (c : C) : (presentation C F) ((SymmetricAlgebra.ι C (↑F →₀ C)) (Finsupp.single f c)) = c • monomialDegreeOne C ⋯

Each free coordinate maps to the corresponding degree-one monomial.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.presentation_gradedZeroRingHom_algebraMap (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (c : C) : (presentation C F).gradedZeroRingHom ((algebraMap C ↥(SymmetricAlgebra.homogeneousSubmodule C (↑F →₀ C) 0)) c) = (algebraMap C ↥(gradedRing C F 0)) c

The graded presentation preserves the coefficient ring in degree zero.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.presentation_surjective (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} : Function.Surjective ⇑(presentation C F)

The free coordinates generate the entire graded ring of the submodule blowup.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.evalOne_monomialDegreeOne (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {f : B} (hf : f ∈ F) : (coeffSubalgebra.evalOne fun (n : ℕ) => Submodule.span C F ^ n) (monomialDegreeOne C hf) = f

Evaluation of R(J) ⊆ B[T] at T = 1 sends f T to f.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.map_evalOne_irrelevant (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) : Ideal.map (coeffSubalgebra.evalOne fun (n : ℕ) => Submodule.span C F ^ n) (HomogeneousIdeal.irrelevant (gradedRing C F)).toIdeal = ⊤

If F generates the unit ideal of B, the ideal of B generated by the image of the irrelevant ideal of R(J) under evaluation at T = 1 is all of B.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.exists_algebraMap_pow_mem_span_of_span_eq_top {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] [Algebra C B] {F : Set B} (hF : Ideal.span F = ⊤) {h : C} (hs : ∀ (b : B), ∃ (c : C) (m : ℕ), (algebraMap C B) c = (algebraMap C B) h ^ m * b) : ∃ (N : ℕ), (algebraMap C B) (h ^ N) ∈ Submodule.span C F

If F generates the unit ideal of B and every element of B becomes, after multiplication by a power of h ∈ C, the image of an element of C, then some power of h maps into J = span C F. Indeed the elements b with hⁿ b ∈ J for some n form an ideal containing F.

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.fractionSubalgebra (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] (F : Set B) (S : Finset B) (L : Type u_3) [CommRing L] [Algebra B L] [Algebra C L] : Subalgebra C L

The chart ring C[F/S]. The C-subalgebra of L generated by the fractions f/f' with f ∈ F and f' ∈ S, that is, by the elements z with f' z = f. When L is a localization of B away from the product t of the elements of S, every f' ∈ S is a unit of L and f/f' is the unique such z. If moreover S is a nonempty subset of F and the C-algebra structure of L is the one induced from B (IsScalarTower C B L), then C[F/S] is the coordinate ring of the standard open D₊(t T^{#S}) of the blowup Proj R(J) (submoduleBlowup.basicOpenIsoSpec).

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fractionSubalgebra_def (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] (F : Set B) (S : Finset B) (L : Type u_3) [CommRing L] [Algebra B L] [Algebra C L] : fractionSubalgebra C F S L = Algebra.adjoin C {z : L | ∃ f ∈ F, ∃ f' ∈ S, (algebraMap B L) f' * z = (algebraMap B L) f}

C[F/S] is generated over C by the elements z with f' z = f, for f ∈ F and f' ∈ S.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.mem_fractionSubalgebra_of_mul_eq {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} {L : Type u_3} [CommRing L] [Algebra B L] [Algebra C L] {f f' : B} (hf : f ∈ F) (hf' : f' ∈ S) {z : L} (hz : (algebraMap B L) f' * z = (algebraMap B L) f) : z ∈ fractionSubalgebra C F S L

The fraction f/f', for f ∈ F and f' ∈ S, lies in C[F/S].

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.fractionSubalgebra_le_iff {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} {L : Type u_3} [CommRing L] [Algebra B L] [Algebra C L] {A : Subalgebra C L} : fractionSubalgebra C F S L ≤ A ↔ ∀ f ∈ F, ∀ f' ∈ S, ∀ (z : L), (algebraMap B L) f' * z = (algebraMap B L) f → z ∈ A

A subalgebra of L contains C[F/S] exactly when it contains every fraction f/f' with f ∈ F and f' ∈ S.

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.monomialProd (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} [Algebra C B] (hS : ↑S ⊆ F) : ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)

The element t T^{#S} of degree #S of R(J), for a finite subset S ⊆ F with product t: the product of the elements f T with f ∈ S.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.coe_monomialProd (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} [Algebra C B] (hS : ↑S ⊆ F) : ↑(monomialProd C hS) = (Polynomial.monomial S.card) (∏ g ∈ S, g)

t T^{#S} is the monomial of degree #S with coefficient t.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.monomialProd_mem_gradedRing (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} [Algebra C B] (hS : ↑S ⊆ F) : monomialProd C hS ∈ gradedRing C F S.card

t T^{#S} is homogeneous of degree #S.

@[simp]

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.evalOne_monomialProd (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} [Algebra C B] (hS : ↑S ⊆ F) : (coeffSubalgebra.evalOne fun (n : ℕ) => Submodule.span C F ^ n) (monomialProd C hS) = ∏ g ∈ S, g

Evaluation of R(J) ⊆ B[T] at T = 1 sends t T^{#S} to t.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.monomialDegreeOne_mul_monomialProd_erase_mem_gradedRing (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} [Algebra C B] [DecidableEq B] (hS : ↑S ⊆ F) {f f' : B} (hf : f ∈ F) (hf' : f' ∈ S) : monomialDegreeOne C hf * monomialProd C ⋯ ∈ gradedRing C F (1 • S.card)

For f ∈ F and f' ∈ S, the product (f T) ∏_{g ∈ S, g ≠ f'} g T is homogeneous of degree #S, the degree of t T^{#S}: it is the numerator of (f T)/(f' T) over t T^{#S}.

noncomputable def TauCeti.AlgebraicGeometry.submoduleBlowup.awayEquivFractionSubalgebra (C : Type u_1) {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} (L : Type u_3) [CommRing L] [Algebra B L] [Algebra C B] [Algebra C L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) : HomogeneousLocalization.Away (gradedRing C F) (monomialProd C hS) ≃ₐ[C] ↥(fractionSubalgebra C F S L)

The affine charts of the blowup of a submodule. For a finite subset S ⊆ F with product t, the homogeneous localization R(J)_(t T^{#S}) is isomorphic to the chart ring C[F/S] inside a localization L of B away from t: the fraction x/(t T^{#S})ⁿ corresponds to b/tⁿ, where x = b T^{n #S}. The isomorphism preserves coefficients from C. When S is nonempty, R(J)_(t T^{#S}) is the coordinate ring of the standard open D₊(t T^{#S}) of Proj R(J).

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.algebraMap_pow_mul_awayEquivFractionSubalgebra_mk {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} {L : Type u_3} [CommRing L] [Algebra B L] [Algebra C B] [Algebra C L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) {n : ℕ} {x : ↥(coeffSubalgebra fun (n : ℕ) => Submodule.span C F ^ n)} (hx : x ∈ gradedRing C F (n • S.card)) : (algebraMap B L) (∏ g ∈ S, g) ^ n * ↑((awayEquivFractionSubalgebra C L hS) (HomogeneousLocalization.Away.mk (gradedRing C F) ⋯ n x hx)) = (algebraMap B L) ((↑x).coeff (n • S.card))

The fraction x/(t T^{#S})ⁿ, for x = b T^{n #S} homogeneous of degree n #S, corresponds to the element b/tⁿ of C[F/S].

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.mem_fractionSubalgebra_iff {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} {L : Type u_3} [CommRing L] [Algebra B L] [Algebra C B] [Algebra C L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] (hS : ↑S ⊆ F) {z : L} : z ∈ fractionSubalgebra C F S L ↔ ∃ (n : ℕ), ∃ y ∈ Submodule.span C F ^ (n * S.card), (algebraMap B L) (∏ g ∈ S, g) ^ n * z = (algebraMap B L) y

The elements of C[F/S]. For a finite subset S ⊆ F with product t, an element z of a localization L of B away from t lies in C[F/S] exactly when tⁿ z ∈ J^{n #S} for some n, that is, when z is a fraction y/tⁿ with y ∈ J^{n #S}.

theorem TauCeti.AlgebraicGeometry.submoduleBlowup.awayEquivFractionSubalgebra_symm_apply_of_mul_eq {C : Type u_1} {B : Type u_2} [CommRing C] [CommRing B] {F : Set B} {S : Finset B} {L : Type u_3} [CommRing L] [Algebra B L] [Algebra C B] [Algebra C L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L] [DecidableEq B] (hS : ↑S ⊆ F) {f f' : B} (hf : f ∈ F) (hf' : f' ∈ S) {z : L} (hz : (algebraMap B L) f' * z = (algebraMap B L) f) : (awayEquivFractionSubalgebra C L hS).symm ⟨z, ⋯⟩ = HomogeneousLocalization.Away.mk (gradedRing C F) ⋯ 1 (monomialDegreeOne C hf * monomialProd C ⋯) ⋯

The generators of the chart. For f ∈ F and f' ∈ S, the generator f/f' of C[F/S] corresponds to 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}).