Base change of the affine blow-up algebra

For a ring map R → S, J = IS and b the image of a, the induced map R[I/a] → S[J/b] and the S-algebra map S ⊗[R] R[I/a] → S[J/b], which is surjective with kernel the b-power torsion [TSPA, Tag 0BIP], and is an isomorphism when S is flat over R (the ring-level form of the compatibility of blow-ups with flat base change [TSPA, Tag 0805]: flatness preserves the injectivity of multiplication by a).

Main declarations

• AlgebraicGeometry.awayMapₐ S a : Localization.Away a →ₐ[R] Localization.Away (algebraMap R S a), the map of localizations induced by R → S.
• affineBlowUpAlgebra.baseChangeHom I a S : R[I/a] →ₐ[R] S[IS/b] with baseChangeHom_frac and baseChangeHom_unique.
• affineBlowUpAlgebra.tensorHom I a S : S ⊗[R] R[I/a] →ₐ[S] S[IS/b] with tensorHom_tmul_frac, tensorHom_unique, tensorHom_surjective, tensorHom_apply_eq_zero_iff and tensorHom_bijective_of_flat.

The arguments

The induced map. R_a → S_b sends x/a to (image of x)/b, so it maps the generators of R[I/a] into S[J/b].

Surjectivity. S[J/b] is generated over S by the y/b, y ∈ J = IS, and y = ∑ sᵢ (image of xᵢ) gives y/b = ∑ sᵢ · (image of xᵢ)/b, the image of ∑ sᵢ ⊗ xᵢ/a.

Kernel. Every element w of S ⊗[R] R[I/a] satisfies bⁿ w = p ⊗ 1 for some n and p ∈ S: for a pure tensor s ⊗ z with z aⁿ = r in R_a (z ∈ R[I/a] ⊆ R_a) one has bⁿ (s ⊗ z) = s ⊗ aⁿ z = s ⊗ r = (image of r) s ⊗ 1, and the property is additive. If w maps to 0 then p maps to 0 in S_b, so bᵏ p = 0 and bⁿ⁺ᵏ w = 0. Conversely b is a nonzerodivisor of S[J/b] (affineBlowUpAlgebra.algebraMap_mem_nonZeroDivisors), so b-power torsion maps to 0. The Stacks Project proves the kernel statement by constructing the inverse map on S[J/b]; the common-denominator computation above is the same identity bⁿ (s ⊗ x/aⁿ) = s x ⊗ 1 read forwards.

Flat case. If S is flat over R, multiplication by a on R[I/a] (injective) stays injective after S ⊗[R] -, and it is multiplication by b on the tensor product; so the b-power torsion vanishes and the surjection is bijective.

Conventions

No hypothesis a ∈ I is needed ([TSPA, Tag 0BIP] assumes it; it is not used here). The b-power torsion of the S-module S ⊗[R] R[I/a] is written ∃ k, bᵏ • w = 0.

Boundary cases

S = 0: both sides are the zero ring. a = 0: S[J/0] is the zero ring and every w is 0-power torsion (0¹ • w = 0), consistently.

noncomputable def AlgebraicGeometry.awayMapₐ {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) : Localization.Away a →ₐ[R] Localization.Away ((algebraMap R S) a)

The map R_a → S_b induced by R → S on localizations, as an R-algebra map.

Equations

• AlgebraicGeometry.awayMapₐ S a = IsLocalization.Away.liftAlgHom a ⋯

theorem AlgebraicGeometry.awayMapₐ_algebraMap {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a r : R) : (awayMapₐ S a) ((algebraMap R (Localization.Away a)) r) = (algebraMap S (Localization.Away ((algebraMap R S) a))) ((algebraMap R S) r)

theorem AlgebraicGeometry.awayMapₐ_invSelf {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) : (awayMapₐ S a) (IsLocalization.Away.invSelf a) = IsLocalization.Away.invSelf ((algebraMap R S) a)

theorem AlgebraicGeometry.affineBlowUpAlgebra.awayMapₐ_mem {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (z : ↥(affineBlowUpAlgebra I a)) : (awayMapₐ S a) ↑z ∈ affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a)

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.baseChangeHom {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) : ↥(affineBlowUpAlgebra I a) →ₐ[R] ↥(affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a))

