The order of an ideal sheaf along a closed submanifold

For the ideal sheaf I_Y of a closed submanifold Y and a locally finitely generated ideal sheaf I, the order ν_{Y,a}(I) = sup {p : I_a ⊆ I_{Y,a}^p} along Y at a (IdealSheaf.ordAlongIdeal) is the order of I along Y of [BM97, §3] and Hironaka's ν(J_x) at the points of the centre [Hir64, Ch. 0, §5, p. 142]; Kollár defines the order along an irreducible Z at its generic point [Kol07, Definition 47]. This file proves that the order is

• at most the order at a (ordAlong_le_ord, since I_{Y,a} ⊆ 𝔪_a);
• locally constant on Y, hence constant on preconnected subsets of Y (ordAlong_eq_of_isPreconnected): in an adapted chart at b ∈ Y, I_b ⊆ I_{Y,b}^p iff all iterated derivatives of the local generators along fewer than p centre coordinates vanish on Y near b (stalkIdeal_le_pow_iff, the Taylor criterion of Hironaka.Algebra.Local.PartialEuler read on the stalk through the coordinate derivations and the restriction of germs to Y), and a section vanishing on Y near one point of a connected chart ball of Y vanishes on Y near every point of the ball, by the identity theorem for analytic functions on the chart of Y (eventually_zero_on_of_eventually_zero); so the order is constant on the ball (exists_open_ordAlong_eq), locally constant on Y (isLocallyConstant_ordAlong), and IsLocallyConstant.apply_eq_of_isPreconnected finishes;
• the generic order along the component through a (genericOrdAlong_eq_ordAlong);
• for connected Y, ≥ p at one point iff the order of I is ≥ p at every point of Y (le_ordAlong_iff_forall_le_ord; the converse direction reads the derivatives of order < p vanishing at every point of Y near a, through the lowering of the power of the maximal ideal by a coordinate derivative (iterD_mem_pow), as the vanishing on Y of the coefficient functions).

The constancy of the order along a connected centre is what makes the exponent of Hironaka's weak transform well defined; the order along a centre is the quantity the order-reduction arguments of Hironaka.Manifold.Sequence.OrderReduction track.

def Manifold.centreIdx {n c : ℕ} (σ : Fin c ↪ Fin n) : Finset (Fin n)

The index set of the centre coordinates of an adapted chart.

Equations

• Manifold.centreIdx σ = Finset.map σ Finset.univ

theorem Manifold.coe_centreIdx {n c : ℕ} (σ : Fin c ↪ Fin n) : ↑(centreIdx σ) = Set.range ⇑σ

The centre indices as a set: the range of σ.

theorem Manifold.mem_centreIdx {n c : ℕ} {σ : Fin c ↪ Fin n} {j : Fin n} : j ∈ centreIdx σ ↔ ∃ (k : Fin c), σ k = j

Membership in the centre indices.

theorem Manifold.coordDerivStalk_coord_eq_ite {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) (i j : Fin n) : (coordDerivStalk E ψ φ hφ hb i) (coord E ψ φ hφ hb j) = if i = j then 1 else 0

∂_i x_j = δ_ij on the coordinate germs, as an element of the stalk.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_coordIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hY : IsClosedSubmanifold ψ Y c) (hφ : IsAdaptedChart ψ Y φ σ) {b : M} (hb : b ∈ Y) (hbφ : b ∈ φ.source) : hY.idealSheaf.stalkIdeal b = IsLocalRing.coordIdeal (fun (i : Fin n) => coord E ψ φ ⋯ hbφ i) (centreIdx σ)

At a point of Y in an adapted chart, the stalk of I_Y is the coordinate ideal J_S of the centre indices.

noncomputable def Manifold.iterDSec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} (hφm : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (l : List (Fin n)) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

Iterated coordinate derivatives of a section along a list of indices (coordDeriv on sections).

Equations

• Manifold.iterDSec ψ hφm V hV l f = List.foldr (fun (i : Fin n) (g : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) => (Manifold.coordDeriv E ψ φ hφm V hV i) g) f l

theorem Manifold.germ_iterDSec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} (hφm : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) {b : M} (hbV : b ∈ V) (l : List (Fin n)) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hbV)) (iterDSec ψ hφm V hV l f) = IsLocalRing.iterD (fun (i : Fin n) => coordDerivStalk E ψ φ hφm ⋯ i) l ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hbV)) f)

The germ of the iterated derivative is the iterated stalk derivative.

theorem Manifold.eval_germ' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (V : TopologicalSpace.Opens M) {b : M} (hbV : b ∈ V) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (eval 𝕜 E M b) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hbV)) g) = extendSection 𝕜 E g b

The value of a germ is the value of the section.

theorem Manifold.IsClosedSubmanifold.germ_mem_stalkIdeal_idealSheaf_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (V : TopologicalSpace.Opens M) (hY : IsClosedSubmanifold ψ Y c) {b : M} (hb : b ∈ Y) (hbV : b ∈ V) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hbV)) g ∈ hY.idealSheaf.stalkIdeal b ↔ ∀ᶠ (y : ↑Y) in nhds ⟨b, hb⟩, extendSection 𝕜 E g ↑y = 0

