The dictionary, part I: orders, the component family, and clause (ii) of Main Theorem II

The first part of the translation between Hironaka's Main Theorem II [Hir64, Main Theorem II] and Kollár's smooth blow-up sequences of order d [Kol07, Definition 66] (definitions in Hironaka/Scheme/Snc/Dictionary.lean):

• orders: Hironaka's "d the maximum of ν(J_x)" (IsGreatest (Set.range J.ord) d) is Kollár's "max-ord J = d, attained" [Kol07, Definition 47] (maxOrd_le_iff, le_maxOrd);
• the component family: its members are the reduced irreducible components (rfl), they cover V(E) (every point of a closed set specializes from a generic point, Closeds.exists_mem_genericPoints_specializes), the reduced union of the family is the radical of E (Mathlib's vanishingIdeal_support), and a reduced closed subscheme's ideal sheaf is radical (its sections are kernels of surjections onto the reduced rings of sections of the subscheme, Ideal.isRadical_iff_quotient_reduced);
• clause (ii): along a smooth blow-up sequence of order d for (X, J, F) with max-ord J = d, every weak transform has max-ord ≤ d ([Kol07, Remark 67]: IsOrderGeSeq.maxOrd_le through isOrderGeSeq_iff_isOrderSeq, the marked and the unmarked transforms coinciding), = d at a stage with a nonempty center, and at every point of a center the order is ≥ d by upper semicontinuity from the generic points (ord_le_ord_of_specializes on the stage, smooth of relative dimension n over k by IsSmooth.stageMap_smoothOfRelativeDimension), hence = d.

theorem AlgebraicGeometry.isGreatest_range_ord_iff {X : Scheme} (J : X.IdealSheafData) (d : ℕ∞) : IsGreatest (Set.range J.ord) d ↔ J.maxOrd = d ∧ ∃ (x : ↥X), J.ord x = d

Hironaka's "d is the maximum of the orders ν(J_x)" [Hir64, Main Theorem II] is Kollár's "max-ord J = d and the maximum is attained" [Kol07, Definition 47].

theorem AlgebraicGeometry.componentFamily_component {X : Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.IdealSheafData) (η : ↑E.support.genericPoints) : E.componentFamily.component η = Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {↑η})

The member of E.componentFamily at the generic point η is the irreducible component closure {η} with its reduced structure.

theorem AlgebraicGeometry.support_unionIdeal {X : Scheme} (F : X.DivisorFamily) : F.unionIdeal.support = F.support

The support of the reduced union of a family is the union of the supports of its members (coe_support_vanishingIdeal).

theorem AlgebraicGeometry.support_componentFamily {X : Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.IdealSheafData) : E.componentFamily.support = E.support

The irreducible components of V(E) cover V(E): each closure {η} lies in the closed V(E), and every point of V(E) is a specialization of one of its generic points (Closeds.exists_mem_genericPoints_specializes).

theorem AlgebraicGeometry.unionIdeal_componentFamily {X : Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.IdealSheafData) : E.componentFamily.unionIdeal = E.radical

The reduced union of the irreducible components of V(E) is the radical of E (support_componentFamily and Mathlib's vanishingIdeal_support).

theorem AlgebraicGeometry.radical_eq_self_of_isReduced_subscheme {X : Scheme} (E : X.IdealSheafData) [IsReduced E.subscheme] : E.radical = E

The ideal sheaf of a reduced closed subscheme (Hironaka's "E a reduced subscheme") is radical: on each affine open its ideal is the kernel of the surjection onto the sections of the subscheme (Mathlib's ker_subschemeι_app, subschemeι_app_surjective), a reduced ring, so the ideal is radical (Ideal.isRadical_iff_quotient_reduced).

theorem AlgebraicGeometry.unionIdeal_componentFamily_of_isReduced {X : Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.IdealSheafData) [IsReduced E.subscheme] : E.componentFamily.unionIdeal = E

For a reduced E the reduced union of its irreducible components is E.

theorem AlgebraicGeometry.IsSmooth.stageMap_smoothOfRelativeDimension {k : Type u} [Field k] {X : Scheme} [PerfectField k] {S : X.BlowUpSequence} {f : X ⟶ Spec ↧k} {n : ℕ} [SmoothOfRelativeDimension n f] (h : S.IsSmooth f) (i : Fin (S.length + 1)) : SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp (S.stageMap i) f)

Every stage of a smooth blow-up sequence (IsSmooth: smooth centers of any shape) over an equidimensional smooth X is smooth of the same relative dimension [Kol07, Notation 19]: smoothOfRelativeDimension_blowUpπ_comp_of_smooth at each step. This is IsSmoothOfRelativeDimension.smoothOfRelativeDimension_stageMap under the weaker hypothesis.

theorem AlgebraicGeometry.IsOrderSeq.maxOrd_weakTransformSeq_le {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {J : X.IdealSheafData} {F : X.DivisorFamily} {d : ℕ} (h : S.IsOrderSeq f J F d) (hmax : J.maxOrd = ↑d) (i : Fin (S.length + 1)) : (S.weakTransformSeq J i).maxOrd ≤ ↑d

Along a smooth blow-up sequence of order d starting with max-ord J = d, every weak transform J_i has max-ord J_i ≤ d ([Kol07, Lemma 61] iterated, as in [Kol07, Remark 67]; the remark following [Hir64, Main Theorem II]): IsOrderGeSeq.maxOrd_le for the marked transforms, which are the weak transforms (IsOrderSeq.markedTransformSeq_eq_weakTransformSeq).

theorem AlgebraicGeometry.IsOrderSeq.maxOrd_weakTransformSeq_eq {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {J : X.IdealSheafData} {F : X.DivisorFamily} {d : ℕ} (h : S.IsOrderSeq f J F d) (hmax : J.maxOrd = ↑d) (i : Fin S.length) (hne : (↑(S.center i).support).Nonempty) : (S.weakTransformSeq J i.castSucc).maxOrd = ↑d

"d is the maximum of ν(J_{i,z}) for all the points z of X_i" (the remark following [Hir64, Main Theorem II]): at a stage with a nonempty center the maximal order of J_i is exactly d; it is d at a generic point of the center ([Kol07, Definition 66 (4)]) and at most d everywhere.

theorem AlgebraicGeometry.IsOrderSeq.le_ord_of_mem_center {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {J : X.IdealSheafData} {F : X.DivisorFamily} {d : ℕ} (h : S.IsOrderSeq f J F d) (i : Fin S.length) {x : ↥(S.stage i.castSucc)} (hx : x ∈ (S.center i).support) : ↑d ≤ (S.weakTransformSeq J i.castSucc).ord x

Along a smooth blow-up sequence of order d, ν(J_{i,x}) ≥ d at every point x of the center: the order is d at a generic point of the center specializing to x ([Kol07, Definition 66 (4)]), and it can only increase under specialization on the stage, smooth of relative dimension n over k. The inequality of clause (ii) of [Hir64, Main Theorem II].

theorem AlgebraicGeometry.IsOrderSeq.ord_eq_of_mem_center {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {J : X.IdealSheafData} {F : X.DivisorFamily} {d : ℕ} (h : S.IsOrderSeq f J F d) (hmax : J.maxOrd = ↑d) (i : Fin S.length) {x : ↥(S.stage i.castSucc)} (hx : x ∈ (S.center i).support) : (S.weakTransformSeq J i.castSucc).ord x = ↑d

Along a smooth blow-up sequence of order d starting with max-ord J = d, ν(J_{i,x}) = d at every point of the center: clause (ii) of [Hir64, Main Theorem II] and clause (2) of [Hir64, Main Theorem II(N)].