Maximal coefficient ideal sheaves, D-balanced and MC-invariant ideal sheaves

The analytic forms of three notions of Kollár's proof, for a locally finitely generated ideal sheaf J on an analytic manifold, with the derivative ideal sheaves D^j J of Hironaka/Manifold/IdealSheaf/Deriv.lean:

• IdealSheaf.tuning J m s is Kollár's maximal coefficient ideal W_s(I) = ∑_{wt(e) ≥ s} ∏_j (D^j I)^{e_j} [Kol07, Definition 98], the ideal sheaf with that stalk at every point (ofStalks). It is locally finitely generated because the sum is finite: ∑_{e ∈ tuningExponents m s} suffices (IsLocalRing.iSup_wt_eq_sum_tuningExponents), and a finite sum of finite products of powers of locally finitely generated ideal sheaves is locally finitely generated (the monoid structures of Hironaka/Manifold/IdealSheaf/Monoid.lean). Kollár's m = max-ord I is an explicit parameter.
• IdealSheaf.IsDBalanced J m: (D^i J)^m ⊆ J^{m−i} for i < m [Kol07, Definition 83] (the analytic form of the Hironaka library's IsDBalanced).
• IdealSheaf.IsMCInvariant J m: MC(J) · D(J) ⊆ J with MC(J) = D^{m−1} J [Kol07, Definition 79; 53, (53.1)] (the analytic form of the Hironaka library's IsMCInvariant).

The properties of W_s(J) — Kollár's Proposition 99, its orders and cosupports — are read off the Hironaka library's coefficient ideals RegularCoords.W at the stalks in Hironaka/Manifold/IdealSheaf/TuningLemmas.lean; the tuned ideal sheaves are the input of the order-reduction algorithm (Hironaka/Resolution/Analytic/OrderReduction/).

The maximal coefficient ideal sheaf (Kollár Definition 98)

theorem Manifold.IdealSheaf.hasLocalGenerators_tuning {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) (m s : ℕ) : HasLocalGenerators fun (x : ↑↧M) => ⨆ (e : Fin (m + 1) → ℕ), ⨆ (_ : s ≤ IsLocalRing.wt m e), ∏ j : Fin (m + 1), (J.iteratedDeriv ↑j).stalkIdeal x ^ e j

Kollár's W_s as a finite sum of finite products [Kol07, Definition 98]: the stalks W_s(J)_x = ∑_{wt(e) ≥ s} ∏_j ((D^j J)_x)^{e_j} have local generators, the sum being the finite one over tuningExponents m s.

noncomputable def Manifold.IdealSheaf.tuning {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) (m s : ℕ) : IdealSheaf (structureSheaf 𝕜 E M)

The maximal coefficient ideal sheaf W_s(J) = ∑_{wt(e) ≥ s} ∏_j (D^j J)^{e_j} of order s [Kol07, Definition 98], with the parameter m (Kollár's max-ord I) explicit — the ideal sheaf with Kollár's sum as its stalk at every point.

Equations

• One or more equations did not get rendered due to their size.

def Manifold.IdealSheaf.IsDBalanced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) (m : ℕ) : Prop

J is D-balanced with respect to m if (D^i J)^m ⊆ J^{m−i} for every i < m [Kol07, Definition 83], with D the derivative ideal sheaf (the analytic form of the Hironaka library's IsDBalanced).

Equations

• J.IsDBalanced m = ∀ i < m, J.iteratedDeriv i ^ m ≤ J ^ (m - i)

theorem Manifold.IdealSheaf.isDBalanced_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] (J : IdealSheaf (structureSheaf 𝕜 E M)) : J.IsDBalanced 1

Every ideal sheaf is D-balanced with respect to 1: the only clause is J ≤ J.

def Manifold.IdealSheaf.IsMCInvariant {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) (m : ℕ) : Prop

J is MC-invariant with respect to m if MC(J) · D(J) ⊆ J, MC(J) = D^{m−1} J [Kol07, Definition 79; 53, (53.1)] (the analytic form of the Hironaka library's IsMCInvariant, the maximal contact ideal written as iteratedDeriv (m - 1)).

Equations

• J.IsMCInvariant m = (J.iteratedDeriv (m - 1) * J.deriv ≤ J)