Local existence of a smooth hypersurface of maximal contact

Kollár's local construction of maximal contact [Kol07, Theorem 80 (2); 51.2]: for m = max-ord I, every point x has an open neighbourhood U and a section h ∈ H⁰(U, MC(I)) whose zero divisor H := (h = 0) ⊂ U is smooth, where MC(I) = D^{m−1}(I) is the (m−1)-st derivative ideal [Kol07, 51]. Kollár's proof: at a point x with ord_x I = m the ideal MC(I) has order 1 (by his Lemma 74 (3)), so some local section of MC(I) has order 1 at x, "and so its zero divisor is smooth in a neighborhood of x". On analytic manifolds the last step — the Jacobian criterion — is the analytic implicit function theorem in the form exists_adapted_chart_of_ord_eq_one' (Hironaka/Manifold/Chart/Adapted.lean). Włodarczyk's tangent directions are the same sections: functions of multiplicity one in D^{µ−1}(I) Wlo09, Lemma 5.3.4; Definition 5.3.5; Lemma 5.3.6.

• ord_iteratedDeriv_eq_one: at a point of order exactly m ≥ 1, ord_x D^{m−1}(I) = 1. The stalk of D^{m−1}(I) is the iterated derivative ideal D^{m−1}(I_x) of the stalk in the regular coordinates of a chart (stalkIdeal_iteratedDeriv_eq_Dpow), whose order is ord I_x − (m − 1) = 1 (ord_Dpow_of_ord_eq; [Kol07, Lemma 74 (3)]).
• exists_mem_carrier_iteratedDeriv_ordElem_eq_one: a local section of MC(I) of order 1 at x. The stalk MC(I)_x is spanned by the germs of finitely many local sections of MC(I) (local finite generation), and the order of a finitely generated ideal is attained by one of its generators (exists_ord_span_eq_ordElem); the generator set is nonempty since the zero ideal has order ⊤ ≠ 1.
• exists_smoothDivisor_of_ordElem_eq_one (the analytic implicit function theorem applied): a section g of an ideal sheaf J with order 1 at x restricts, to the source U of an adapted chart e with g = ψ(e(·))_{σ 0} on U, to a section h ∈ J(U) whose zero set is a closed submanifold of codimension 1 of U and whose order at every zero y ∈ U is 1: the germ of h at y is the coordinate germ coord … (σ 0) (two sections agreeing on U have the same germs), whose value at a zero is 0 and whose σ 0-th coordinate derivative is 1 ≠ 0 (coordDerivStalk_coord_eq_ite), which is the order-one criterion ord_eq_one_iff_exists_coordDerivStalk_ne_zero'.
• exists_maximalContactHypersurface_nhd, the theorem, for m ≥ max-ord I and every x. If x lies in the cosupport of MC(I) then m ≥ 1 (for m = 0, MC(I) = I and ord_x I ≤ 0 puts x off the cosupport) and ord_x I = m (cosupport_iteratedDeriv: cosupp MC(I) = {ord I ≥ m}), and the two lemmas above give the section. Otherwise MC(I) is the unit ideal sheaf on the open complement of its cosupport, where the constant section 1 lies in MC(I) and has empty zero set — Kollár's H_x = ∅, a smooth (empty) divisor; this covers the points with ord_x I < m, the zero-dimensional manifolds and the case m = 0.

This is the local input of the order-reduction algorithm on analytic manifolds (Hironaka/Resolution/Analytic/OrderReduction/LocalMaximalContact.lean).

theorem Manifold.exists_smoothDivisor_of_ordElem_eq_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) {V : TopologicalSpace.Opens M} {x : M} (hxV : x ∈ V) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (hg : g ∈ J.carrier V) (hord : IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V x hxV)) g) = 1) : ∃ (U : TopologicalSpace.Opens M) (_ : x ∈ U), ∃ h ∈ J.carrier U, IsClosedSubmanifoldOn ψ (↑U) (↑U ∩ {y : M | extendSection 𝕜 E h y = 0}) 1 ∧ ∀ (y : M) (hy : y ∈ U), extendSection 𝕜 E h y = 0 → IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U y hy)) h) = 1

The analytic implicit function theorem applied to a section of order one (Kollár's local section of MC(I) of order 1 at x, whose "zero divisor is smooth in a neighborhood of x", [Kol07, Theorem 80, proof]): a section g ∈ J(V) of order 1 at x restricts to the source U of an adapted chart to a section h ∈ J(U) whose zero set is a closed submanifold of codimension 1 of U and which has order 1 at each of its zeros.

theorem Manifold.ord_iteratedDeriv_eq_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : 1 ≤ m) {x : M} (hx : I.ord x = ↑m) : (I.iteratedDeriv (m - 1)).ord x = 1

Kollár's "pick x ∈ X such that ord_x I = m. Then ord_x MC(I) = 1 by (74.3)" ([Kol07, Theorem 80, proof]; [Kol07, Lemma 74 (3)] at the stalk, through the regular coordinates of a chart): at a point of order exactly m ≥ 1, the derivative ideal MC(I) = D^{m−1}(I) has order 1.

theorem Manifold.exists_mem_carrier_iteratedDeriv_ordElem_eq_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : 1 ≤ m) {x : M} (hx : I.ord x = ↑m) : ∃ (U : TopologicalSpace.Opens M) (hxU : x ∈ U), ∃ h ∈ (I.iteratedDeriv (m - 1)).carrier U, IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U x hxU)) h) = 1

Kollár's "there is a local section of MC(I) that has order 1 at x" (Kol07, Theorem 80, proof; [Kol07, 51.2]): at a point of order exactly m ≥ 1, an open neighbourhood U of x carries a section h ∈ H⁰(U, MC(I)) of order 1 at x — one of the finitely many local generators of the stalk MC(I)_x, whose order is attained by a generator.

theorem Manifold.exists_maximalContactHypersurface_nhd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hI : ∀ (y : ↑↧M), I.ord y ≤ ↑m) (x : M) : ∃ (U : TopologicalSpace.Opens M) (_ : x ∈ U), ∃ h ∈ (I.iteratedDeriv (m - 1)).carrier U, IsClosedSubmanifoldOn ψ (↑U) (↑U ∩ {y : M | extendSection 𝕜 E h y = 0}) 1 ∧ ∀ (y : M) (hy : y ∈ U), extendSection 𝕜 E h y = 0 → IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U y hy)) h) = 1

Local existence of a smooth hypersurface of maximal contact ([Kol07, Theorem 80 (2)] and its proof; [Kol07, 51.2]; Włodarczyk's tangent directions, Wlo09, Lemma 5.3.4; Definition 5.3.5; Lemma 5.3.6): for m ≥ max-ord I, every x ∈ M has an open neighbourhood U and a section h ∈ H⁰(U, MC(I)) whose zero divisor H := (h = 0) ⊂ U is smooth — its zero set is a closed submanifold of codimension 1 of U and h has order 1 at each of its zeros. At a point of the cosupport of MC(I) the order of I is exactly m ≥ 1 and a section of order 1 exists; off the cosupport MC(I) is the unit ideal sheaf and the constant section 1, with empty zero set, is such a section.