Pullback of ideal sheaves under analytic maps

For an analytic map φ : N → M and an ideal sheaf J of the structure sheaf of M, the pullback φ^* J = IdealSheaf.pullback J φ hφ is the ideal sheaf generated by the f ∘ φ, f a section of J: Hironaka's total transform f⁻¹(J), "the one generated by J with reference to f" [Hir64, pp. 141–142], and Bierstone–Milman's σ⁻¹(I) := σ^*(I) · 𝒪 [BM97, Theorem 1.10].

• Its stalk at b is the image of J_{φ b} under the stalk map germMap φ hφ b (stalkIdeal_pullback), generated near b by the germs of the f_i ∘ φ for local generators f_i of J (stalkIdeal_pullback_eq_span).
• It is monotone (pullback_le_pullback), multiplicative (pullback_mul, pullback_pow, pullback_top), and the identity pulls back to the identity (pullback_id_eq_self); V(φ^* J) = φ⁻¹ V(J) (support_pullback, the stalk map being a local homomorphism).
• The order does not drop under pullback (ord_le_ord_pullback) and is preserved at a point where φ is a local analytic isomorphism (ord_pullback_of_isLocalDiffeomorphAt: the stalk map of a local inverse is a two-sided inverse).
• Along a diffeomorphism g, the vanishing ideal of g⁻¹ Z at x pulls back to the vanishing ideal of Z at g x (comap_germMap_vanishingStalk).

The pullback is the total transform of the analytic main theorems (the inverse image J.pullback f f.contMDiff along an analytic map f) and the inverse image along the blow-ups and local isomorphisms of the resolution (Hironaka/Manifold/BlowUp/).

theorem Ideal.map_eq_top_iff_of_isLocalHom {R : Type u_3} {S : Type u_4} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (g : R →+* S) [IsLocalHom g] (I : Ideal R) : map g I = ⊤ ↔ I = ⊤

Ideal.map under a local homomorphism is the unit ideal iff the ideal is.

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_pullback {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (b : N) : (pullback φ hφ J).stalkIdeal b = Ideal.map (germMap φ hφ b) (J.stalkIdeal (φ b))

theorem Manifold.IdealSheaf.pullback_le_pullback {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {J K : IdealSheaf (structureSheaf 𝕜 E M)} (h : J ≤ K) : pullback φ hφ J ≤ pullback φ hφ K

The pullback of ideal sheaves is monotone, for any models (stalkwise, Ideal.map is monotone; IdealSheaf.pullback_mono is the same-model form).

theorem Manifold.IdealSheaf.pullback_pow {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (k : ℕ) : pullback φ hφ (J ^ k) = pullback φ hφ J ^ k

The pullback of a power of an ideal sheaf is the power of the pullback (stalkwise, Ideal.map of a power).

theorem Manifold.IdealSheaf.stalkIdeal_pullback_eq_span {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (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))) {b : N} (hb : φ b ∈ U) : (pullback φ hφ J).stalkIdeal b = Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E' N).presheaf.germ (preimageOpens φ hφ U) b ⋯)) (comapSection φ hφ (f i)))

@[simp]

theorem Manifold.IdealSheaf.support_pullback {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : (pullback φ hφ J).support = φ ⁻¹' J.support

V(φ^* J) = φ⁻¹ V(J).

theorem Manifold.IdealSheaf.ord_le_ord_pullback {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (b : N) : J.ord (φ b) ≤ (pullback φ hφ J).ord b

The order does not drop under pullback (IsLocalRing.ord_le_ord_map).

theorem Manifold.IdealSheaf.ord_pullback_of_isLocalDiffeomorphAt {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (h : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ b) : (pullback φ hφ J).ord b = J.ord (φ b)

For a local isomorphism φ at b, the stalk map has the stalk map of a local inverse as a two-sided inverse, so ν_b(φ^* J) = ν_{φ(b)}(J).

Pullback algebra and the germ map of a diffeomorphism

theorem Manifold.IdealSheaf.pullback_mul {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (I J : IdealSheaf (structureSheaf 𝕜 E M)) : pullback φ hφ (I * J) = pullback φ hφ I * pullback φ hφ J

The pullback of a product of ideal sheaves is the product of the pullbacks (stalkwise, Ideal.map of a product).

theorem Manifold.IdealSheaf.pullback_top {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) : pullback φ hφ ⊤ = ⊤

The pullback of the unit ideal sheaf is the unit ideal sheaf.

theorem Manifold.IdealSheaf.pullback_id_eq_self {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) : pullback id ⋯ J = J

theorem Manifold.comap_germMap_vanishingStalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u_3} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u_4} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) (Z : Set M₂) (x : M₁) : Ideal.comap (germMap ⇑g ⋯ x) (vanishingStalk (⇑g ⁻¹' Z) x) = vanishingStalk Z (g x)

The vanishing ideal of g⁻¹ Z at x pulls back along the germ map of the diffeomorphism g to the vanishing ideal of Z at g x.