The affine blow-up algebra R[I/a]: elements, basic properties, lifting

For a ring R, an ideal I ⊆ R and an element a ∈ R, the affine blow-up algebra R[I/a] is the R-subalgebra of R_a = R[1/a] generated by the fractions x/a, x ∈ I [TSPA, Tag 052P]; [Hau14, Definition 4.13] (the rings R[g₁/gⱼ, …, g_k/gⱼ] ⊆ R_{gⱼ}); [Hau14, Definition 4.16] (the degree-zero part of the localized Rees algebra). Spec R[I/a] is the chart of the blow-up of Spec R along I at the generator a (Hironaka.Scheme.BlowUp.AffineBlowUp.Chart). The definition AlgebraicGeometry.affineBlowUpAlgebra is in Hironaka.Scheme.BlowUp.AffineBlowUpAlgebra; this module builds its properties.

Main declarations

• affineBlowUpAlgebra.frac hx = x/a for x ∈ I, the generators, written as algebraMap x * invSelf a (coe_frac; coe_frac_eq_awayFrac relates them to the fraction awayFrac a 1 x of the definition module); affineBlowUpAlgebra_eq_adjoin and the induction principle affineBlowUpAlgebra.induction_on.
• affineBlowUpAlgebra.mem_iff: for a ∈ I the elements of R[I/a] are the fractions x/aⁿ with x ∈ Iⁿ; algebraMap_mul_pow_eq_iff: x/aⁿ = y/aᵐ in R_a iff aᵏ(aᵐx − aⁿy) = 0 for some k.
• affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors, map_algebraMap_eq_span_singleton, isLocalization_away [TSPA, Tag 07Z3]: a is a nonzerodivisor of R[I/a], I·R[I/a] = a·R[I/a] for a ∈ I, and R[I/a]_a = R_a.
• affineBlowUpAlgebra.lift with lift_comp_algebraMap, lift_unique, mul_pow_of_comp_eq [Hau14, Theorem 4.18, proof (d)]: if β : R → S sends f ∈ I to a nonzerodivisor generating β(I)S, there is a unique ring map δ : R[I/f] → S extending β, and it is given by "division by β(f)": δ(x/fⁿ)·β(f)ⁿ = β(x).

The arguments

Elements. A generator x/a is x/a¹; r ∈ R is r/a⁰; a sum x/aⁿ + y/aᵐ = (x aᵐ + y aⁿ)/aⁿ⁺ᵐ needs a ∈ I to keep the numerator in Iⁿ⁺ᵐ; a product is xy/aⁿ⁺ᵐ. Conversely x/aⁿ ∈ R[I/a] for x ∈ Iⁿ by induction on n, since Iⁿ⁺¹ = I·Iⁿ.

Basic properties. a is a unit of R_a ⊇ R[I/a], so multiplication by a is injective on R[I/a]. For x ∈ I, x = a·(x/a) shows I·R[I/a] ⊆ (a), and a ∈ I gives the other inclusion. R_a is the localization of R[I/a] at a because a is a unit of R_a, every element of R_a is p/aⁿ = (image of p)·a⁻ⁿ, and R[I/a] → R_a is injective.

Lifting. Hauser defines δ(hₗ/fˡ) = aₗ where β(hₗ) = aₗ β(f)ˡ, the quotient being unique because β(f) is a nonzerodivisor. This division is realized as follows: β induces R_f → S_{β(f)} on localizations; restricted to R[I/f] its values lie in the image of S, because β(x) ∈ (β(I)S)ⁿ = (β(f)ⁿ) for x ∈ Iⁿ; and S → S_{β(f)} is injective because β(f) is a nonzerodivisor. So δ is the composite of the restricted map with the inverse of this injection. Uniqueness: a ring map δ' extending β satisfies δ'(z) β(f)ⁿ = β(x) whenever z fⁿ = x, which pins δ'(z) by cancellation.

Conventions

The definition takes any a : R; the hypothesis a ∈ I of the sources enters only the lemmas that need it. The fraction x/a is algebraMap R R_a x * invSelf a with IsLocalization.Away.invSelf a = 1/a, and x/aⁿ is written multiplicatively (y * aⁿ = x).

Boundary cases

a = 0: R_a and R[I/a] are the zero ring. a = 1: R[I/1] is the image of R in R_1 ≅ R. I = ⊥: R[⊥/a] is the image of R in R_a. I = ⊤, a ∈ I arbitrary: R[R/a] = R_a.

