Independence of the embedding #
Kollár's resolution BR(X) of an affine scheme X is built from a closed embedding X ↪ A into
a smooth affine scheme. The proof of [Kol07, Theorem 36] shows that the result does not depend on
the embedding: since the principalization functor commutes with closed embeddings, it suffices to
compare embeddings into affine spaces X ↪ 𝔸ⁿ; the dimension n may be increased at will along
𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ; and by [Kol07, Lemma 39] two embeddings into affine spaces become conjugate under an
automorphism of a larger affine space, along which the functor is transported. This file carries
out that argument.
The argument (BR_affine_indep) #
For two admissible embeddings emb₁ : X ↪ TA₁.X.left and emb₂ : X ↪ TA₂.X.left:
- Boundary normalisation (
BR_affine_emptiedTriple):BR_affine TAᵢ embᵢdoes not change when the boundary ofTAᵢ(a family with empty index type) is replaced by the literal empty family, since the principalization sequence does not distinguish the two (BP_emptiedTriple). - The ambient into affine space (
exists_closedImmersion_affineSpace):TAᵢ.X.leftis affine of finite type overk, so its ring of functions is a finitely generatedk-algebra andTAᵢ.X.left ↪ 𝔸^{Nᵢ}overk; the image ofTAᵢ.Iis nonzero everywhere becauseTAᵢ.Iis, so(𝔸^{Nᵢ}, TAᵢ.I.map ι, ∅)is a triple, andBR_affinemoves to it becauseBPcommutes with closed embeddings [Kol07, Theorem 35 (5)] (BR_affine_eq_affineSpaceTriple). - Stabilisation to the common
𝔸ⁿ⁺ᵐalongcoordInclFst n mandcoordInclSnd n m(BR_affine_stabilizeFst,BR_affine_stabilizeSnd), again by [Kol07, Theorem 35 (5)]. - Lemma 39 (
exists_aut_conj_embeddings): an automorphismφof𝔸ⁿ⁺ᵐoverkwithi₁ ≫ coordInclFst n m ≫ φ = i₂ ≫ coordInclSnd n m. - Transport along
φ(BR_affine_conj):BPcommutes with the smooth surjectionφ[Kol07, Theorem 35 (4)], and the ideal of the conjugated embedding is the inverse image of the ideal of the other (Scheme.Hom.ker_comp,comap_map_of_isClosedImmersion). - Back down the second side by steps 3, 2 and 1.
BR_affine'_eq then reads the embedding-free BR_affine' k X off any admissible pair.
Conventions #
The clauses of [Kol07, Theorem 35] used here are the library's BP_pushforward_of_closedEmbedding
and BP_pullback_of_surjective (Hironaka.Resolution.Algebraic.Kol07.Thm35.Principalization). The
independence theorem is the input to the affine part of Kollár's resolution functor
(Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) and to its functoriality under smooth morphisms and
change of fields.
Boundary normalisation #
The triple T with its boundary replaced by the empty family (the same ambient and ideal).
Equations
- Hironaka.Resolution.emptiedTriple T = { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := AlgebraicGeometry.Scheme.DivisorFamily.empty T.X.left, isSnc := ⋯ }
Instances For
The principalization sequence does not distinguish a boundary with empty index type from the
empty family: with an empty boundary BP is the order reduction BMO_1 (BP_of_isEmpty), which
is indifferent to empty members of the boundary (dimFreeBMO_indifferentToEmptyMembers).
BR_affine does not distinguish a boundary with empty index type from the empty family.
The ambient into affine space #
For a morphism g : X ⟶ Spec R, g = X.toSpecΓ ≫ Spec.map (ΓSpecIso.inv ≫ g.appTop)
(the unit of the Γ ⊣ Spec adjunction).
An affine scheme X of finite type over k embeds as a closed subscheme into an affine space
over k: the ring of global sections is a finitely generated k-algebra (finite type read on
global sections, HasRingHomProperty.iff_of_isAffine), and a surjection k[Fin N] → Γ(X, ⊤)
gives the closed immersion Spec.map composed with X ≅ Spec Γ(X, ⊤). Used for the ambient of
a triple here and for the affine members of the class of the resolution functor later.
The affine ambient TA.X.left of a triple embeds as a closed subscheme into an affine space
over k, the case X := TA.X.left of exists_closedImmersion_affineSpace_of_isAffine (the
triple's finite type supplies the instance). This is the passage from an arbitrary smooth affine
ambient to an affine space in the proof of [Kol07, Theorem 36].
The three moves on affine-space triples #
Steps 1 and 2 of the argument: for a triple TA with empty boundary and a closed immersion
ι : TA.X.left ↪ 𝔸^N over k, BR_affine built in TA equals BR_affine built in the
affine-space triple (𝔸^N, TA.I.map ι, ∅), by boundary normalisation and [Kol07, Theorem 35 (5)]
along ι.
Step 3 of the argument, first block: stabilisation along 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ, x ↦ (x, 0), by
[Kol07, Theorem 35 (5)] along coordInclFst n m.
Step 3 of the argument, second block: stabilisation along 𝔸ᵐ ↪ 𝔸ⁿ⁺ᵐ, y ↦ (0, y), by
[Kol07, Theorem 35 (5)] along coordInclSnd n m.
Step 5 of the argument: transport along an automorphism φ of 𝔸^N over k carrying the
ideal I₂ to I₁, by [Kol07, Theorem 35 (4)] for the smooth surjection φ
(BP_pullback_of_surjective) and BR_affine_eq_of_BP_eq_pullback.
The theorem #
Independence of the embedding [Kol07, Theorem 36, proof]: for any two admissible
embeddings emb₁ : X ↪ TA₁.X.left and emb₂ : X ↪ TA₂.X.left of a scheme X over k,
BR_affine TA₁ emb₁ = BR_affine TA₂ emb₂. The proof is Kollár's: both sides are moved to
affine-space triples (BR_affine_eq_affineSpaceTriple), stabilised to the common 𝔸ⁿ⁺ᵐ
(BR_affine_stabilizeFst, BR_affine_stabilizeSnd), and the two coordinate embeddings are
conjugated by the automorphism of [Kol07, Lemma 39] (exists_aut_conj_embeddings), along which
BR_affine is transported (BR_affine_conj); the ideal of the conjugated embedding is the
inverse image of the other ideal (Scheme.Hom.ker_comp, comap_map_of_isClosedImmersion).
The embedding-free BR_affine' k X equals BR_affine TA emb for every admissible pair
(TA, emb): the pair chosen by BR_affine' is admissible and BR_affine_indep compares.