Affine space over k: polynomial maps, coordinate inclusions and shears #
Kollár proves that the resolution of an affine scheme X does not depend on the embedding
X ↪ A by passing to embeddings into affine spaces X ↪ 𝔸ⁿ, enlarging n at will along the
coordinate inclusion 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ, and conjugating two embeddings by a nonlinear automorphism
of 𝔸ⁿ⁺ᵐ [Kol07, Theorem 36, proof; Lemma 39]. This file defines the affine-space morphisms
those arguments use; the identities between them are proved in
Hironaka.Resolution.Algebraic.Kol07.Thm36.Shear and
Hironaka.Resolution.Algebraic.Kol07.Thm36.Lemma39.
Main definitions #
polynomialMap v : 𝔸ⁿ ⟶ 𝔸ᵐ, the morphismx ↦ (v₁(x), …, v_m(x))given bympolynomials innvariables (Spec.mapof the evaluation homomorphismaeval v); Kollár's extensionsj₁,j₂of the embeddings are such maps.coordInclFst n m : 𝔸ⁿ ⟶ 𝔸ⁿ⁺ᵐ,x ↦ (x, 0), andcoordInclSnd n m : 𝔸ᵐ ⟶ 𝔸ⁿ⁺ᵐ,y ↦ (0, y), the embeddings of the two coordinate subspaces, closed immersions overk.shearY v : 𝔸ⁿ⁺ᵐ ⟶ 𝔸ⁿ⁺ᵐ,(x, y) ↦ (x, y + v(x)), andshearX w,(x, y) ↦ (x + w(y), y), the two automorphisms of the proof of [Kol07, Lemma 39]; their inverses areshearY (-v)andshearX (-w).prodEmb i₁ i₂ : X ⟶ 𝔸ⁿ⁺ᵐ, Kollár'si₁ × i₂ : X → 𝔸ⁿ × 𝔸ᵐfor a schemeXoverk, defined on coordinate rings: the coordinatex_ipulls back toi₁^♯ x_i, the coordinatey_ltoi₂^♯ y_l, and the constants to the structure morphism's (no scheme product is formed).affineSpaceTriple k n I hI : Triple k, the triple(𝔸ⁿ_k, I, ∅)for an ideal sheafIon𝔸ⁿ_knonzero on every irreducible component, the ambient of Kollár'sBP(𝔸ⁿ, I_X, ∅).
Conventions #
𝔸ᴺ_k is Spec k[Fin N] with structure morphism AlgebraicGeometry.affineSpaceToSpec k N. In
𝔸ⁿ⁺ᵐ = Spec k[Fin (n + m)] the first block of coordinates (Kollár's x) is indexed through
finSumFinEquiv (Sum.inl i) and the second block (Kollár's y) through
finSumFinEquiv (Sum.inr l); coordX and coordY name the two blocks as polynomials.
Polynomial maps between affine spaces #
The morphism 𝔸ⁿ ⟶ 𝔸ᵐ given by m polynomials v₁, …, v_m in the n coordinates,
x ↦ (v₁(x), …, v_m(x)): Spec.map of the evaluation homomorphism y_l ↦ v_l. Kollár's
extensions j₁ : 𝔸ᵐ → 𝔸ⁿ of i₁ and j₂ : 𝔸ⁿ → 𝔸ᵐ of i₂ in the proof of [Kol07, Lemma 39]
are morphisms of this form.
Equations
Instances For
A polynomial map is a morphism over k.
The coordinate subspaces 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ, 𝔸ᵐ ↪ 𝔸ⁿ⁺ᵐ #
The first block of coordinates of 𝔸ⁿ⁺ᵐ (Kollár's x), as polynomials in n + m
variables.
Equations
- Hironaka.Resolution.coordX n m i = MvPolynomial.X (finSumFinEquiv (Sum.inl i))
Instances For
The second block of coordinates of 𝔸ⁿ⁺ᵐ (Kollár's y), as polynomials in n + m
variables.
Equations
- Hironaka.Resolution.coordY n m l = MvPolynomial.X (finSumFinEquiv (Sum.inr l))
Instances For
The closed immersion 𝔸ⁿ ⟶ 𝔸ⁿ⁺ᵐ, x ↦ (x, 0), onto the first coordinate subspace: the
polynomial map sending the first block of coordinates to the coordinates of 𝔸ⁿ and the second
block to 0. It is the "further embedding 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ" of the proof of [Kol07, Theorem 36] and
the first of the two coordinate subspaces of [Kol07, Lemma 39].
Equations
- Hironaka.Resolution.coordInclFst n m = Hironaka.Resolution.polynomialMap fun (j : Fin (n + m)) => Sum.elim MvPolynomial.X (fun (x : Fin m) => 0) (finSumFinEquiv.symm j)
Instances For
The closed immersion 𝔸ᵐ ⟶ 𝔸ⁿ⁺ᵐ, y ↦ (0, y), onto the second coordinate subspace.
Equations
- Hironaka.Resolution.coordInclSnd n m = Hironaka.Resolution.polynomialMap fun (j : Fin (n + m)) => Sum.elim (fun (x : Fin n) => 0) MvPolynomial.X (finSumFinEquiv.symm j)
Instances For
The evaluation defining coordInclFst is surjective: x_i is the image of the coordinate
coordX n m i.
The evaluation defining coordInclSnd is surjective.
The coordinate inclusion 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ is a closed immersion: its coordinate ring map is
surjective.
The coordinate inclusion 𝔸ᵐ ↪ 𝔸ⁿ⁺ᵐ is a closed immersion.
The two shears of Lemma 39 #
The shear of 𝔸ⁿ⁺ᵐ along the second block by m polynomials v in the coordinates of the
first block: the polynomial map fixing x and sending y_l ↦ y_l + v_l(x). Its inverse is
shearY (-v) (Hironaka.Resolution.isIso_shearY). This is the automorphism
(x, y) ↦ (x, y + j₂(x)) of the proof of [Kol07, Lemma 39].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The shear of 𝔸ⁿ⁺ᵐ along the first block by n polynomials w in the coordinates of the
second block: the polynomial map fixing y and sending x_i ↦ x_i + w_i(y). Its inverse is
shearX (-w) (Hironaka.Resolution.isIso_shearX). This is the automorphism
(x, y) ↦ (x + j₁(y), y) of the proof of [Kol07, Lemma 39].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product embedding i₁ × i₂ #
For a scheme X over k and two morphisms i₁ : X ⟶ 𝔸ⁿ, i₂ : X ⟶ 𝔸ᵐ, the morphism
X ⟶ 𝔸ⁿ⁺ᵐ whose first block of coordinates is i₁'s and whose second block is i₂'s: on
coordinate rings, the homomorphism k[Fin (n + m)] → Γ(X, ⊤) sending x_i ↦ i₁^♯ x_i,
y_l ↦ i₂^♯ y_l and the constants to the structure morphism's, composed with X.toSpecΓ. This
is Kollár's i₁ × i₂ : X → 𝔸ⁿ × 𝔸ᵐ in the proof of [Kol07, Lemma 39]; no scheme product
𝔸ⁿ ×_k 𝔸ᵐ is formed, 𝔸ⁿ⁺ᵐ standing in for it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triple (𝔸ⁿ_k, I, ∅) #
The structure morphism 𝔸ⁿ_k → Spec k is smooth of relative dimension n, as an instance:
the affine space is the ambient of Kollár's BP(𝔸ⁿ, I_X, ∅), a triple in the sense of
[Kol07, Notation 64].
The structure morphism 𝔸ⁿ_k → Spec k is smooth.
The triple (𝔸ⁿ_k, I, ∅) [Kol07, Notation 64] for an ideal sheaf I on 𝔸ⁿ_k with nonzero
stalk at every point (IsNonzeroEverywhere; on the integral 𝔸ⁿ_k this is Kollár's "nonzero on
every irreducible component"): the structure morphism affineSpaceToSpec k n is smooth of relative
dimension n, and the empty boundary has simple normal crossings. It is the ambient of the
principalization BP(𝔸ⁿ, I_X, ∅) in the proof of [Kol07, Theorem 36].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triple (𝔸ⁿ_k, I, ∅) has an affine ambient.
The empty boundary of (𝔸ⁿ_k, I, ∅) has empty index type.