Local existence of hypersurfaces of maximal contact

[Kol07, Theorem 80 (2)]: for m = max-ord I, every point of X has a neighbourhood on which a smooth hypersurface of maximal contact exists. Kollár's proof is three sentences: at a point x with ord_x I = m, ord_x MC(I) = 1 by [Kol07, Lemma 74 (3)]; so some local section of MC(I) has order 1 at x; and its zero divisor is smooth near x. This file carries them out on ideal sheaves, and adds the two things the printed proof does not spell out: the points where ord_x I < m (there MC(I) is the unit ideal sheaf near x, and the empty hypersurface ⊤ works) and the transport of the equation from the affine open where it is found to the open where its zero divisor is smooth. [Kol07, Aside 81] notes that such an H exists locally but usually not globally; only the local statement is proved here.

• The ideal sheaf of a section. principal h (Hironaka/Resolution/Algebraic/MaximalContact/Principal.lean) is described by principal_ideal, stalkIdeal_principal, principal_le_iff, principal_one and ord_principal; comap_principal says that it restricts as the section does, (principal h).comap g = principal (g^* h) (stalkwise: the germ of g^* h at y is the image of the germ of h at g y, Mathlib's germ_stalkMap_apply).
• From the stalk to a section. ord_x MC(I) = 1 gives an element a ∈ MC(I)_x with a ∈ 𝔪_x ∖ 𝔪_x² (ordElem_eq_one_iff); the stalk is the localization of MC(I)(U) at x for an affine U ∋ x (Mathlib's IsAffineOpen.isLocalization_stalk), so a · germ u = germ s with s ∈ MC(I)(U) and u invertible at x; multiplying by a unit does not change the order (ordElem_mul_of_isUnit), so ordElem (germ s) = 1.
• The smooth locus of an equation. For a global section h of order 1 at x, the set {y | ord_y (h) < 2} is open (upper semicontinuity of the order, which is where smoothness in characteristic zero enters) and contains x; on it, at every point of V(h), the germ of h lies in 𝔪 ∖ 𝔪² (order exactly 1), which is the generator clause of IsSmoothDivisor, and 𝒪_y/(h) is regular (IsRegularLocalRing.quotient_span_singleton), which gives the regularity of V(h). The order of the restricted sheaf is read off with ord_comap_ι.
• The unit case. Where ord_x I < m, the open {ord I < m} has ord MC(I) = 0 at every point, so MC(I|_U) = (MC I)|_U = 𝒪_U.
• Assembly. Under max-ord I = m, ord_x I ≤ m; if m = 0 then I = 𝒪_X and U = X, h = 1; if ord_x I < m, the unit case and h = 1; if ord_x I = m ≥ 1, the section of order one lives on an affine U₁ and is viewed as a global section h₂ of the open subscheme U₁ (Mathlib's Opens.topIso), whose germ at x has order 1 (the stalks of U₁ are those of X, Opens.stalkIso) and whose ideal sheaf lies in MC(I|_{U₁}); the smooth locus of h₂ is an open V ∋ x of U₁; the final open is the range of V ⟶ U₁ ⟶ X, identified with V by Mathlib's isoOpensRange, along which principal, IsSmoothDivisor and IsMaximalContact are transported by comap.
• The dynamic form. IsOrderSeq.strictTransformSeq_le_center_of_le_MC turns the static hypersurface into a dynamic one on every open immersion, exactly as in isDynamicMaximalContact_of_isMaximalContact, without Kollár's I|_H ≠ 0 (which a local H need not satisfy).

The local hypersurfaces are the input of the globalization of blow-up sequences ([Kol07, Theorem 105], Hironaka/Resolution/Algebraic/Kol07/MaximalContactGlobalization.lean), which patches the order reduction on the opens U into one on X.

theorem Hironaka.Local.ordElem_mul_of_isUnit {R : Type u_1} [CommRing R] [IsLocalRing R] {a v : R} (hv : IsUnit v) : IsLocalRing.ordElem (a * v) = IsLocalRing.ordElem a

Multiplying by a unit does not change the order of an element.

The ideal sheaf of a section: the five unfoldings and restriction

theorem AlgebraicGeometry.Scheme.IdealSheafData.principal_ideal {X : Scheme} (h : ↑(X.presheaf.obj (Opposite.op ⊤))) (U : ↑X.affineOpens) : (principal h).ideal U = Ideal.span {(CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) h}

On every affine open U the ideal sheaf generated by h is the principal ideal (h|_U) (Mathlib's ofIdealTop_ideal: the image of the ideal (h) of the global sections).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_principal {X : Scheme} (h : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↥X) : (principal h).stalkIdeal x = Ideal.span {(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) h}

The stalk of (h) at x is generated by the germ of h.

theorem AlgebraicGeometry.Scheme.IdealSheafData.principal_le_iff {X : Scheme} (h : ↑(X.presheaf.obj (Opposite.op ⊤))) (J : X.IdealSheafData) : principal h ≤ J ↔ ∀ (U : ↑X.affineOpens), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) h ∈ J.ideal U

h is a section of J iff (h) ≤ J.

theorem AlgebraicGeometry.Scheme.IdealSheafData.principal_one {X : Scheme} : principal 1 = ⊤

The unit section generates the unit ideal sheaf.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_principal {X : Scheme} (h : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↥X) : (principal h).ord x = IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) h)

The order of (h) at x is the order of the germ of h.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_principal {X Y : Scheme} (g : Y ⟶ X) (h : ↑(X.presheaf.obj (Opposite.op ⊤))) : (principal h).comap g = principal ((CategoryTheory.ConcreteCategory.hom (Hom.appTop g)) h)

The ideal sheaf of a section restricts as the section does: along g : Y ⟶ X, (h) pulls back to (g^* h). Stalkwise, the germ of g^* h at y is the image of the germ of h at g y (germ_stalkMap_apply).

The section of order one, and the unit case, on a smooth scheme

theorem AlgebraicGeometry.Scheme.IdealSheafData.MC_comap_eq_top_of_forall_ord_eq_zero {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m : ℕ) (U : X.Opens) (hU : ∀ (u : ↥U), (MC f I m).ord (U.ι u) = 0) : MC (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m = ⊤

If MC(I) has order 0 at every point of an open U, then MC of the restriction I|_U is the unit ideal sheaf: MC commutes with the (smooth) open immersion, and an ideal sheaf whose stalks are all the unit ideal is ⊤.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_MC_comap_eq_top_of_ord_lt {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} {x : ↥X} (hx : I.ord x < ↑m) : ∃ (U : X.Opens), x ∈ U ∧ MC (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m = ⊤

The points the proof of [Kol07, Theorem 80 (2)] passes over: at a point where ord_x I < m, the open {ord I < m} carries MC(I|_U) = 𝒪_U, since MC(I) has order 0 there.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_mem_ideal_MC_ordElem_eq_one {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) {x : ↥X} (hx : I.ord x = ↑m) : ∃ (U : ↑X.affineOpens) (hxU : x ∈ ↑U), ∃ h ∈ (MC f I m).ideal U, IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) x hxU)) h) = 1

