The affine charts of the blowup algebra

Let I be an ideal of a commutative ring R and a ∈ I. Then a gives an element a t of degree one of the Rees algebra R[It], and the standard affine open D₊(a t) of Proj R[It], the blowup of Spec R along V(I), is the spectrum of the homogeneous localization R[It]_(a t), the ring of degree zero fractions (b tⁿ)/(a t)ⁿ with b ∈ Iⁿ.

This file identifies that ring with the affine blowup algebra R[I/a] of TauCeti/RingTheory/Ideal/AffineBlowup.lean, the subalgebra of R_a generated by the fractions i/a with i ∈ I: the fraction (b tⁿ)/(a t)ⁿ corresponds to b/aⁿ. Thus the explicit algebras R[I/a] are the coordinate rings of the charts of the blowup.

Main definitions

• reesAlgebra.awayEquivAffineBlowup S ha: the isomorphism R[It]_(a t) ≃ₐ[R] R[I/a], for a localization S of R away from a.

Main results

• reesAlgebra.algebraMap_pow_mul_awayEquivAffineBlowup_mk: the fraction x/(a t)ⁿ, with x homogeneous of degree n, corresponds to the fraction b/aⁿ of S, where b is the coefficient of x.
• reesAlgebra.awayEquivAffineBlowup_apply_mk_monomialDegreeOne: the fraction (i t)/(a t) corresponds to the generator i/a of R[I/a].

References

• The Stacks Project, Section Blowing up, in particular Lemma 0804 for the affine charts.

noncomputable def reesAlgebra.awayEquivAffineBlowup {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.Away a S] (ha : a ∈ I) : HomogeneousLocalization.Away (grade I) (monomialDegreeOne ha) ≃ₐ[R] ↥(I.affineBlowup a S)

The affine charts of the blowup. For a ∈ I, the homogeneous localization R[It]_(a t) of the Rees algebra, the coordinate ring of the standard affine open D₊(a t) of Proj R[It], is isomorphic to the affine blowup algebra R[I/a]; the fraction x/(a t)ⁿ corresponds to b/aⁿ, where x = b tⁿ. The isomorphism preserves coefficients from R.

Equations

• reesAlgebra.awayEquivAffineBlowup S ha = AlgEquiv.ofBijective ((reesAlgebra.awayToLocalization✝ S ha).codRestrict (I.affineBlowup a S) ⋯) ⋯

theorem reesAlgebra.algebraMap_pow_mul_awayEquivAffineBlowup_mk {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.Away a S] (ha : a ∈ I) {n : ℕ} {x : ↥(reesAlgebra I)} (hx : x ∈ grade I (n • 1)) : (algebraMap R S) a ^ n * ↑((awayEquivAffineBlowup S ha) (HomogeneousLocalization.Away.mk (grade I) ⋯ n x hx)) = (algebraMap R S) ((↑x).coeff n)

The fraction x/(a t)ⁿ, for x = b tⁿ homogeneous of degree n, corresponds to the element b/aⁿ of R[I/a].

@[simp]

theorem reesAlgebra.awayEquivAffineBlowup_apply_mk_monomialDegreeOne {R : Type u_1} [CommRing R] {I : Ideal R} {a : R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.Away a S] (ha : a ∈ I) {i : R} (hi : i ∈ I) : (awayEquivAffineBlowup S ha) (HomogeneousLocalization.Away.mk (grade I) ⋯ 1 (monomialDegreeOne hi) ⋯) = ⟨TauCeti.Localization.divBy i a, ⋯⟩

The fraction (i t)/(a t) corresponds to the generator i/a of R[I/a].