theorem AlgebraicGeometry.awayFrac_one_eq {R : Type u} [CommRing R] {a : R} (x : R) : awayFrac a 1 x = (algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a

The fraction x/a of R_a (the generator shape of the definition module) is algebraMap x * invSelf a with invSelf a = 1/a.

theorem AlgebraicGeometry.affineBlowUpAlgebra_eq_adjoin {R : Type u} [CommRing R] (I : Ideal R) (a : R) : affineBlowUpAlgebra I a = Algebra.adjoin R ((fun (x : R) => (algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a) '' ↑I)

R[I/a] is generated by the fractions algebraMap x * invSelf a, x ∈ I (the definition's generators Localization.mk x a rewritten).

theorem AlgebraicGeometry.affineBlowUpAlgebra.mul_invSelf_mem {R : Type u} [CommRing R] {I : Ideal R} {a x : R} (hx : x ∈ I) : (algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a ∈ affineBlowUpAlgebra I a

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.frac {R : Type u} [CommRing R] {I : Ideal R} {a x : R} (hx : x ∈ I) : ↥(affineBlowUpAlgebra I a)

The generator x/a ∈ R[I/a] for x ∈ I.

Equations

• AlgebraicGeometry.affineBlowUpAlgebra.frac hx = ⟨(algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a, ⋯⟩

@[simp]

theorem AlgebraicGeometry.affineBlowUpAlgebra.coe_frac {R : Type u} [CommRing R] {I : Ideal R} {a x : R} (hx : x ∈ I) : ↑(frac hx) = (algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a

theorem AlgebraicGeometry.affineBlowUpAlgebra.coe_frac_eq_awayFrac {R : Type u} [CommRing R] {I : Ideal R} {a x : R} (hx : x ∈ I) : ↑(frac hx) = awayFrac a 1 x

theorem AlgebraicGeometry.affineBlowUpAlgebra.induction_on {R : Type u} [CommRing R] {I : Ideal R} {a : R} {p : (y : Localization.Away a) → y ∈ affineBlowUpAlgebra I a → Prop} (mem : ∀ (x : R) (hx : x ∈ I), p ((algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a) ⋯) (algebraMap : ∀ (r : R), p ((algebraMap R (Localization.Away a)) r) ⋯) (add : ∀ (y z : Localization.Away a) (hy : y ∈ affineBlowUpAlgebra I a) (hz : z ∈ affineBlowUpAlgebra I a), p y hy → p z hz → p (y + z) ⋯) (mul : ∀ (y z : Localization.Away a) (hy : y ∈ affineBlowUpAlgebra I a) (hz : z ∈ affineBlowUpAlgebra I a), p y hy → p z hz → p (y * z) ⋯) {y : Localization.Away a} (hy : y ∈ affineBlowUpAlgebra I a) : p y hy

Induction over R[I/a] along its generators x/a, the constants, sums and products.

theorem AlgebraicGeometry.affineBlowUpAlgebra.mul_invSelf_pow_mem {R : Type u} [CommRing R] {I : Ideal R} {a : R} (n : ℕ) {x : R} : x ∈ I ^ n → (algebraMap R (Localization.Away a)) x * IsLocalization.Away.invSelf a ^ n ∈ affineBlowUpAlgebra I a

x/aⁿ ∈ R[I/a] for x ∈ Iⁿ.

theorem AlgebraicGeometry.affineBlowUpAlgebra.mem_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 * (algebraMap R (Localization.Away a)) a ^ n = (algebraMap R (Localization.Away a)) x

For a ∈ I, y ∈ R[I/a] iff y · aⁿ = x in R_a for some n and x ∈ Iⁿ [TSPA, Tag 052P].

theorem AlgebraicGeometry.affineBlowUpAlgebra.algebraMap_mul_pow_eq_iff {R : Type u} [CommRing R] {a : R} (x y : R) (n m : ℕ) : (algebraMap R (Localization.Away a)) x * (algebraMap R (Localization.Away a)) a ^ m = (algebraMap R (Localization.Away a)) y * (algebraMap R (Localization.Away a)) a ^ n ↔ ∃ (k : ℕ), a ^ k * (a ^ m * x - a ^ n * y) = 0

x/aⁿ = y/aᵐ in R_a iff aᵏ(aᵐx − aⁿy) = 0 in R for some k [TSPA, Tag 052P].

Basic properties

theorem AlgebraicGeometry.affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors {R : Type u} [CommRing R] {I : Ideal R} {a : R} : (algebraMap R ↥(affineBlowUpAlgebra I a)) a ∈ nonZeroDivisors ↥(affineBlowUpAlgebra I a)

a is a nonzerodivisor of R[I/a], being a unit of R_a ⊇ R[I/a] [TSPA, Tag 07Z3].

theorem AlgebraicGeometry.affineBlowUpAlgebra.map_algebraMap_eq_span_singleton {R : Type u} [CommRing R] {I : Ideal R} {a : R} (ha : a ∈ I) : Ideal.map (algebraMap R ↥(affineBlowUpAlgebra I a)) I = Ideal.span {(algebraMap R ↥(affineBlowUpAlgebra I a)) a}

I·R[I/a] = a·R[I/a] for a ∈ I, since x = a·(x/a) for x ∈ I [TSPA, Tag 07Z3].

theorem AlgebraicGeometry.affineBlowUpAlgebra.isLocalization_away {R : Type u} [CommRing R] {I : Ideal R} {a : R} : IsLocalization.Away ((algebraMap R ↥(affineBlowUpAlgebra I a)) a) (Localization.Away a)

R[I/a]_a = R_a: the ring R_a is the localization of its subring R[I/a] at a [TSPA, Tag 07Z3].

theorem AlgebraicGeometry.affineBlowUpAlgebra.algHom_ext {R : Type u} [CommRing R] {I : Ideal R} {a : R} {A : Type v} [Semiring A] [Algebra R A] {φ ψ : ↥(affineBlowUpAlgebra I a) →ₐ[R] A} (h : ∀ (x : R) (hx : x ∈ I), φ (frac hx) = ψ (frac hx)) : φ = ψ

Two R-algebra maps out of R[I/a] agreeing on the generators x/a are equal.

The lifting lemma

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.liftAux {R : Type u} [CommRing R] {S : Type v} [CommRing S] (β : R →+* S) {f : R} : Localization.Away f →+* Localization.Away (β f)

The map R_f → S_{β(f)} induced by β on localizations.

Equations

• AlgebraicGeometry.affineBlowUpAlgebra.liftAux β = IsLocalization.Away.map (Localization.Away f) (Localization.Away (β f)) β f

theorem AlgebraicGeometry.affineBlowUpAlgebra.liftAux_algebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] (β : R →+* S) {f : R} (r : R) : (liftAux β) ((algebraMap R (Localization.Away f)) r) = (algebraMap S (Localization.Away (β f))) (β r)

theorem AlgebraicGeometry.affineBlowUpAlgebra.liftAux_mem_range {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hf : f ∈ I) (hI : Ideal.map β I = Ideal.span {β f}) (z : ↥(affineBlowUpAlgebra I f)) : (liftAux β) ↑z ∈ (algebraMap S (Localization.Away (β f))).range

The restriction of R_f → S_{β(f)} to R[I/f] lands in the image of S: for x ∈ Iⁿ, β(x) ∈ (β(I)S)ⁿ = (β(f)ⁿ), so β(x)/β(f)ⁿ comes from S.

theorem AlgebraicGeometry.affineBlowUpAlgebra.injective_algebraMap_away {R : Type u} [CommRing R] {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hβf : β f ∈ nonZeroDivisors S) : Function.Injective ⇑(algebraMap S (Localization.Away (β f)))

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.lift {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hf : f ∈ I) (hβf : β f ∈ nonZeroDivisors S) (hI : Ideal.map β I = Ideal.span {β f}) : ↥(affineBlowUpAlgebra I f) →+* S

The ring map δ : R[I/f] → S extending β, given by division by the nonzerodivisor β(f) [Hau14, Theorem 4.18, proof (d)].

Equations

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

theorem AlgebraicGeometry.affineBlowUpAlgebra.algebraMap_lift {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hf : f ∈ I) (hβf : β f ∈ nonZeroDivisors S) (hI : Ideal.map β I = Ideal.span {β f}) (z : ↥(affineBlowUpAlgebra I f)) : (algebraMap S (Localization.Away (β f))) ((lift β hf hβf hI) z) = (liftAux β) ↑z

theorem AlgebraicGeometry.affineBlowUpAlgebra.lift_comp_algebraMap {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hf : f ∈ I) (hβf : β f ∈ nonZeroDivisors S) (hI : Ideal.map β I = Ideal.span {β f}) : (lift β hf hβf hI).comp (algebraMap R ↥(affineBlowUpAlgebra I f)) = β

The lift extends β.

theorem AlgebraicGeometry.affineBlowUpAlgebra.mul_pow_of_comp_eq {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (δ : ↥(affineBlowUpAlgebra I f) →+* S) (hδ : δ.comp (algebraMap R ↥(affineBlowUpAlgebra I f)) = β) (z : ↥(affineBlowUpAlgebra I f)) (x : R) (n : ℕ) (hz : ↑z * (algebraMap R (Localization.Away f)) f ^ n = (algebraMap R (Localization.Away f)) x) : δ z * β f ^ n = β x

Every ring map δ : R[I/f] → S extending β satisfies δ(z)·β(f)ⁿ = β(x) whenever z·fⁿ = x; this is Hauser's formula δ(hₗ/fˡ) = aₗ with β(hₗ) = aₗ β(f)ˡ [Hau14, Theorem 4.18, proof (d)].

theorem AlgebraicGeometry.affineBlowUpAlgebra.lift_unique {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] (β : R →+* S) {f : R} (hf : f ∈ I) (hβf : β f ∈ nonZeroDivisors S) (hI : Ideal.map β I = Ideal.span {β f}) (δ : ↥(affineBlowUpAlgebra I f) →+* S) (hδ : δ.comp (algebraMap R ↥(affineBlowUpAlgebra I f)) = β) : δ = lift β hf hβf hI

A ring map R[I/f] → S extending β is the lift: δ is unique with this property [Hau14, Theorem 4.18, proof (d)].