The chart rings of the affine blow-up: (R̃_{at})₀ ≅ R[I/a] #
For g ∈ I, the degree-zero elements of the localized Rees algebra R̃_g form the ring
R[I g⁻¹] of fractions f/gˡ with f ∈ Iˡ [Hau14, Definition 4.16], and the affine chart
D₊(a t) of Proj of the Rees algebra is the spectrum of the affine blow-up algebra R[I/a]
[TSPA, Tag 0804]. This file proves the ring isomorphism behind these statements, between
Mathlib's degree-zero homogeneous localization HomogeneousLocalization.Away (grading I) (a t)
of the graded Rees algebra and the affine blow-up algebra affineBlowUpAlgebra I a ⊆ R_a.
The construction #
Evaluation at 1/a is the R-algebra map reesAlgebra I → R_a, ∑ pₙ tⁿ ↦ ∑ pₙ/aⁿ
(reesAlgebra.evalInv, Mathlib's Polynomial.aeval at IsLocalization.Away.invSelf a). It
sends a t to a · (1/a) = 1, so it extends to the localization (reesAlgebra I)_{at}
(reesAlgebra.awayLift, by IsLocalization.Away.lift) and restricts along val to the
degree-zero part (reesAlgebra.chartHom). On the fraction x tⁿ/(at)ⁿ it gives x/aⁿ
(reesAlgebra.chartHom_mk_eq_awayFrac, by the normal form of the grading), so its image lies in
R[I/a] and, by mem_affineBlowUpAlgebra_iff, is all of it. Injectivity: if x/aⁿ = 0 in
R_a then aᵏx = 0 for some k, so (at)ᵏ · x tⁿ = aᵏx · tⁿ⁺ᵏ = 0 and the fraction
x tⁿ/(at)ⁿ is already 0 in the localization of the Rees algebra. The result is
reesAlgebra.chartRingEquiv a : Away (grading I) (a t) ≃+* affineBlowUpAlgebra I a, compatible
with the constants: R → grading I 0 → Away → R[I/a] is algebraMap R R[I/a]
(reesAlgebra.chartRingEquiv_fromZeroRingHom). The ring isomorphism and the constant-map
compatibility are the two halves of "isomorphism of R-algebras": Mathlib puts no R-algebra
structure on HomogeneousLocalization, only one over grading I 0, so the ring equivalence is
built first and the compatibility with the constants proved separately.
Boundary cases #
No hypothesis on a beyond a ∈ I (carried by a : I). For a nilpotent both rings are
zero rings and the isomorphism is between singletons; for a = 1 ∈ I = R it is
(R[t]_t)₀ ≅ R.
Evaluation of the Rees algebra at 1/a: the R-algebra map reesAlgebra I → R_a,
∑ pₙ tⁿ ↦ ∑ pₙ/aⁿ.
Equations
Instances For
Evaluation at 1/a sends the monomial c tⁿ to c/aⁿ.
The ring map (reesAlgebra I)_{at} → R_a extending evaluation at 1/a, which sends the
unit at to 1.
Equations
Instances For
The chart map: the ring map from the degree-zero part (R̃_{at})₀ to R_a,
x tⁿ/(at)ⁿ ↦ x/aⁿ (reesAlgebra.chartHom_mk_eq_awayFrac).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chart map sends x tⁿ/(at)ⁿ to x/aⁿ.
The image of the chart map lies in R[I/a] (the normal form of the grading and
Away.mk_surjective).
Injectivity of the chart map: if x/aⁿ = 0 in R_a then aᵏx = 0 for some k, so (at)ᵏ
kills x tⁿ and the fraction vanishes in (R̃_{at})₀.
The chart ring isomorphism (R̃_{at})₀ ≃+* R[I/a], x tⁿ/(at)ⁿ ↦ x/aⁿ
[Hau14, Definition 4.16]; [TSPA, Tags 0804 and 052P].
Equations
Instances For
The val of a constant of degree zero in the homogeneous localization is the constant.
Compatibility with the constants: R → grading I 0 → (R̃_{at})₀ → R_a is algebraMap R R_a;
with reesAlgebra.chartRingEquiv this is the statement that the chart ring isomorphism is one of
R-algebras.