The presentation of the affine blow-up algebra

For I = (a, gᵢ : i ∈ ι) the R-algebra map R[xᵢ : i ∈ ι]/(a xᵢ − gᵢ) → R[I/a], xᵢ ↦ gᵢ/a, is surjective, and its kernel is the a-power torsion of the source [TSPA, Tag 0G8S]; when the generators form a regular sequence the torsion vanishes and the chart ring is the quotient itself [Hau14, Theorem 4.20 (b)].

Main declarations

• AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal a g: the ideal (a xᵢ − gᵢ : i ∈ ι) of MvPolynomial ι R.
• affineBlowUpAlgebra.presentationHom a g hg : R[xᵢ]/(a xᵢ − gᵢ) →ₐ[R] R[I/a] with presentationHom_mk_X and presentationHom_unique (existence and uniqueness).
• affineBlowUpAlgebra.presentationHom_surjective (for I = (a, gᵢ)).
• affineBlowUpAlgebra.presentationHom_apply_eq_zero_iff: φ(z) = 0 iff aᵏ z = 0 for some k.

The argument

The Stacks Project proves the kernel statement by base change from the universal case P = ℤ[t₁, …, tₙ], I = (t₁, …, tₙ), a = t₁, where source and target are t₁-torsion free and the map is an isomorphism after inverting t₁. Here the argument is run directly over R, where the source is not torsion free, and it gives the kernel:

• the target R[I/a] ⊆ R_a has a as a nonzerodivisor (affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors), so a-power torsion of the source maps to zero;
• conversely, for a polynomial p there are d and a constant c ∈ R with a^d p ≡ c (mod (a xᵢ − gᵢ)): this is the elimination a xᵢ ≡ gᵢ, by induction on p (a^{d+1} p xᵢ = a^d p (a xᵢ − gᵢ) + gᵢ a^d p ≡ gᵢ c). If the class of p maps to zero then c = 0 in R_a, i.e. a^k c = 0 in R, and then a^{k+d} p ≡ a^k c = 0, so the class of p is a-power torsion.

The only place the description of I enters is surjectivity: R[I/a] is generated by the x/a, x ∈ I, and x = r a + ∑ rᵢ gᵢ gives x/a = r + ∑ rᵢ (gᵢ/a). The construction and the kernel computation only need gᵢ ∈ I.

Conventions

The index type ι is arbitrary (the sources have n generators); the proofs do not use finiteness. The a-power torsion of the quotient module is written ∃ k, a ^ k • z = 0.

Boundary cases

ι empty: I = (a) and the presentation says R/T_a ≅ R[(a)/a] with T_a the a-power torsion (compare [Hau14, Example 4.31], the blow-up along a zero divisor). a = 0: R[I/0] is the zero ring and every element of the source is 0-power torsion (0¹ • z = 0), consistently.

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) : Ideal (MvPolynomial ι R)

The relation ideal (a xᵢ − gᵢ : i ∈ ι) of the presentation.

Equations

• AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal a g = Ideal.span (Set.range fun (i : ι) => MvPolynomial.C a * MvPolynomial.X i - MvPolynomial.C (g i))

theorem AlgebraicGeometry.affineBlowUpAlgebra.sub_mem_presentationIdeal {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) (i : ι) : MvPolynomial.C a * MvPolynomial.X i - MvPolynomial.C (g i) ∈ presentationIdeal a g

theorem AlgebraicGeometry.affineBlowUpAlgebra.aeval_frac_mem_ker {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (p : MvPolynomial ι R) (hp : p ∈ presentationIdeal a g) : (MvPolynomial.aeval fun (i : ι) => frac ⋯) p = 0

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.presentationHom {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) : MvPolynomial ι R ⧸ presentationIdeal a g →ₐ[R] ↥(affineBlowUpAlgebra I a)

The presentation map R[xᵢ]/(a xᵢ − gᵢ) → R[I/a], xᵢ ↦ gᵢ/a [TSPA, Tag 0G8S].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.affineBlowUpAlgebra.presentationHom_mk {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (p : MvPolynomial ι R) : (presentationHom a g hg) ((Ideal.Quotient.mk (presentationIdeal a g)) p) = (MvPolynomial.aeval fun (i : ι) => frac ⋯) p

theorem AlgebraicGeometry.affineBlowUpAlgebra.presentationHom_mk_X {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (i : ι) : (presentationHom a g hg) ((Ideal.Quotient.mk (presentationIdeal a g)) (MvPolynomial.X i)) = frac ⋯

theorem AlgebraicGeometry.affineBlowUpAlgebra.presentationHom_unique {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (φ : MvPolynomial ι R ⧸ presentationIdeal a g →ₐ[R] ↥(affineBlowUpAlgebra I a)) (hφ : ∀ (i : ι), φ ((Ideal.Quotient.mk (presentationIdeal a g)) (MvPolynomial.X i)) = frac ⋯) : φ = presentationHom a g hg

The presentation map is the unique R-algebra map with xᵢ ↦ gᵢ/a.

theorem AlgebraicGeometry.affineBlowUpAlgebra.presentationHom_surjective {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (hI : I = Ideal.span (insert a (Set.range g))) : Function.Surjective ⇑(presentationHom a g hg)

For I = (a, gᵢ : i ∈ ι) the presentation map is surjective [TSPA, Tag 0G8S], since R[I/a] is generated by the x/a, x ∈ I, and x = r a + ∑ rᵢ gᵢ gives x/a = r + ∑ rᵢ (gᵢ/a).

theorem AlgebraicGeometry.affineBlowUpAlgebra.exists_pow_mul_sub_C_mem {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) (p : MvPolynomial ι R) : ∃ (d : ℕ) (c : R), MvPolynomial.C (a ^ d) * p - MvPolynomial.C c ∈ presentationIdeal a g

Elimination of the variables: a^d p ≡ c (mod (a xᵢ − gᵢ)) for some d and constant c.

theorem AlgebraicGeometry.affineBlowUpAlgebra.algHom_apply_eq_zero_iff {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (φ : MvPolynomial ι R ⧸ presentationIdeal a g →ₐ[R] ↥(affineBlowUpAlgebra I a)) (z : MvPolynomial ι R ⧸ presentationIdeal a g) : φ z = 0 ↔ ∃ (k : ℕ), a ^ k • z = 0

The kernel of any R-algebra map from the presentation ring R[xᵢ]/(a xᵢ − gᵢ) to R[I/a] is the a-power torsion of the source [TSPA, Tag 0G8S]; the values on the variables play no role, only the relations a xᵢ = gᵢ and the regularity of a on R[I/a].

theorem AlgebraicGeometry.affineBlowUpAlgebra.presentationHom_apply_eq_zero_iff {R : Type u} [CommRing R] {ι : Type v} (a : R) (g : ι → R) {I : Ideal R} (hg : ∀ (i : ι), g i ∈ I) (z : MvPolynomial ι R ⧸ presentationIdeal a g) : (presentationHom a g hg) z = 0 ↔ ∃ (k : ℕ), a ^ k • z = 0

The kernel of the presentation map is the a-power torsion of the source [TSPA, Tag 0G8S].