The space of a closed submanifold is the closed subspace cut out by its ideal sheaf #
For a closed submanifold Y ⊆ M of an analytic manifold (IsClosedSubmanifold, with its induced
charts), the analytic space Sp(Y) is K-isomorphic to the closed subspace Sp(M) / 𝓘_Y of
Sp(M) cut out by the ideal sheaf 𝓘_Y = hY.idealSheaf of the functions vanishing on Y,
compatibly with the inclusion Y → M (toSpace_closedSubmanifold,
toSpace_closedSubmanifold_comp). Thus the closed submanifolds of M are closed subspaces of
Sp(M) in the sense of [Hir64, Ch. 0, §1, p. 119] (a local analytic K-space is
(S(I), (𝒜_G/I)|S(I))) and of [BM97, §3] (a closed subspace is defined by an ideal sheaf of finite
type). The comparison is used to read a closed submanifold, the exceptional divisor of a blow-up, as
a closed subspace of the analytic space
(Hironaka.Resolution.Analytic.Wlo09.PreimageSing); the local description of the sections
of the quotient sheaf (exists_local_rep) is used in the gluing of local resolutions
(Hironaka.Resolution.Analytic.Kol07Thm45.PieceLemma39Model).
The morphism closedHom : Sp(Y) ⟶ Sp(M) / 𝓘_Y is built directly:
- its base is the identification of
Ywith the cosupport of𝓘_Y(cosupport_idealSheaf:S(𝓘_Y) = Y); - a section of the quotient sheaf over
Vis a compatible family of classess_z ∈ 𝒪_{M,z}/𝓘_{Y,z}; since𝓘_{Y,z}is proper it lies in the maximal ideal, so evaluation atzdescends to the fibre (fiberEval), andy ↦ ev_y(s_y)is an analytic function onY ∩ V, being locally the restriction toYof the ambient section representings(exists_local_rep,contMDiff_closedSectionFun); - on stalks the map is
𝒪_{M,y}/𝓘_{Y,y} → 𝒪_{Y,y}induced by the restriction of germsrestrictStalk(stalkMap_closedHomAux_eq), a bijection becauserestrictStalkis onto with kernel exactly𝓘_{Y,y}(bijective_fiberRestrict); - a morphism of locally ringed spaces that is a homeomorphism on points and an isomorphism on every
stalk is an isomorphism (Mathlib's stalk criterion); the
K-structure is respected because constants evaluate to constants.
The composite with the canonical morphism Sp(M)/𝓘_Y ⟶ Sp(M) is Sp of the inclusion
(closedHom_comp_quotientι), by the extensionality of morphisms between spaces of manifolds on
their underlying maps (hom_ext_baseFun).
A compatible germ family on the quotient of Sp(M) is, near each point of its domain, the
family of the classes of one ambient analytic function (the local predicate defining the quotient
sheaf, unfolded).
On the cosupport of 𝒥, the stalk ideal 𝒥_z is proper, hence contained in the maximal ideal,
which is the kernel of evaluation.
Evaluation at z on the fibre 𝒪_{M,z}/𝒥_z of a point of the cosupport.
Equations
- AnalyticSpace.KLocallyRingedSpace.fiberEval J z = Ideal.Quotient.lift (J.stalkIdeal ↑z) (Manifold.eval K E M ↑z) ⋯
Instances For
The ideal sheaf 𝓘_Y of the closed submanifold, read as an ideal sheaf on the locally ringed
space Sp(M) (the same term; the retyping lets the quotient constructions apply). Internal to the
construction: the exported closedHom, closedHom_comp_quotientι, closedSubmanifoldIso and
toFun_closedSubmanifoldIso_hom_comp are typed with hY.idealSheaf.
Equations
Instances For
The points of a closed submanifold are the cosupport of its ideal sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The base map Y → S(𝓘_Y) of the comparison morphism.
Equations
- AnalyticSpace.KLocallyRingedSpace.closedBase hY = TopCat.ofHom { toFun := ⇑(AnalyticSpace.KLocallyRingedSpace.closedBaseHomeo hY), continuous_toFun := ⋯ }
Instances For
The function on Y ∩ V underlying the image of a section of the quotient sheaf over V:
the evaluation of its classes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The evaluated family is analytic on Y ∩ V: near each point it is the restriction to Y of the
ambient section representing the family.
The sheaf map of the comparison morphism, 𝒪_M/𝓘_Y ⟶ 𝒪_Y on Y = S(𝓘_Y): a compatible family
of classes goes to its evaluation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation.) The morphism of presheafed spaces Sp(Y) ⟶ Sp(M)/𝓘_Y.
Equations
Instances For
The fibre 𝒪_{M,y}/𝓘_{Y,y} maps to 𝒪_{Y,y} by the restriction of germs, 𝓘_{Y,y} being
its kernel.
Equations
- AnalyticSpace.KLocallyRingedSpace.fiberRestrict hY y = Ideal.Quotient.lift (hY.idealSheaf.stalkIdeal ↑y) (hY.restrictStalk y) ⋯
Instances For
The induced map 𝒪_{M,y}/𝓘_{Y,y} → 𝒪_{Y,y} is a bijection: restrictStalk is onto with kernel
𝓘_{Y,y}.
The stalk map of the comparison morphism is the restriction of germs through the
identification 𝒪_{Sp(M)/𝓘_Y, y} ≃ 𝒪_{M,y}/𝓘_{Y,y} (stalkEquiv).
(Implementation.) The morphism of locally ringed spaces Sp(Y) ⟶ Sp(M)/𝓘_Y.
Equations
- AnalyticSpace.KLocallyRingedSpace.closedHomL hY = { toHom := AnalyticSpace.KLocallyRingedSpace.closedHomAux hY, prop := ⋯ }
Instances For
The comparison K-morphism Sp(Y) ⟶ Sp(M)/𝓘_Y: the identification of Y with S(𝓘_Y) on
points, evaluation of classes on sections.
Equations
Instances For
The comparison morphism followed by the canonical morphism Sp(M)/𝓘_Y ⟶ Sp(M) is Sp of the
inclusion Y → M (a morphism into Sp(M) is determined by its points, hom_ext_baseFun).
The comparison morphism is an isomorphism: a homeomorphism on points, an isomorphism on every stalk.
Sp(Y) ≅ Sp(M)/𝓘_Y, the K-isomorphism given by the comparison morphism.
Equations
Instances For
Sp sends a closed submanifold Y to the closed subspace of Sp(M) cut out by its ideal
sheaf, compatibly with the inclusion on points.
Sp(Y) ≅ Sp(M)/𝓘_Y composed with the canonical morphism is Sp of the inclusion: the
morphism form of toSpace_closedSubmanifold.