Cosupport and order of an ideal sheaf on an analytic manifold

For a locally finitely generated ideal sheaf J of the structure sheaf of an analytic manifold:

• the cosupport V(J) is, on a generating open set U, the common zero set of the generators (mem_cosupport_iff_forall_eq_zero: a germ is a unit iff its value is nonzero) — Bierstone–Milman's V(I) = {x : f(x) = 0 for all f ∈ I} [BM97, Introduction];
• the order ν_a(J) [Hir64, p. 133] is read on the Taylor series in a chart: the order of a germ is the order of its Taylor series (ordElem_eq_order_taylorHom, through taylorHom_mem_maximalIdeal_pow_iff), ν_a(J) = min_i ord T_a(f_i) over local generators (ord_eq_iInf_order_taylorHom; the order of a function at a point in the sense of Bierstone–Milman [BM97, §3]), ν_a(J) ≥ p iff the Taylor coefficients of degree < p of the generators vanish (le_ord_iff_forall_coeff_eq_zero), and ν_a(J) = ∞ iff J_a = 0 (ord_eq_top_iff, the Taylor homomorphism being injective).

Also here: modelCoord, coordinates on the finite-dimensional model space, the chart coordinates used whenever a statement is chart-free. The order is the invariant the order-reduction algorithm lowers.

theorem Manifold.IdealSheaf.mem_support_iff_forall_eq_zero {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) {U : TopologicalSpace.Opens M} {k : ℕ} {f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))} (hgen : ∀ (b : M) (hb : b ∈ U), J.stalkIdeal b = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U b hb)) (f i))) {a : M} (ha : a ∈ U) : a ∈ J.support ↔ ∀ (i : Fin k), ↑(f i) ⟨a, ha⟩ = 0

On a generating open set, V(J) ∩ U is the common zero set of the generators ([BM97, Introduction]): a germ is a unit iff its value is nonzero.

theorem Manifold.IdealSheaf.ordElem_eq_order_taylorHom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : IsLocalRing.ordElem s = ((taylorHom E ψ φ ha hφ) s).order

The order of a germ is the order of its Taylor series.

theorem Manifold.IdealSheaf.ord_eq_iInf_order_taylorHom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (J : IdealSheaf (structureSheaf 𝕜 E M)) {U : TopologicalSpace.Opens M} (haU : a ∈ U) {k : ℕ} {f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))} (hgen : ∀ (b : M) (hb : b ∈ U), J.stalkIdeal b = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U b hb)) (f i))) : J.ord a = ⨅ (i : Fin k), ((taylorHom E ψ φ ha hφ) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a haU)) (f i))).order

ν_a(J) = min_i ord T_a(f_i) for local generators [BM97, §3].

theorem Manifold.IdealSheaf.le_ord_iff_forall_coeff_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (J : IdealSheaf (structureSheaf 𝕜 E M)) {U : TopologicalSpace.Opens M} (haU : a ∈ U) {k : ℕ} {f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))} (hgen : ∀ (b : M) (hb : b ∈ U), J.stalkIdeal b = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U b hb)) (f i))) (p : ℕ) : ↑p ≤ J.ord a ↔ ∀ (i : Fin k) (ν : Fin n →₀ ℕ), Finsupp.degree ν < p → (MvPowerSeries.coeff ν) ((taylorHom E ψ φ ha hφ) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a haU)) (f i))) = 0

ν_a(J) ≥ p iff the Taylor coefficients of degree < p of the generators vanish.

noncomputable def Manifold.IdealSheaf.modelCoord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : E ≃L[𝕜] Fin (Module.finrank 𝕜 E) → 𝕜

Coordinates on the finite-dimensional model space.

Equations

• Manifold.IdealSheaf.modelCoord = (Module.finBasis 𝕜 E).equivFun.toContinuousLinearEquiv

theorem Manifold.IdealSheaf.ord_eq_top_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) (a : M) : J.ord a = ⊤ ↔ J.stalkIdeal a = ⊥

ν_a(J) = ∞ iff J_a = 0 (the Taylor homomorphism is injective).