The model case: blowing up a coordinate subspace #
For R = A[xᵢ : i ∈ σ], I = (xᵢ : i ∈ S) and j ∈ S, the chart R[I/xⱼ] is again a polynomial
ring over A in the variables σ, via xᵢ/xⱼ ↦ xᵢ for i ∈ S, i ≠ j, xⱼ ↦ xⱼ and xᵢ ↦ xᵢ
for i ∉ S; under this identification the inclusion R → R[I/xⱼ] is Hauser's chart map πⱼ:
xᵢ ↦ xᵢ xⱼ for i ∈ S, i ≠ j, and xᵢ ↦ xᵢ otherwise Hau14, Definition 4.12 and
Example 4.42.
Main declarations #
Hironaka.BlowUp.affineBlowUpAlgebra.coordinateSubspaceEquiv A S j : affineBlowUpAlgebra (Ideal.span (X '' S)) (X (R := A) j) ≃ₐ[A] MvPolynomial σ A, withcoordinateSubspaceEquiv_frac,coordinateSubspaceEquiv_algebraMap_X_of_mem,coordinateSubspaceEquiv_algebraMap_X_of_notandcoordinateSubspaceEquiv_unique.
The argument #
Let L = R[1/xⱼ]. The A-algebra map α : A[xᵢ] → L, xᵢ ↦ xᵢ/xⱼ (i ∈ S, i ≠ j),
xᵢ ↦ xᵢ otherwise, and the chart map γ : A[xᵢ] → R → L, xᵢ ↦ xᵢ xⱼ (i ∈ S, i ≠ j),
xᵢ ↦ xᵢ otherwise, both send xⱼ to the unit xⱼ of L and so extend to endomorphisms
α', γ' of L, which are inverse to each other (check on the generators: α'γ'(xᵢ) = (xᵢ/xⱼ) xⱼ = xᵢ and γ'α'(xᵢ) = (xᵢ xⱼ)/xⱼ = xᵢ). Hence α' is bijective, and α = α' ∘ (R → L)
is injective because xⱼ is a nonzerodivisor of the polynomial ring. The image of α is
R[I/xⱼ]: its generators land there, and conversely R[I/xⱼ] is generated over R by the
xᵢ/xⱼ = α(xᵢ), i ∈ S, while R itself is the image of γ, i.e. α ∘ (substitution). So
α is an isomorphism of A[xᵢ] onto R[I/xⱼ], and the equivalence is its inverse
[Hau14, Example 4.42].
Conventions #
The variable type σ and the centre S ⊆ σ are arbitrary (Hauser has n variables and
S = {1, …, k}); the proofs do not use finiteness. The hypothesis j ∈ S of the source is not
used by the construction (for j ∉ S the same map is still an isomorphism, with xⱼ ∉ I).
Boundary cases #
S = {j}: I = (xⱼ) and R[I/xⱼ] ≃ R is the identity on the variables. S = univ: every
variable except xⱼ becomes a ratio. A = 0: everything is the zero ring.
Two A-algebra maps out of R[I/a], for an A-algebra R, agreeing on the image of R and
on the generators x/a are equal.
The centre I = (xᵢ : i ∈ S).
Equations
Instances For
The substitution xᵢ ↦ xᵢ xⱼ (i ∈ S, i ≠ j), xᵢ ↦ xᵢ otherwise: Hauser's chart map
πⱼ [Hau14, Definition 4.12] on the polynomial ring.
Equations
- AlgebraicGeometry.affineBlowUpAlgebra.chartSubst A S j = MvPolynomial.aeval fun (i : σ) => if i ∈ S ∧ i ≠ j then MvPolynomial.X i * MvPolynomial.X j else MvPolynomial.X i
Instances For
The map α : A[xᵢ] → R[1/xⱼ], xᵢ ↦ xᵢ/xⱼ (i ∈ S, i ≠ j), xᵢ ↦ xᵢ otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
α ∘ πⱼ is the localization map R → R[1/xⱼ].
The extension of α to an endomorphism of R[1/xⱼ].
Equations
Instances For
The extension of πⱼ to an endomorphism of R[1/xⱼ].
Equations
Instances For
α is injective: xⱼ is a nonzerodivisor of the polynomial ring, and α extends to the
automorphism α' of R[1/xⱼ].
α with values in R[I/xⱼ].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chart R[I/xⱼ] of the blow-up of A[xᵢ : i ∈ σ] along (xᵢ : i ∈ S) is the polynomial
ring A[xᵢ : i ∈ σ], via xᵢ/xⱼ ↦ xᵢ for i ∈ S, i ≠ j [Hau14, Example 4.42].
Equations
Instances For
xᵢ/xⱼ ↦ xᵢ for i ∈ S, i ≠ j.
Under the identification, the inclusion R → R[I/xⱼ] is xᵢ ↦ xᵢ xⱼ for i ∈ S, i ≠ j:
Hauser's chart map πⱼ [Hau14, Definition 4.12].
The inclusion R → R[I/xⱼ] is xᵢ ↦ xᵢ for i = j and for i ∉ S.
The identification is the unique A-algebra isomorphism with the values of
[Hau14, Example 4.42] on the variables.