The affine blow-up algebra R[I/a]

For an ideal I ⊆ R and a ∈ I, the affine blow-up algebra R[I/a] is the R-subalgebra of the localization R_a = R[1/a] generated by the fractions x/a, x ∈ I [TSPA, Tag 052P]; it is Hauser's ring extension R_j = R[g₁/g_j, …, g_k/g_j] ⊆ R_{g_j} [Hau14, Definition 4.13] and the degree-zero part of the localized Rees algebra, consisting of the fractions f/gˡ with f ∈ Iˡ [Hau14, Definition 4.16]. Its elements are exactly the fractions x/aⁿ with x ∈ Iⁿ (mem_affineBlowUpAlgebra_iff): the set of such fractions contains the generators and the constants and is closed under sums (x/aⁿ + y/aᵐ = (aᵐx + aⁿy)/aⁿ⁺ᵐ, with aᵐx ∈ Iⁿ⁺ᵐ because a ∈ I) and products, and conversely x/aⁿ⁺¹ = ∑ (d/aⁿ)(c/a) for x = ∑ dc ∈ Iⁿ · I. Equality of fractions is that of R_a: x/aⁿ = y/aᵐ iff aᵏ(aᵐx − aⁿy) = 0 for some k (IsLocalization.mk'_eq_iff_eq).

The definition makes sense for every a; the membership lemma uses a ∈ I (as the sources assume) exactly once, to place aᵐx in Iⁿ⁺ᵐ when adding two fractions — for a ∉ I it fails (R = k[a, b], I = (b): b/a + b²/a² is no z/aⁿ with z ∈ (bⁿ)). Boundary cases: a = 1 gives R_1 ≅ R and R[I/1] = R_1 (every constant is a fraction x/1⁰); a nilpotent gives the zero ring R_a. The properties of R[I/a] (its generators, a a nonzerodivisor, I·R[I/a] = a·R[I/a], the lifting property) are in Hironaka.Scheme.BlowUp.AffineAlgebra; its spectrum is the chart of the affine blow-up at a (Hironaka.Scheme.BlowUp.Rees.ChartRing).

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.awayFrac {R : Type u} [CommRing R] (a : R) (n : ℕ) (x : R) : Localization.Away a

The fraction x / aⁿ in R_a, the shape of the elements of R[I/a].

Equations

• AlgebraicGeometry.awayFrac a n x = Localization.mk x ⟨a ^ n, ⋯⟩

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra {R : Type u} [CommRing R] (I : Ideal R) (a : R) : Subalgebra R (Localization.Away a)

The affine blow-up algebra R[I/a] [TSPA, Tag 052P]; [Hau14, Definitions 4.13 and 4.16]: the R-subalgebra of R_a generated by the fractions x/a, x ∈ I. Its elements are the fractions x/aⁿ with x ∈ Iⁿ (mem_affineBlowUpAlgebra_iff).

Equations

• AlgebraicGeometry.affineBlowUpAlgebra I a = Algebra.adjoin R ((fun (x : R) => Localization.mk x ⟨a, ⋯⟩) '' ↑I)

theorem AlgebraicGeometry.awayFrac_one {R : Type u} [CommRing R] {a : R} (x : R) : awayFrac a 1 x = Localization.mk x ⟨a, ⋯⟩

theorem AlgebraicGeometry.awayFrac_zero {R : Type u} [CommRing R] {a : R} (x : R) : awayFrac a 0 x = (algebraMap R (Localization.Away a)) x

theorem AlgebraicGeometry.awayFrac_add {R : Type u} [CommRing R] {a : R} (n m : ℕ) (x y : R) : awayFrac a n x + awayFrac a m y = awayFrac a (n + m) (a ^ m * x + a ^ n * y)

theorem AlgebraicGeometry.awayFrac_mul {R : Type u} [CommRing R] {a : R} (n m : ℕ) (x y : R) : awayFrac a n x * awayFrac a m y = awayFrac a (n + m) (x * y)

theorem AlgebraicGeometry.awayFrac_mem_affineBlowUpAlgebra {R : Type u} [CommRing R] {I : Ideal R} {a : R} (n : ℕ) {x : R} (hx : x ∈ I ^ n) : awayFrac a n x ∈ affineBlowUpAlgebra I a

The fractions x/aⁿ, x ∈ Iⁿ, lie in R[I/a] [TSPA, Tag 052P].

theorem AlgebraicGeometry.mem_affineBlowUpAlgebra_iff {R : Type u} [CommRing R] {I : Ideal R} {a : R} (ha : a ∈ I) {y : Localization.Away a} : y ∈ affineBlowUpAlgebra I a ↔ ∃ (n : ℕ), ∃ x ∈ I ^ n, y = awayFrac a n x

The membership lemma [TSPA, Tag 052P]: the elements of R[I/a] are exactly the fractions x/aⁿ with x ∈ Iⁿ.