Every affine scheme of finite type has an admissible embedding

The resolution of an affine scheme is defined through an admissible embedding (TA, emb) (Hironaka.Resolution.Algebraic.Kol07.Thm36.Independence): a closed immersion over k into the ambient of a triple with affine ambient and empty boundary, whose ideal is the kernel of the embedding. To use that definition one needs such a pair to exist, and a triple asks for more than a closed immersion into an affine scheme: its ideal must be nonzero in every stalk, so that its principalization sequence is a genuine one (condition (2) of [Kol07, Notation 64]).

The construction, after "pick any embedding X ↪ A into a smooth affine scheme" Kol07, Theorem 36, proof: embed X into 𝔸^N_k (exists_closedImmersion_affineSpace_of_isAffine, from the finite type of the ring of global sections), then into 𝔸^{N+1}_k through the coordinate hyperplane coordInclFst N 1. The kernel of the composite X ↪ 𝔸^{N+1} contains the last coordinate x_{N+1}, a nonzero global section of the integral scheme 𝔸^{N+1}, so it is nonzero in every stalk; affineSpaceTriple k (N+1) _ _ is then the admissible ambient.

• ker_coordInclFst_ideal_top_ne_bot: the last coordinate lies in the kernel of the coordinate hyperplane, read on global sections through ΓSpecIso and MvPolynomial.aeval.
• isNonzeroEverywhere_ker_comp_coordInclFst: the kernel of ι ≫ coordInclFst N 1 is nonzero in every stalk (Scheme.Hom.le_ker_comp, integrality of 𝔸^{N+1}).
• exists_admissibleEmbedding: the admissible pair.
• exists_admissibleEmbedding_of_codim: an admissible pair whose ambient has Krull dimension ≥ 2 at the image of every generic point of X (exists_affineEmbedding composed with the coordinate hyperplane), the hypothesis of the clauses of Theorem 36 for the affine resolution.

These pairs are used to evaluate the affine resolution BRAffine (Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) and to derive its functoriality (Hironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent).

theorem Hironaka.Resolution.ker_coordInclFst_ideal_top_ne_bot {k : Type u} [Field k] (N : ℕ) : (AlgebraicGeometry.Scheme.Hom.ker (coordInclFst N 1)).ideal ⟨⊤, ⋯⟩ ≠ ⊥

The last coordinate of 𝔸^{N+1} vanishes on the coordinate hyperplane 𝔸^N: the kernel of coordInclFst N 1 has nonzero global sections.

theorem Hironaka.Resolution.isNonzeroEverywhere_ker_comp_coordInclFst {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} {N : ℕ} (ι : X ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial (Fin N) k)) : (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp ι (coordInclFst N 1))).IsNonzeroEverywhere

The kernel of ι ≫ coordInclFst N 1 : X ⟶ 𝔸^{N+1} is nonzero at every point of 𝔸^{N+1}: it contains the last coordinate, and 𝔸^{N+1} is integral, so no nonzero section vanishes in a stalk.

theorem Hironaka.Resolution.exists_admissibleEmbedding {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : ∃ (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left), AdmissibleEmbedding k X TA emb

Every affine scheme of finite type over k has an admissible pair ("embed X into an affine space", [Kol07, Theorem 36, proof]): X ↪ 𝔸^N ↪ 𝔸^{N+1} through the coordinate hyperplane, whose kernel is nonzero everywhere.

theorem Hironaka.Resolution.exists_admissibleEmbedding_of_codim {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : ∃ (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left), AdmissibleEmbedding k X TA emb ∧ ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))

Every affine scheme of finite type over k has an admissible pair whose ambient has Krull dimension ≥ 2 at the image of every generic point of X (the embedding X ↪ A into a smooth affine scheme with dim A ≥ dim X + 2 of the proofs of [Kol07, Theorem 36] and [Kol07, Corollary 22]): the codimension-two embedding exists_affineEmbedding into 𝔸^N, followed by the coordinate hyperplane 𝔸^N ↪ 𝔸^{N+1} (a closed immersion: the stalk map is surjective, so the dimension of the stalk does not decrease).