The first two sentences of the proof of [Kol07, Theorem 80 (2)]: at a point of order m ≥ 1 of I, ord_x MC(I) = 1, so MC(I)_x contains an element a of 𝔪_x ∖ 𝔪_x²; the stalk is the localization of MC(I)(U) at x for an affine U ∋ x, so a · germ u = germ s with s ∈ MC(I)(U) and u invertible at x, and germ s has order 1 as well.

The smooth locus of an equation of order one

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_isSmoothDivisor_comap_principal {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (h : ↑(X.presheaf.obj (Opposite.op ⊤))) {x : ↥X} (hord : IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) h) = 1) : ∃ (U : X.Opens), x ∈ U ∧ IsSmoothDivisor ((principal h).comap U.ι)

The last sentence of the proof of [Kol07, Theorem 80 (2)], "its zero divisor is smooth in a neighborhood of x": for a global section h whose germ at x has order exactly 1, the open set U := {y | ord_y (h) < 2} contains x, and on it the ideal sheaf (h) is a smooth divisor: at every point of V(h) ∩ U the germ of h lies in 𝔪 ∖ 𝔪² (order exactly 1, ordElem_eq_one_iff), and the quotient of the regular stalk by it is regular (IsRegularLocalRing.quotient_span_singleton), so V(h) ∩ U is regular.

Theorem 80 (2): the assembly and its corollaries

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_principal_isSmoothDivisor_isMaximalContact {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hI : I.maxOrd = ↑m) (x : ↥X) : ∃ (U : X.Opens), x ∈ U ∧ ∃ (h : ↑((↑U).presheaf.obj (Opposite.op ⊤))), IsSmoothDivisor (principal h) ∧ IsMaximalContact (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m (principal h)

[Kol07, Theorem 80 (2)]: for m = max-ord I, every point has an open neighbourhood U with a section h ∈ 𝒪(U) whose zero divisor (h) is a smooth hypersurface of U with (h) ⊆ MC(I|_U). Where ord_x I < m (or m = 0, when I = 𝒪_X), h = 1 on the open where MC(I|_U) = 𝒪_U; where ord_x I = m ≥ 1, exists_mem_ideal_MC_ordElem_eq_one gives the equation on an affine open U₁, viewed as a global section of the open subscheme U₁, exists_opens_isSmoothDivisor_comap_principal gives the open V ⊆ U₁ where its zero divisor is smooth, and the data are transported to the open V ⟶ U₁ ⟶ X of X along Mathlib's isoOpensRange.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_isSmoothDivisor_isMaximalContact {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hI : I.maxOrd = ↑m) (x : ↥X) : ∃ (U : X.Opens), x ∈ U ∧ ∃ (H : (↑U).IdealSheafData), IsSmoothDivisor H ∧ IsMaximalContact (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m H

[Kol07, Theorem 80 (2)] with the hypersurface as an ideal sheaf: for m = max-ord I, every point has an open neighbourhood carrying a smooth divisor that is a static hypersurface of maximal contact for the restricted ideal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_opens_isSmoothDivisor_isDynamicMaximalContact {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hI : I.maxOrd = ↑m) (hm : 1 ≤ m) (x : ↥X) : ∃ (U : X.Opens), x ∈ U ∧ ∃ (H : (↑U).IdealSheafData), IsSmoothDivisor H ∧ IsMaximalContact (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m H ∧ IsDynamicMaximalContact (CategoryTheory.CategoryStruct.comp U.ι f) (I.comap U.ι) m H

[Kol07, Theorem 80 (1) and (2)] together: for m = max-ord I ≥ 1, every point has an open neighbourhood carrying a smooth divisor that is a hypersurface of maximal contact in the static and the dynamic sense; the dynamic form is IsOrderSeq.strictTransformSeq_le_center_of_le_MC on every open immersion, exactly as in isDynamicMaximalContact_of_isMaximalContact, and needs no I|_H ≠ 0.