The chart transitions of the model blow-up #
The charts U_j and U_ℓ of B_L 𝔸ⁿ_A are glued along the transition map x_i ↦ x_i/x_ℓ
(i ∈ J ∖ {j, ℓ}), x_j ↦ 1/x_ℓ, x_ℓ ↦ x_j x_ℓ, x_i ↦ x_i (i ∉ J) [Hau14, Definition 4.12];
Hauser prints the first line as x_i ↦ x_i/x_j, the formula for the opposite direction, and the
form used here is the one for the coordinates of U_ℓ as functions on D(x_ℓ) ⊆ U_j. Since the
blow-up is already glued (Mathlib's Proj of the Rees algebra), the statement is the
compatibility Spec (A[x] → A[x]_{x_ℓ}) ≫ U_j = Spec (τ_{jℓ}) ≫ U_ℓ on the overlap D(x_ℓ) ⊆ U_j
(modelTransition_spec). The proof goes through Mathlib's chart of D₊(f g), f = x_j t,
g = x_ℓ t (Proj.SpecMap_awayMap_awayι: the chart of f g is the chart of f restricted along
awayMap, and likewise for g): the ring (R̃_{fg})₀ is the localization of (R̃_f)₀ ≃ A[x] at
g/f ↦ x_ℓ (Away.isLocalization_mul), which identifies it with A[x]_{x_ℓ} (θ); under θ the
restriction from the chart of f is the localization map (by construction), and the restriction
from the chart of g is Hauser's τ_{jℓ} — checked on the generators of (R̃_g)₀ ≃ A[x], where
the only computation is (x_i t / x_ℓ t) · (x_ℓ t / x_j t) = x_i t / x_j t in (R̃_{fg})₀.
The generator x_j as an element of the center ideal.
Equations
- Hironaka.BlowUp.CoordinateSubspace.genX A n r j hj = ⟨MvPolynomial.X j, ⋯⟩
Instances For
The chart ring of x_j, (R̃_{x_j t})₀ ≃ A[x], through the chart of the affine blow-up and the
identification of Hironaka.Scheme.BlowUp.Model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
chartAwayEquiv on the fraction x_i t / x_j t: the variable x_i (i < r, i ≠ j).
chartAwayEquiv on a constant p ∈ R: the chart map π_j applied to p.
mul_comm stated over [CommRing R], so that both sides carry the Mul instance path of a
CommRing binder — the path in the statements of Mathlib's Proj lemmas. (Elaborating
mul_comm itself against such a statement on the Rees algebra, a Subalgebra of A[x][t],
unifies the CommMagma path with the ring path and times out at the pinned Mathlib version.)
Mathlib's Proj.SpecMap_awayMap_awayι with the membership x ∈ 𝒜 (m + m') taken as a
hypothesis instead of transported along hx (hx ▸ SetLike.mul_mem_graded f_deg g_deg). Stated
for variables f g x; instantiated at the generators of the Rees algebra its conclusion carries no
cast. At the pinned Mathlib version the kernel, before using proof irrelevance on a stuck
hx ▸ _, tries to reduce it by K-reduction, which tests x ≡ f * g definitionally — for products
of the degree-one generators of the Rees algebra that test unfolds through Polynomial,
AddMonoidAlgebra and Finsupp and does not finish.
Commutation of the two degree-one generators x_j t, x_ℓ t of the Rees algebra.
The overlap chart ring (R̃_{fg})₀, f = x_j t, g = x_ℓ t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The overlap chart ring as the localization of the chart ring of x_j at t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identification of the overlap chart ring with A[x]_{x_ℓ} (the functions on
D(x_ℓ) ⊆ U_j).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left-hand side of the gluing identity, written through θ and the restriction from the
chart of x_j to the chart of f g.
θ on the constants of the overlap chart ring: through the chart ring of x_j.
The key computation in the overlap chart ring:
(x_i t / x_ℓ t) · (x_ℓ t / x_j t) = x_i t / x_j t.
θ on the image of the ratio x_i t / x_ℓ t of the chart ring of x_ℓ: x_i / x_ℓ for
i ≠ j, and 1/x_ℓ for i = j.
The core: under θ, the restriction from the chart of x_ℓ to the overlap is
Hauser's transition map, checked on the generators of the chart ring (R̃_{x_ℓ t})₀ ≃ A[x].
The left-hand side of the gluing identity through the chart of f g.
The right factorization at the level of CommRingCat morphisms.
The right-hand side, rewritten through the chart of x_ℓ.
The right-hand side, through the overlap chart ring (first half).
The chart of x_ℓ restricted to the overlap is the chart of f g (Mathlib's
Proj.SpecMap_awayMap_awayι, instantiated).
The gluing of the charts U_j and U_ℓ along the transition map [Hau14, Definition 4.12]:
on the overlap D(x_ℓ) ⊆ U_j the charts U_j and U_ℓ agree through τ_{jℓ}, which verifies the
transition formula in the form stated in Hironaka.Scheme.BlowUp.CoordinateSubspace.Charts.