Locality of the derivative ideal sheaves

Kollár's D(f^*I) = f^*(D(I)) for a smooth morphism f [Kol07, Lemma 74 (4)], proved here for the maps the Hironaka library needs — local analytic isomorphisms, in particular the inclusion of an open subset (the "local question" clause at the start of the proof of [Kol07, Theorem 80]) and the blow-down off the centre. At a point b where φ is a local analytic isomorphism the germ map 𝒪_{M, φ b} → 𝒪_{N, b} is a ring isomorphism respecting 𝕜 (germMap_bijective_of_isLocalDiffeomorphAt), and Ideal.derivative_map_ringEquiv transports Kollár's derivative ideal along it; the derivative ideal sheaves are determined by their stalks (stalkIdeal_deriv). Hence D^j(φ^* J) = φ^*(D^j(J)) for a local analytic isomorphism (iteratedDeriv_pullback_of_isLocalDiffeomorph) and D^j(J|_U) = (D^j J)|_U for an open subset (iteratedDeriv_restrictOpens).

Also here, for local analytic isomorphisms: the vanishing ideal of a preimage along a diffeomorphism is the image of the vanishing ideal under the germ map (vanishingStalk_preimage_diffeomorph), the local-generator condition of the vanishing ideals is invariant under a diffeomorphism (hasLocalGenerators_vanishingStalk_preimage_iff), and an inequality of stalks at a point of the range of a local analytic isomorphism can be checked after pulling back (IdealSheaf.stalkIdeal_le_of_comap_le). These are the transport lemmas used when the resolution is built on charts and open subsets and glued (Hironaka/Resolution/Analytic/Functor/PullbackTransport.lean, Hironaka/Resolution/Analytic/MaximalContactTheorem.lean).

theorem Manifold.stalkIdeal_deriv_pullback_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (hb : Function.Bijective ⇑(germMap φ hφ b)) : (IdealSheaf.pullback φ hφ J).deriv.stalkIdeal b = (IdealSheaf.pullback φ hφ J.deriv).stalkIdeal b

At a point where the germ map is bijective, the stalk of D(φ^* J) is the stalk of φ^*(D(J)) (Ideal.derivative_map_ringEquiv).

theorem Manifold.deriv_pullback_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (hb : ∀ (b : N), Function.Bijective ⇑(germMap φ hφ b)) : (IdealSheaf.pullback φ hφ J).deriv = IdealSheaf.pullback φ hφ J.deriv

If the germ map is bijective at every point, D(φ^* J) = φ^*(D(J)).

theorem Manifold.iteratedDeriv_pullback_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (hb : ∀ (b : N), Function.Bijective ⇑(germMap φ hφ b)) (j : ℕ) : (IdealSheaf.pullback φ hφ J).iteratedDeriv j = IdealSheaf.pullback φ hφ (J.iteratedDeriv j)

If the germ map is bijective at every point, D^j(φ^* J) = φ^*(D^j(J)).

theorem Manifold.germMap_bijective_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) {b : N} (h : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ b) : Function.Bijective ⇑(germMap φ hφ b)

At a point where φ is a local analytic isomorphism, the germ map is bijective: the germ map of a local inverse is a two-sided inverse.

theorem Manifold.stalkIdeal_deriv_pullback_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ b) : (IdealSheaf.pullback φ hφ J).deriv.stalkIdeal b = (IdealSheaf.pullback φ hφ J.deriv).stalkIdeal b

Locality of D ([Kol07, Lemma 74 (4)] at a point where φ is a local analytic isomorphism): the stalk of D(φ^* J) at b is the stalk of φ^*(D(J)).

theorem Manifold.iteratedDeriv_pullback_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (hloc : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (j : ℕ) : (IdealSheaf.pullback φ hφ J).iteratedDeriv j = IdealSheaf.pullback φ hφ (J.iteratedDeriv j)

Locality of D ([Kol07, Lemma 74 (4)] for a local analytic isomorphism φ): D^j(φ^* J) = φ^*(D^j(J)).

The vanishing ideals along a diffeomorphism

theorem Manifold.vanishingStalk_preimage_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) (Z : Set M₂.carrier) (x : M₁.carrier) : vanishingStalk (⇑g ⁻¹' Z) x = Ideal.map (germMap ⇑g ⋯ x) (vanishingStalk Z (g x))

Along a diffeomorphism the vanishing ideal of the preimage is the image of the vanishing ideal under the (bijective) germ map.

theorem Manifold.hasLocalGenerators_vanishingStalk_preimage_of {𝕜 : Type} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) (W : Set M₂.carrier) (h : IdealSheaf.HasLocalGenerators fun (y : M₂.carrier) => vanishingStalk W y) : IdealSheaf.HasLocalGenerators fun (x : M₁.carrier) => vanishingStalk (⇑g ⁻¹' W) x

Local generators of the vanishing ideals transport along a diffeomorphism (the pullback of the ideal sheaf they define).

theorem Manifold.hasLocalGenerators_vanishingStalk_preimage_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) (W : Set M₂.carrier) : (IdealSheaf.HasLocalGenerators fun (x : M₁.carrier) => vanishingStalk (⇑g ⁻¹' W) x) ↔ IdealSheaf.HasLocalGenerators fun (y : M₂.carrier) => vanishingStalk W y

The local-generator condition of the vanishing ideals is invariant under a diffeomorphism.

theorem AnalyticManifold.IdealSheaf.iteratedDeriv_restrictOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (U : TopologicalSpace.Opens M.carrier) (j : ℕ) : Manifold.IdealSheaf.iteratedDeriv (J.restrict U) j = restrict (Manifold.IdealSheaf.iteratedDeriv J j) U

Locality of D for the inclusion of an open subset ([Kol07, Lemma 74 (4)]; "being a hypersurface of maximal contact is a local question", [Kol07, Theorem 80, proof]): the derivative ideal sheaves of the restriction of J to an open U are the restrictions of the derivative ideal sheaves of J, D^j(J|_U) = (D^j J)|_U (the germ map of the inclusion is bijective, germMap_val_bijective).

Stalk inequalities along a local isomorphism

theorem Manifold.IdealSheaf.stalkIdeal_le_of_comap_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) {A B : M.IdealSheaf} (y : N.carrier) (h : (pullback ⇑g ⋯ A).stalkIdeal y ≤ (pullback ⇑g ⋯ B).stalkIdeal y) : stalkIdeal A (g y) ≤ stalkIdeal B (g y)

An inequality of stalks at a point of the range of a local analytic isomorphism g can be checked after pulling back along g: the germ map is bijective.