The resolution of an affine scheme without a chosen embedding

Once the resolution BR(X) of an affine scheme is known to be independent of the embedding X ↪ A used to construct it [Kol07, Theorem 36, proof], it can be defined without a choice. This file fixes the hypotheses under which Kollár's construction runs and makes that definition.

Main definitions

• AdmissibleEmbedding k X TA emb: emb : X ⟶ TA.X.left is a closed immersion over k into the ambient of a triple TA = (A, I_X, ∅) with A affine (Kollár's "smooth affine scheme": smoothness is part of being a triple), empty boundary, and I_X = ker emb. Every use of the independence theorem Hironaka.Resolution.BR_affine_indep goes through this one predicate.
• BR_affine' k X : BlowUpSequence X: Kollár's BR(X) for a scheme X over k without a chosen embedding, namely BR_affine TA emb for a chosen admissible pair (TA, emb) when one exists (Classical.choice; Hironaka.Resolution.BR_affine'_eq shows that the value does not depend on the choice), and the empty sequence nil X otherwise.

The second branch is never reached for an affine scheme of finite type over k, which always has an admissible embedding (Hironaka.Resolution.exists_admissibleEmbedding); the definition is nevertheless total, so that no existence statement is built into it. The unfolding lemmas BR_affine'_of_pos and BR_affine'_of_neg are the two branches of the if.

def Hironaka.Resolution.AdmissibleEmbedding (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) : Prop

An admissible embedding of the scheme X over k into the ambient of the triple TA: a closed immersion emb : X ⟶ TA.X.left over k, with TA.X.left affine, the boundary of TA empty and the ideal of TA the kernel of emb. These are the hypotheses of Kollár's construction of the resolution of an affine scheme: an embedding X ↪ A into a smooth affine scheme and the blow-up sequence BP(A, I_X, ∅) (the proof of [Kol07, Theorem 36]).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.Resolution.BR_affine' (k : Type u) [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] : X.BlowUpSequence

Kollár's resolution BR(X) of a scheme X over k without a chosen embedding: BR_affine TA emb for a chosen admissible pair (TA, emb) if one exists, the empty sequence otherwise. BR_affine'_eq shows that the value does not depend on the choice [Kol07, Theorem 36, proof].

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Resolution.BR_affine'_of_pos (k : Type u) [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] (h : ∃ (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left), AdmissibleEmbedding k X TA emb) : BR_affine' k X = BR_affine h.choose ⋯.choose

theorem Hironaka.Resolution.BR_affine'_of_neg (k : Type u) [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] (h : ¬∃ (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left), AdmissibleEmbedding k X TA emb) : BR_affine' k X = AlgebraicGeometry.Scheme.BlowUpSequence.nil X