Embedding an affine scheme in affine space with ambient dimension at least two

Kollár's resolution of an affine scheme X starts from a closed embedding X ↪ A into a smooth affine scheme with dim A ≥ dim X + 2 [Kol07, Theorem 36, proof; Corollary 22, proof]. An affine scheme of finite type over k whose ring of functions has n generators embeds in 𝔸^{n+2} with the last two coordinates zero; at every point the ambient local ring has dimension ≥ 2, its prime containing the kernel of the projection killing the last two variables, a prime of height ≥ 2.

• padProj, dropLast, padProj_surjective: the coordinate projections 𝔸^{n+2} → 𝔸^n and 𝔸^{n+2} → 𝔸^{n+1} on coordinate rings;
• two_le_height_of_ker_padProj_le: a prime containing ker padProj has height ≥ 2;
• exists_affineEmbedding_aux, exists_affineEmbedding: the embedding, with the dimension bound at every point, respectively at the generic points (the form used to build admissible pairs).

The coordinate projections

noncomputable def Hironaka.Resolution.padProj {k : Type u} [Field k] (n : ℕ) : MvPolynomial (Fin (n + 2)) k →ₐ[k] MvPolynomial (Fin n) k

The projection 𝔸^{n+2} → 𝔸^n on the coordinate rings: x_i ↦ x_i for i < n, the last two variables to 0.

Equations

• Hironaka.Resolution.padProj n = MvPolynomial.aeval fun (i : Fin (n + 2)) => if h : ↑i < n then MvPolynomial.X ⟨↑i, h⟩ else 0

noncomputable def Hironaka.Resolution.dropLast {k : Type u} [Field k] (n : ℕ) : MvPolynomial (Fin (n + 2)) k →ₐ[k] MvPolynomial (Fin (n + 1)) k

The projection 𝔸^{n+2} → 𝔸^{n+1} killing the last variable only.

Equations

• Hironaka.Resolution.dropLast n = MvPolynomial.aeval fun (i : Fin (n + 2)) => if h : ↑i < n + 1 then MvPolynomial.X ⟨↑i, h⟩ else 0

theorem Hironaka.Resolution.padProj_X_of_lt {k : Type u} [Field k] (n : ℕ) (i : Fin (n + 2)) (h : ↑i < n) : (padProj n) (MvPolynomial.X i) = MvPolynomial.X ⟨↑i, h⟩

theorem Hironaka.Resolution.padProj_X_of_le {k : Type u} [Field k] (n : ℕ) (i : Fin (n + 2)) (h : n ≤ ↑i) : (padProj n) (MvPolynomial.X i) = 0

theorem Hironaka.Resolution.dropLast_X_of_lt {k : Type u} [Field k] (n : ℕ) (i : Fin (n + 2)) (h : ↑i < n + 1) : (dropLast n) (MvPolynomial.X i) = MvPolynomial.X ⟨↑i, h⟩

theorem Hironaka.Resolution.dropLast_X_last {k : Type u} [Field k] (n : ℕ) : (dropLast n) (MvPolynomial.X (Fin.last (n + 1))) = 0

theorem Hironaka.Resolution.padProj_surjective {k : Type u} [Field k] (n : ℕ) : Function.Surjective ⇑(padProj n)

theorem Hironaka.Resolution.padProj_eq_comp_dropLast {k : Type u} [Field k] (n : ℕ) : padProj n = (MvPolynomial.aeval fun (j : Fin (n + 1)) => if h : ↑j < n then MvPolynomial.X ⟨↑j, h⟩ else 0).comp (dropLast n)

padProj factors through dropLast.

The height bound

theorem Hironaka.Resolution.two_le_height_of_ker_padProj_le {k : Type u} [Field k] (n : ℕ) (p : Ideal (MvPolynomial (Fin (n + 2)) k)) (hp : RingHom.ker (padProj n) ≤ p) : 2 ≤ p.height

A prime of k[x_0, …, x_{n+1}] containing the kernel of the projection killing the last two variables has height ≥ 2 (the chain ⊥ < ker dropLast < ker padProj).

The embedding

theorem Hironaka.Resolution.exists_affineEmbedding_aux {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine X] : ∃ (N : ℕ) (emb : X ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial (Fin N) k)), AlgebraicGeometry.IsClosedImmersion emb ∧ CategoryTheory.CategoryStruct.comp emb (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin N) k)))) = X ↘ AlgebraicGeometry.Spec ↧k ∧ ∀ (x : ↥X), 2 ≤ ringKrullDim ↑((AlgebraicGeometry.Spec ↧(MvPolynomial (Fin N) k)).presheaf.stalk (emb x))

An affine scheme of finite type over k embeds as a closed subscheme of 𝔸^{n+2}_k over k (n generators of its ring of functions and two zero coordinates) with the local rings of the ambient space of dimension ≥ 2 at every point, as in the proof of [Kol07, Theorem 36].

theorem Hironaka.Resolution.exists_affineEmbedding {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine X] : ∃ (N : ℕ) (emb : X ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial (Fin N) k)), AlgebraicGeometry.IsClosedImmersion emb ∧ CategoryTheory.CategoryStruct.comp emb (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k (MvPolynomial (Fin N) k)))) = X ↘ AlgebraicGeometry.Spec ↧k ∧ ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑((AlgebraicGeometry.Spec ↧(MvPolynomial (Fin N) k)).presheaf.stalk (emb η))

The embedding of exists_affineEmbedding_aux with the dimension bound stated only at the generic points of X (a special case), the form in which it enters the construction of an admissible embedding of an affine scheme.