The dimension of a triple

Kollár's functors BO_m, BMO_m of [Kol07, Theorems 68 and 69] are assembled from the stages of the induction of [Kol07, 70], one stage per dimension bound. A triple is equidimensional by [Kol07, Notation 64 (1)] — its structure morphism is smooth of ONE relative dimension (Triple.smoothOfRelativeDimension : ∃ n, SmoothOfRelativeDimension n (X ↘ Spec k)) — so "dim X", the maximum of the local dimensions, is that relative dimension: Triple.dim T chooses it. Every triple then lies in the stage dim X (HasDimLE T T.dim), and tower base T.dim is the canonical stage for X (the coherence of Hironaka.Resolution.Algebraic.Stage.Coherence makes every higher stage agree with it). On a nonempty X the relative dimension is unique (SmoothOfRelativeDimension.eq_of_nonempty), so HasDim n ↔ dim = n and HasDimLE n ↔ dim ≤ n (HironakaExamples.Stage.BaseCases); on the empty scheme every n is a relative dimension and dim is the chosen one. No cotangent-rank computation is needed: equidimensional triples carry their dimension as data.

noncomputable def AlgebraicGeometry.Triple.dim {k : Type u} [Field k] (T : Triple k) : ℕ

The dimension of a triple (Kollár's dim X = n of [Kol07, Theorem 103], for the equidimensional X of [Kol07, Notation 64 (1)]): the relative dimension of its structure morphism, chosen from Triple.smoothOfRelativeDimension; unique when X is nonempty (SmoothOfRelativeDimension.eq_of_nonempty).

Equations

• T.dim = Classical.choose ⋯

theorem AlgebraicGeometry.Triple.hasDim_dim {k : Type u} [Field k] (T : Triple k) : T.HasDim T.dim

The chosen relative dimension is a relative dimension of the structure morphism (Classical.choose_spec on Triple.smoothOfRelativeDimension).

theorem AlgebraicGeometry.Triple.hasDimLE_dim {k : Type u} [Field k] (T : Triple k) : T.HasDimLE T.dim

Every triple lies in some stage: the stage of its own dimension.