The class of the source of a closed embedding #
Kollár's Claim 71.2 [Kol07, Claim 71.2] compares BMO_1(X, I, 1, ∅) with τ_* BMO_1(Y, J, 1, ∅)
for a closed embedding τ : Y ↪ X of smooth schemes. In the library the functors are the stage
functors of the tower (Hironaka.Resolution.Algebraic.Stage.Tower), defined on the class
MarkedTriple.BMOClass n 1 — mark 1 and dimension ≤ n. The triple of X is in the class by
hypothesis; the triple of Y is in it because a closed subscheme smooth over k of a scheme of
dimension ≤ n has dimension ≤ n and carries the same mark (MarkedTriple.ClosedEmbedding). This
module proves that membership, bmoClass_of_closedEmbedding, so that the identity of Claim 71.2
(Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingGeneral) can be stated without taking Y's
class as a hypothesis Kollár does not have.
The dimension inequality dim Y ≤ dim X is read off the Krull dimension of the stalks at a closed
point (Scheme.ringKrullDim_stalk_of_smoothOfRelativeDimension_of_isClosed, over a perfect field —
PerfectField.ofCharZero): the stalk of Y at a closed point p is a quotient of the stalk of X
at τ p (the stalk map of a closed immersion is surjective), so its Krull dimension is at most that
of X's stalk (Mathlib's ringKrullDim_le_of_surjective); τ p is a closed point (a closed
immersion is a closed embedding), and a closed point of Y exists when Y is nonempty (Y is of
finite type over k, hence Jacobson — exists_isClosed_singleton_mem_specializes); an empty Y
has every relative dimension (smoothOfRelativeDimension_of_isEmpty).
A closed embedding of smooth k-schemes does not raise the dimension bound: for j : Y ↪ X
a closed immersion with X of dimension ≤ n, Y has dimension ≤ n — at a closed point p of
Y the stalk of Y is a quotient of the stalk of X at the closed point j p, so
dim Y = dim 𝒪_{Y,p} ≤ dim 𝒪_{X,j p} = dim X (the Krull dimension of the stalks at closed points of
a scheme smooth of relative dimension d over a perfect field). Only the closed immersion and the
two triples' smoothness enter; the k-compatibility of j is not needed.
The source of a closed embedding of marked triples with E = ∅ and mark 1 is in the stage
class: TY.BMOClass n 1 from TX.BMOClass n 1 — the mark is transported by
MarkedTriple.ClosedEmbedding, the dimension bound by hasDimLE_of_closedEmbedding. This is the
class proof on the side of Y in the statements of Claim 71.2.