The inverse image of an ideal sheaf along the morphism of an analytic map

The stalk map of Sp(f) at x, for an analytic map f : M → N (ofManifoldHom: precomposition of sections with f), is the map germMap f x of germs, composition with f (stalkMap_ofManifoldHom_eq_germMap). Consequently the inverse image QuotientSpace.comap Sp(f) J of an ideal sheaf J on N, defined for a morphism of locally ringed spaces as the ideal sheaf generated stalkwise by the image of J (the body of AnalyticSpace.ClosedSubspace.comap, the inverse image of a closed subspace used in the statements of the analytic main theorems), is the pullback J.pullback f defined on the manifold side (comap_ofManifoldHom_eq_pullback).

For the morphism of spaces of a blow-up this identifies the inverse image of a closed subspace with the total transform of its ideal sheaf on the manifold [Hir64, Ch. 0, §5, p. 141], and the inverse image of the centre with the exceptional ideal sheaf. It is used wherever the analytic-space inverse image and the manifold pullback have to be compared, chiefly the modules of Hironaka.Manifold.Sequence.Restrict that read ideal sheaves on manifolds as closed subspaces.

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_ofManifoldHom_eq_germMap {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace K E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (f : M → N) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (x : M) (s : ↑((Manifold.structureSheaf K E' N).presheaf.stalk (f x))) : (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(ofManifoldHom f hf)) x)) s = (Manifold.germMap f hf x) s

The stalk map of Sp(f) is the map of germs germMap f x: both send the germ of a section g at f x to the germ of g ∘ f at x.

theorem AnalyticSpace.KLocallyRingedSpace.comap_ofManifoldHom_eq_pullback {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace K E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (f : M → N) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (J : Manifold.IdealSheaf (Manifold.structureSheaf K E' N)) : QuotientSpace.comap (↑(ofManifoldHom f hf)) J = Manifold.IdealSheaf.pullback f hf J

The inverse image along Sp(f) of an ideal sheaf on N is its pullback along f: stalkwise, the ideal generated by the image of the stalk ideal under the stalk map [Hir64, Ch. 0, §5, p. 141].