Two embeddings into affine space are conjugate by an automorphism #
[Kol07, Lemma 39]: for closed embeddings i₁ : X ↪ 𝔸ⁿ and i₂ : X ↪ 𝔸ᵐ of an affine scheme, the
two embeddings X ↪ 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ and X ↪ 𝔸ᵐ ↪ 𝔸ⁿ⁺ᵐ into the coordinate subspaces are equivalent
under a (nonlinear) automorphism of 𝔸ⁿ⁺ᵐ. Kollár's proof: extend i₂ to j₂ : 𝔸ⁿ → 𝔸ᵐ (lift
the coordinate functions y_l ∘ i₂ along the surjection k[x] → 𝒪(X)); then the shear
(x, y) ↦ (x, y + j₂(x)) carries (i₁, 0) to i₁ × i₂, and symmetrically the shear
(x, y) ↦ (x + j₁(y), y) carries (0, i₂) to i₁ × i₂. The main results:
hom_ext_affineSpace: two morphismsX ⟶ 𝔸ᴺagree once they agree on the constants and on the coordinate functions (Mathlib'sext_of_isAffineandMvPolynomial.ringHom_extthroughΓSpecIso); every identity of the lemma is checked this way.exists_polynomialMap_comp_eq: the extensionsj₁,j₂, from the surjectivity of the coordinate ring map of a closed immersion between affine schemes.shearY_comp_prodEmb,shearX_comp_prodEmb: the two shears carry the coordinate embeddings to the product embeddingprodEmb i₁ i₂.exists_aut_conj_embeddings: the lemma, with the automorphismshearY v ≫ inv (shearX w).
The lemma is the step of the proof of [Kol07, Theorem 36] that makes the resolution of an affine
scheme independent of the embedding; see Hironaka.Resolution.Algebraic.Kol07.Thm36.Assembly.
Global sections of morphisms into an affine scheme #
The global sections of Spec.map φ, read through ΓSpecIso, are φ
(ΓSpecIso_inv_naturality pointwise).
Two morphisms from a scheme into the affine space 𝔸ᴺ_k agree once they agree on the constants
and on the coordinate functions (through ΓSpecIso): Mathlib's ext_of_isAffine and
MvPolynomial.ringHom_ext.
The global sections of a polynomial map on a constant.
The global sections of a polynomial map on a coordinate: y_l ↦ v_l.
The global sections of a polynomial map on any polynomial: substitution.
The global sections of the structure morphism of 𝔸ⁿ_k on a scalar: the constant polynomial.
The global sections of the product embedding on a constant: the structure morphism's.
The global sections of the product embedding on a coordinate of the first block: i₁'s.
The global sections of the product embedding on a coordinate of the second block: i₂'s.
The coordinate inclusions on polynomials #
Substituting the coordinate inclusion x ↦ (x, 0) into a polynomial renamed into the first
block gives the polynomial back.
Substituting the coordinate inclusion y ↦ (0, y) into a polynomial renamed into the second
block gives the polynomial back.
Morphisms over k on constants #
A morphism i : X ⟶ 𝔸ⁿ over k sends the constant c to the structure morphism's c.
The lifts j₁, j₂ #
The extension step of the proof of [Kol07, Lemma 39] ("we can extend i₂ to a morphism
j₂ : 𝔸ⁿ → 𝔸ᵐ"): for a closed immersion i₁ : X ↪ 𝔸ⁿ over k and any morphism i₂ : X ⟶ 𝔸ᵐ
over k, there is a polynomial map 𝔸ⁿ ⟶ 𝔸ᵐ through which i₂ factors: each coordinate
function y_l ∘ i₂ lifts along the surjective coordinate ring map of the closed immersion i₁.
The two shears carry the coordinate embeddings to the product embedding #
The shear (x, y) ↦ (x, y + j₂(x)) carries (i₁, 0) to i₁ × i₂ when j₂ = polynomialMap v
extends i₂ along i₁ [Kol07, Lemma 39, proof].
The shear (x, y) ↦ (x + j₁(y), y) carries (0, i₂) to i₁ × i₂ when j₁ = polynomialMap w
extends i₁ along i₂ [Kol07, Lemma 39, proof].
[Kol07, Lemma 39]: for two closed immersions i₁ : X ↪ 𝔸ⁿ, i₂ : X ↪ 𝔸ᵐ over k, the two
coordinate embeddings X ↪ 𝔸ⁿ⁺ᵐ are conjugate under an automorphism of 𝔸ⁿ⁺ᵐ over k, namely
shearY v ≫ inv (shearX w), each shear carrying its coordinate embedding to prodEmb i₁ i₂.