A germ at b ∈ Y lies in the ideal of Y iff the section vanishes on Y near b.

theorem Manifold.stalkIdeal_le_pow_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (hY : IsClosedSubmanifold ψ Y c) (hφ : IsAdaptedChart ψ Y φ σ) {b : M} (hb : b ∈ Y) (hbV : b ∈ V) (I : IdealSheaf (structureSheaf 𝕜 E M)) {k : ℕ} (f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) (hgen : I.stalkIdeal b = Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hbV)) (f j))) (p : ℕ) : I.stalkIdeal b ≤ hY.idealSheaf.stalkIdeal b ^ p ↔ ∀ (j : Fin k) (l : List (Fin n)), (∀ i ∈ l, i ∈ centreIdx σ) → l.length < p → ∀ᶠ (y : ↑Y) in nhds ⟨b, hb⟩, extendSection 𝕜 E (iterDSec ψ ⋯ V hV l (f j)) ↑y = 0

The Taylor criterion on the manifold: I_b ⊆ I_{Y,b}^p iff all iterated derivatives of the local generators along fewer than p centre coordinates vanish on Y near b.

theorem ENat.le_of_forall_natCast_le' {x y : ℕ∞} (h : ∀ (p : ℕ), ↑p ≤ x → ↑p ≤ y) : x ≤ y

x ≤ y in ℕ∞ when every natural lower bound of x bounds y.

theorem Manifold.analyticAt_embedCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (w : Fin (n - c) → 𝕜) : AnalyticAt 𝕜 (embedCompl σ) w

The coordinate embedding 𝕜^{n-c} → 𝕜^n of the adapted charts is analytic (linear).

theorem Manifold.eventually_zero_on_of_eventually_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) {b : M} (hb : b ∈ Y) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (g : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) {W : Set ↑Y} (hWo : IsOpen W) (hWc : IsPreconnected W) (hWV : ∀ y ∈ W, ↑y ∈ V) {y₀ : ↑Y} (hy₀ : y₀ ∈ W) (h0 : ∀ᶠ (y : ↑Y) in nhds y₀, extendSection 𝕜 E g ↑y = 0) (y : ↑Y) : y ∈ W → ∀ᶠ (y' : ↑Y) in nhds y, extendSection 𝕜 E g ↑y' = 0

The identity theorem on a connected chart ball of Y: a section of 𝒪_M vanishing on Y near one point of a preconnected open W ⊆ Y inside an adapted chart vanishes on Y near every point of W.

theorem Manifold.exists_generators_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (φ : OpenPartialHomeomorph M E) (haφ : a ∈ φ.source) : ∃ (V : TopologicalSpace.Opens M) (_ : ↑V ⊆ φ.source) (_ : a ∈ V) (k : ℕ) (f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))), ∀ (y : M) (hy : y ∈ V), I.stalkIdeal y = Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V y hy)) (f j))

Restricting local generators of I to a smaller open set.

theorem Manifold.exists_open_ordAlong_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {b : M} (hb : b ∈ Y) : ∃ (W : Set ↑Y), IsOpen W ∧ ⟨b, hb⟩ ∈ W ∧ ∀ y ∈ W, hY.idealSheaf.ordAlongIdeal I ↑y = hY.idealSheaf.ordAlongIdeal I b

The order along Y is locally constant on Y.

theorem Manifold.IsClosedSubmanifold.isLocallyConstant_ordAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) : IsLocallyConstant fun (y : ↑Y) => hY.idealSheaf.ordAlongIdeal I ↑y

The order along Y is a locally constant function on Y.

theorem Manifold.ordAlong_eq_of_isPreconnected {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {S : Set M} (hSY : S ⊆ Y) (hS : IsPreconnected S) {a b : M} (ha : a ∈ S) (hb : b ∈ S) : hY.idealSheaf.ordAlongIdeal I a = hY.idealSheaf.ordAlongIdeal I b

The order along Y is constant on preconnected subsets of Y (the generic value of the order along the centre, [BM97, Remark 1.8]).

theorem Manifold.genericOrdAlong_eq_ordAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) : hY.idealSheaf.genericOrdAlong I a = hY.idealSheaf.ordAlongIdeal I a

The generic order along the component through a ∈ Y is the order along Y at a.

theorem Manifold.ordAlong_le_ord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) : hY.idealSheaf.ordAlongIdeal I a ≤ I.ord a

The order along Y at a ∈ Y is at most the order at a.

theorem Manifold.stalkIdeal_le_pow_of_eventually_le_ord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) {p : ℕ} (h : ∀ᶠ (y : ↑Y) in nhds ⟨a, ha⟩, ↑p ≤ I.ord ↑y) : I.stalkIdeal a ≤ hY.idealSheaf.stalkIdeal a ^ p

If the order of I is at least p at the points of Y near a, then I_a ⊆ I_{Y,a}^p.

theorem Manifold.le_ordAlong_iff_forall_le_ord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hconn : IsPreconnected Y) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) (p : ℕ) : ↑p ≤ hY.idealSheaf.ordAlongIdeal I a ↔ ∀ y ∈ Y, ↑p ≤ I.ord y

For connected Y, ν_{Y,a}(I) ≥ p at one point iff ν_y(I) ≥ p at every point of Y.