Flags of closed submanifolds and their ideal sheaves

Ideal-sheaf bookkeeping along a flag S ⊂ Y ⊂ M of closed submanifolds, as in Kollár's reduction of the functoriality for closed embeddings to the case of a hypersurface [Kol07, 108]: locally there is a chain of smooth subvarieties Y = Y_0 ⊂ Y_1 ⊂ ⋯ ⊂ Y_c = X such that "each is a hypersurface in the next one".

• IsClosedSubmanifold.idealSheaf_le_of_subset: a closed submanifold contained in another has the larger reduced ideal sheaf (both have the vanishing stalks, which are antitone in the set);
• IsClosedSubmanifold.idealSheaf_preimage_of_isLocalDiffeomorph: the ideal sheaf of the preimage of a closed submanifold under a local analytic isomorphism is the pull-back of its ideal sheaf (comap_idealSheaf_of_isLocalDiffeomorph read backwards; the pull-back of a blow-up centre along a smooth morphism, [Kol07, 30.1]);
• IsAdaptedChart.exists_flag: from one adapted chart of S of codimension s + 1 whose source is the whole manifold, the zero set Y of the first s adapted coordinates is a closed submanifold of codimension s containing S, and S is a hypersurface of the bundled Y (IsClosedSubmanifold.preimage_val_of_subset at codimension (s + 1) − s);
• IsClosedSubmanifold.pullback_idealSheaf_inclusionMap: the pull-back to the bundled Y of the reduced ideal sheaf of S ⊆ Y is the reduced ideal sheaf of S in Y, for any closed-submanifold structure on S in Y (the hypothesis S ⊆ Y is needed: a hypersurface tangent to Y is a counterexample);
• IdealSheaf.isNonzeroEverywhere_pullback_inclusionMap_of_le: an ideal sheaf I ⊇ 𝓘_S whose pull-back to S is nonzero everywhere pulls back to Y ⊇ S nonzero everywhere — off S its stalk is the unit ideal; at a point of S, a zero pull-back to Y means every germ of I lies in the kernel of the germ map of Y, the stalk of 𝓘_Y ≤ 𝓘_S, so the pull-back to S is zero too (the hypothesis 𝓘_S ≤ I is needed: an I equal to 𝓘_Y along a component of Y missing S is a counterexample).

Everything is assembled from the reduced ideal sheaf of a closed submanifold (vanishing stalks, stalkIdeal_idealSheaf_eq_vanishingStalk), the germ map of the inclusion (onto, with kernel the stalk of the reduced ideal, germMap_inclusionMap) and the relative closed-submanifold structure (IsClosedSubmanifold.preimage_val_of_subset, idealSheaf_preimageVal_eq_pullback). These lemmas are used for the commutation of the resolution with closed embeddings in general codimension (Hironaka/Resolution/Analytic/Functor/ChainClosedEmbeddingChain.lean).

theorem Manifold.IsClosedSubmanifold.idealSheaf_le_of_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y S : Set M.carrier} {c c' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hS : IsClosedSubmanifold ψ S c') (hSY : S ⊆ Y) : hY.idealSheaf ≤ hS.idealSheaf

A closed submanifold contained in another has the larger reduced ideal sheaf (𝓘_Y ⊆ 𝓘_S along the flag of [Kol07, 108]): both have the vanishing stalks, which are antitone in the set.

theorem Manifold.IsClosedSubmanifold.idealSheaf_preimage_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : ⋯.idealSheaf = IdealSheaf.pullback ⇑h ⋯ hY.idealSheaf

The ideal sheaf of the preimage of a closed submanifold under a local analytic isomorphism is the pull-back of its ideal sheaf ([Kol07, 30.1]): comap_idealSheaf_of_isLocalDiffeomorph read backwards (comap is the pull-back by definition).

theorem Manifold.IsAdaptedChart.exists_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S (s + 1)) {φ : OpenPartialHomeomorph M.carrier E} {σ : Fin (s + 1) ↪ Fin n} (hφ : IsAdaptedChart ψ S φ σ) (hsrc : φ.source = Set.univ) : ∃ (Y : Set M.carrier) (hY : IsClosedSubmanifold ψ Y s), S ⊆ Y ∧ IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1

The flag S ⊂ Y ⊂ M from one adapted chart ([Kol07, 108], read from the bottom): from an adapted chart of S (codimension s + 1) whose source is the whole manifold, the zero set Y of the first s adapted coordinates is a closed submanifold of codimension s containing S, and S is a hypersurface of the bundled Y (IsClosedSubmanifold.preimage_val_of_subset at codimension (s + 1) - s).

theorem Manifold.IsClosedSubmanifold.pullback_idealSheaf_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y S : Set M.carrier} {c c' c'' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hS : IsClosedSubmanifold ψ S c') (hSY' : S ⊆ Y) (hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - c) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) c'') : IdealSheaf.pullback ⇑hY.inclusionMap ⋯ hS.idealSheaf = hSY.idealSheaf

The pull-back to the bundled Y of the reduced ideal sheaf of S ⊆ Y is the reduced ideal sheaf of S as a closed submanifold of Y, for any closed-submanifold structure on S in Y (idealSheaf_preimageVal_eq_pullback; the two structures on the same set have the same reduced ideal sheaf, both with the vanishing stalks). The hypothesis S ⊆ Y is needed: a hypersurface tangent to Y is a counterexample.

theorem Manifold.IsClosedSubmanifold.ker_germMap_inclusionMap' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {c : ℕ} (hS : IsClosedSubmanifold ψ S c) (p : hS.toAnalyticManifold.carrier) : RingHom.ker (germMap ⇑hS.inclusionMap ⋯ p) = hS.idealSheaf.stalkIdeal (hS.inclusionMap p)

The kernel of the germ map of the inclusion of a closed submanifold at p is the stalk of its reduced ideal sheaf at p (germMap_inclusionMap and stalkIdeal_idealSheaf_of_mem, at a general model).

theorem Manifold.IdealSheaf.isNonzeroEverywhere_pullback_inclusionMap_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y S : Set M.carrier} {c c' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hS : IsClosedSubmanifold ψ S c') (hSY : S ⊆ Y) (I : M.IdealSheaf) (hle : hS.idealSheaf ≤ I) (hJ : (pullback ⇑hS.inclusionMap ⋯ I).IsNonzeroEverywhere) : (pullback ⇑hY.inclusionMap ⋯ I).IsNonzeroEverywhere

An ideal sheaf containing 𝓘_S whose pull-back to S is nonzero everywhere pulls back to Y ⊇ S nonzero everywhere: off S its stalk is the unit ideal; at a point of S, a zero pull-back to Y means every germ of I lies in the kernel of the germ map of Y, the stalk of 𝓘_Y ≤ 𝓘_S, so the pull-back to S is zero too. The hypothesis 𝓘_S ≤ I is needed: an I equal to 𝓘_Y along a component of Y missing S is a counterexample.