The order along a closed subset and the maximal order

[Kol07, Definition 47]: for an irreducible subvariety Z ⊂ X the order of I along Z is ord_Z I := ord_η I, η the generic point of Z; for Z not irreducible, the notation ord_Z I = m (resp. ord_Z I ≥ m) means that the order of I at every generic point of Z is m (resp. ≥ m); and the maximal order of I along Z is max-ord_Z I := max {ord_z I : z ∈ Z}.

• IrreducibleCloseds.genericPoint Z is the generic point of an irreducible closed subset of a quasi-sober space (Mathlib's IsIrreducible.genericPoint); schemes are quasi-sober and T₀, so it is the unique point with closure {η} = Z.
• Closeds.genericPoints Z are the generic points of a closed subset Z, the generic points of its irreducible components, taken as the points of Z maximal for specialization; the characterization mem_genericPoints_iff identifies them with the points η whose closure closure {η} is a maximal irreducible subset of Z (an irreducible component of Z).
• ordAlong I Z := ord I (generic point of Z) for Z irreducible closed; OrdAlongEq I Z m and LeOrdAlong I Z m are Kollár's conventions ord_Z I = m, ord_Z I ≥ m for a closed Z that need not be irreducible (the condition at every generic point), consistent with ordAlong on irreducible closed sets (ordAlongEq_iff, leOrdAlong_iff); maxOrdAlong I Z := ⨆ z ∈ Z, ord I z is max-ord_Z I (attained and finite under Noetherian hypotheses, Hironaka/Scheme/IdealSheaf/Order/Constructible.lean). [Hau03, Appendix A] defines ord_Z through the localization 𝒪_{W,Z} and notes ord_Z = min_{a ∈ Z} ord_a I; that minimum is Hironaka/Scheme/IdealSheaf/Order/Specialization.lean.

The two lemmas at the end, on membership in a finite union of closed sets and on affine neighbourhoods missing it, are general tools used by the monomial part of the argument (Hironaka/Resolution/Algebraic/Monomial/Geometric).

Used for the cosupport of marked ideals and the centres of blow-ups (Hironaka/Scheme/Snc/Dictionary.lean, HironakaExamples/Sequence/CosuppForcing.lean, Hironaka/Resolution/Algebraic/Balanced/GoingUpChain.lean, Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean, Hironaka.BD.Zminus1).

def TopologicalSpace.Closeds.genericPoints {X : Type u_1} [TopologicalSpace X] (Z : Closeds X) : Set X

The generic points of a closed subset Z ("every generic point of Z", [Kol07, Definition 47]): the points of Z that are maximal for specialization, that is, the generic points of the irreducible components of Z (Closeds.mem_genericPoints_iff).

Equations

• Z.genericPoints = {η : X | η ∈ Z ∧ ∀ ⦃η' : X⦄, η' ∈ Z → η' ⤳ η → η' = η}

theorem TopologicalSpace.Closeds.genericPoints_bot {X : Type u_1} [TopologicalSpace X] : ⊥.genericPoints = ∅

The empty closed set has no generic points.

noncomputable def TopologicalSpace.IrreducibleCloseds.genericPoint {X : Type u_1} [TopologicalSpace X] [QuasiSober X] (Z : IrreducibleCloseds X) : X

The generic point of an irreducible closed subset of a quasi-sober space (Mathlib's IsIrreducible.genericPoint).

Equations

• Z.genericPoint = ⋯.genericPoint

theorem TopologicalSpace.IrreducibleCloseds.isGenericPoint_genericPoint {X : Type u_1} [TopologicalSpace X] [QuasiSober X] (Z : IrreducibleCloseds X) : IsGenericPoint Z.genericPoint ↑Z

The generic point of Z is a generic point of Z: closure {η} = Z.

theorem TopologicalSpace.Closeds.mem_genericPoints_iff {X : Type u_1} [TopologicalSpace X] [T0Space X] [QuasiSober X] (Z : Closeds X) (η : X) : η ∈ Z.genericPoints ↔ Maximal (fun (T : Set X) => T ⊆ ↑Z ∧ IsIrreducible T) (closure {η})

The generic points of a closed Z in a sober T₀ space are the points η ∈ Z whose closure is a maximal irreducible subset of Z — an irreducible component of Z. (A specialization-maximal η has closure {η} maximal: an irreducible T ⊆ Z containing η has a generic point η' of its closure, which specializes to η, so η' = η and T ⊆ closure {η}; conversely maximality of closure {η} forces any η' ∈ Z with η' ⤳ η to satisfy η ⤳ η' as well, hence η' = η.)

theorem TopologicalSpace.IrreducibleCloseds.genericPoints_eq {X : Type u_1} [TopologicalSpace X] [T0Space X] [QuasiSober X] (Z : IrreducibleCloseds X) : { carrier := ↑Z, isClosed' := ⋯ }.genericPoints = {Z.genericPoint}

The only generic point of an irreducible closed Z is its generic point.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.ordAlong {X : Scheme} (I : X.IdealSheafData) (Z : TopologicalSpace.IrreducibleCloseds ↥X) : ℕ∞

[Kol07, Definition 47]: the order of I along an irreducible closed subset Z, ord_Z I := ord_η I for η the generic point of Z.

Equations

• I.ordAlong Z = I.ord Z.genericPoint

def AlgebraicGeometry.Scheme.IdealSheafData.OrdAlongEq {X : Scheme} (I : X.IdealSheafData) (Z : TopologicalSpace.Closeds ↥X) (m : ℕ∞) : Prop

Kollár's notation ord_Z I = m for a closed Z that need not be irreducible ([Kol07, Definition 47]): the order of I at every generic point of Z is m.

Equations

• I.OrdAlongEq Z m = ∀ η ∈ Z.genericPoints, I.ord η = m

def AlgebraicGeometry.Scheme.IdealSheafData.LeOrdAlong {X : Scheme} (I : X.IdealSheafData) (Z : TopologicalSpace.Closeds ↥X) (m : ℕ∞) : Prop

Kollár's notation ord_Z I ≥ m for a closed Z that need not be irreducible ([Kol07, Definition 47]): the order of I at every generic point of Z is at least m.

Equations

• I.LeOrdAlong Z m = ∀ η ∈ Z.genericPoints, m ≤ I.ord η

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.maxOrdAlong {X : Scheme} (I : X.IdealSheafData) (Z : Set ↥X) : ℕ∞

[Kol07, Definition 47]: the maximal order of I along Z, max-ord_Z I := max {ord_z I : z ∈ Z}, as a supremum in ℕ∞ (attained and finite under the hypotheses of Hironaka/Scheme/IdealSheaf/Order/Constructible.lean).

Equations

• I.maxOrdAlong Z = ⨆ z ∈ Z, I.ord z

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlong_eq_of_isGenericPoint {X : Scheme} (I : X.IdealSheafData) {Z : TopologicalSpace.IrreducibleCloseds ↥X} {η : ↥X} (hη : IsGenericPoint η ↑Z) : I.ordAlong Z = I.ord η

ord_Z I = ord_η I for any generic point η of the irreducible closed Z (there is exactly one, schemes being T₀).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ordAlongEq_iff {X : Scheme} (I : X.IdealSheafData) (Z : TopologicalSpace.IrreducibleCloseds ↥X) (m : ℕ∞) : I.OrdAlongEq { carrier := ↑Z, isClosed' := ⋯ } m ↔ I.ordAlong Z = m

For an irreducible closed Z the convention ord_Z I = m is ordAlong I Z = m.

theorem AlgebraicGeometry.Scheme.IdealSheafData.leOrdAlong_iff {X : Scheme} (I : X.IdealSheafData) (Z : TopologicalSpace.IrreducibleCloseds ↥X) (m : ℕ∞) : I.LeOrdAlong { carrier := ↑Z, isClosed' := ⋯ } m ↔ m ≤ I.ordAlong Z

For an irreducible closed Z the convention ord_Z I ≥ m is m ≤ ordAlong I Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_maxOrdAlong {X : Scheme} (I : X.IdealSheafData) {Z : Set ↥X} {z : ↥X} (hz : z ∈ Z) : I.ord z ≤ I.maxOrdAlong Z

ord_z I ≤ max-ord_Z I for z ∈ Z.

theorem AlgebraicGeometry.Scheme.IdealSheafData.maxOrdAlong_le_iff {X : Scheme} (I : X.IdealSheafData) {Z : Set ↥X} {m : ℕ∞} : I.maxOrdAlong Z ≤ m ↔ ∀ z ∈ Z, I.ord z ≤ m

max-ord_Z I ≤ m iff ord_z I ≤ m for every z ∈ Z.

theorem Hironaka.Monomial.PieceFamily.mem_finset_sup_iff {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (s : Finset ι) (g : ι → TopologicalSpace.Closeds ↥X) (x : ↥X) : x ∈ s.sup g ↔ ∃ i ∈ s, x ∈ g i

Membership in a finite supremum of closed sets (a general tool, in the namespace of the monomial part that uses it, Hironaka/Resolution/Algebraic/Monomial/Geometric).

theorem AlgebraicGeometry.exists_affineOpens_of_not_mem_sup {X : Scheme} {ι : Type u_1} (s : Finset ι) (C : ι → TopologicalSpace.Closeds ↥X) {x : ↥X} (hx : x ∉ s.sup C) : ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∀ y ∈ ↑U, y ∉ s.sup C

A point outside a finite union of closed sets has an affine neighbourhood outside it (used by Hironaka/Resolution/Algebraic/Monomial/Geometric/Local.lean).