The induced map R[I/a] → S[IS/b], x/a ↦ (image of x)/b [TSPA, Tag 0BIP].

Equations

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

@[simp]

theorem AlgebraicGeometry.affineBlowUpAlgebra.coe_baseChangeHom {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (z : ↥(affineBlowUpAlgebra I a)) : ↑((baseChangeHom S a I) z) = (awayMapₐ S a) ↑z

theorem AlgebraicGeometry.affineBlowUpAlgebra.baseChangeHom_frac {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) {x : R} (hx : x ∈ I) : (baseChangeHom S a I) (frac hx) = frac ⋯

theorem AlgebraicGeometry.affineBlowUpAlgebra.baseChangeHom_unique {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (ψ : ↥(affineBlowUpAlgebra I a) →ₐ[R] ↥(affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a))) (hψ : ∀ (x : R) (hx : x ∈ I), ψ (frac hx) = frac ⋯) : ψ = baseChangeHom S a I

The induced map is the unique R-algebra map with x/a ↦ (image of x)/b.

noncomputable def AlgebraicGeometry.affineBlowUpAlgebra.tensorHom {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) : TensorProduct R S ↥(affineBlowUpAlgebra I a) →ₐ[S] ↥(affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a))

The S-algebra map S ⊗[R] R[I/a] → S[IS/b] [TSPA, Tag 0BIP].

Equations

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

@[simp]

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_tmul {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (s : S) (z : ↥(affineBlowUpAlgebra I a)) : (tensorHom S a I) (s ⊗ₜ[R] z) = (algebraMap S ↥(affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a))) s * (baseChangeHom S a I) z

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_tmul_frac {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) {x : R} (hx : x ∈ I) : (tensorHom S a I) (1 ⊗ₜ[R] frac hx) = frac ⋯

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_unique {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (Ψ : TensorProduct R S ↥(affineBlowUpAlgebra I a) →ₐ[S] ↥(affineBlowUpAlgebra (Ideal.map (algebraMap R S) I) ((algebraMap R S) a))) (hΨ : ∀ (x : R) (hx : x ∈ I), Ψ (1 ⊗ₜ[R] frac hx) = frac ⋯) : Ψ = tensorHom S a I

The tensor map is the unique S-algebra map with 1 ⊗ x/a ↦ (image of x)/b.

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_surjective {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) : Function.Surjective ⇑(tensorHom S a I)

S ⊗[R] R[I/a] → S[IS/b] is surjective [TSPA, Tag 0BIP].

theorem AlgebraicGeometry.affineBlowUpAlgebra.exists_pow_smul_eq_tmul_one {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (w : TensorProduct R S ↥(affineBlowUpAlgebra I a)) : ∃ (n : ℕ) (p : S), (algebraMap R S) a ^ n • w = p ⊗ₜ[R] 1

Common denominators: bⁿ • w = p ⊗ 1 for some n and p ∈ S.

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_apply_eq_zero_iff {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (w : TensorProduct R S ↥(affineBlowUpAlgebra I a)) : (tensorHom S a I) w = 0 ↔ ∃ (k : ℕ), (algebraMap R S) a ^ k • w = 0

The kernel of S ⊗[R] R[I/a] → S[IS/b] is the b-power torsion [TSPA, Tag 0BIP].

theorem AlgebraicGeometry.affineBlowUpAlgebra.smul_eq_lTensor_mulLeft {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) (w : TensorProduct R S ↥(affineBlowUpAlgebra I a)) : (algebraMap R S) a • w = (LinearMap.lTensor S (LinearMap.mulLeft R ((algebraMap R ↥(affineBlowUpAlgebra I a)) a))) w

Multiplication by b on S ⊗[R] R[I/a] is S ⊗ (multiplication by aonR[I/a]).

theorem AlgebraicGeometry.affineBlowUpAlgebra.tensorHom_bijective_of_flat {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] (a : R) (I : Ideal R) [Module.Flat R S] : Function.Bijective ⇑(tensorHom S a I)

The flat case: for S flat over R, S ⊗[R] R[I/a] → S[IS/b] is an isomorphism, because multiplication by a on R[I/a] is injective and stays injective after S ⊗[R] - (the ring-level form of the compatibility of blow-ups with flat base change [TSPA, Tag 0805]).