Documentation

Hironaka.AnalyticSpace.ClosedSubspaceAnalytic

The local-model clause for a closed subspace of an analytic K-space #

A closed analytic subspace of an analytic K-space is given by a coherent ideal sheaf [Hir64, Ch. 0, ยง1]; it is the quotient (S(๐“˜), (๐’ช_X/๐“˜)|_{S(๐“˜)}) [BM97, ยง3], and its local models are V(fโ‚, โ€ฆ, f_k, gโ‚, โ€ฆ, g_l): the ambient model of X cut out further by ambient lifts of local generators of ๐“˜. This file proves that clause (quotient_locallyModel), the local-model field of the closed subspace as an analytic K-space (closedSubspace).

The general identification. The first section extends the identification of Hironaka/AnalyticSpace/LocalModelRestrict.lean from the model ideal to any finite-type ideal sheaf ๐’ฅ on (G, ๐’œ_G): if ๐’ฅ has local generators g over an open O of G whose image in Kโฟ is G', then the restriction of ๐’ฅ to O, transported along the trace isomorphism (G, ๐’œ_G)|O โ‰… (G', ๐’œ_{G'}), is the model ideal of the g read as analytic functions on G' (transportIdeal_restrictIdeal_eq_modelIdeal; the g live on the image of O, which is G' โ€” functor_obj_eq, generatorsOn). The proof is the same ambient-stalk comparison: stalks of ๐’ฅ over O are images of the ambient ideals of the g (stalkIdeal_eq_map_ambientIdealOf, by Mathlib's restrictStalkIso_inv_eq_germ_apply), pulling back composes stalk maps (stalkIdeal_comap_of_generators), and the inclusion through the trace followed by the open immersion of G is the open immersion of G'.

The local-model clause (quotient_locallyModel). At a point y of Z = X/๐’ฅ with image x โˆˆ X: a chart of X at x, X|U โ‰… (S(๐“˜), โ€ฆ)|W, is (an open of a local model being a local model) a chart X|U โ‰… (S(๐“˜โ‚), โ€ฆ) = (Gโ‚, ๐’œ_{Gโ‚})/๐“˜โ‚; restriction commutes with the quotient, so the open Z|U' over U is (X|U)/(๐’ฅ|U); transporting along the chart makes it a quotient of (Gโ‚, ๐’œ_{Gโ‚})/๐“˜โ‚, hence (a quotient of a quotient) the quotient of (Gโ‚, ๐’œ_{Gโ‚}) by the lifted ideal sheaf ๐’ฅฬƒ, whose local generators near the image point are the f_i and the ambient lifts g_j; on the trace open Gโ‚‚ of those generators, the general identification makes Z over it the local model (S(๐“˜โ‚‚), โ€ฆ), ๐“˜โ‚‚ = (gโ‚, โ€ฆ, g_l) on Gโ‚‚. The remaining bookkeeping โ€” an open of an open is an open (restrictOpen_restrictOpen_iso), an isomorphism restricts over an open (restrictOpenIso), M|โŠค โ‰… M (restrictOpenTopIso) โ€” is in Hironaka/AnalyticSpace/OpenSubspaceLemmas.lean.

source
@[reducible, inline]
noncomputable abbrev AnalyticSpace.imageIn (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) :
TopologicalSpace.Opens (Kn K n)

The image in Kโฟ of an open O of (G, ๐’œ_G).

Equations
Instances For
    source
    theorem AnalyticSpace.functor_obj_eq (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' โ‰ค G) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : โˆ€ (p : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace), p โˆˆ O โ†” โ†‘p โˆˆ G') :
    imageIn K n G O = G'

    The image in Kโฟ of the trace open O is G'.

    source
    noncomputable def AnalyticSpace.generatorsOn (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' โ‰ค G) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : โˆ€ (p : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace), p โˆˆ O โ†” โ†‘p โˆˆ G') {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (i : Fin l) :
    AnalyticFun K n G'

    The generators g, read as analytic functions on G'.

    Equations
    Instances For
      source
      theorem AnalyticSpace.stalkMap_ofRestrict_germ' (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (q : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hq : q โˆˆ O) (i : Fin l) :
      (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘((affine K n).ofRestrict G)) q)) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ (imageIn K n G O) โ†‘q โ‹ฏ)) (g i)) = (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ O q hq)) (g i)
      source
      noncomputable def AnalyticSpace.ambientIdealOf (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (x : Kn K n) :
      Ideal โ†‘((affine K n).presheaf.stalk x)

      The ideal generated by the ambient germs of the g_i at a point of Kโฟ (the unit ideal off the image of O).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AnalyticSpace.ambientIdealOf_of_mem (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) {x : Kn K n} (h : x โˆˆ imageIn K n G O) :
        ambientIdealOf K n G O g x = Ideal.span (Set.range fun (i : Fin l) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ (imageIn K n G O) x h)) (g i))
        source
        theorem AnalyticSpace.stalkIdeal_eq_map_ambientIdealOf (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (J : Manifold.IdealSheaf (analyticSpaceOfOpen K n G).๐’ช) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (hg : โˆ€ (b : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hb : b โˆˆ O), QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace J b = Ideal.span (Set.range fun (i : Fin l) => (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ O b hb)) (g i))) (q : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hq : q โˆˆ O) :
        QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace J q = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘((affine K n).ofRestrict G)) q)) (ambientIdealOf K n G O g โ†‘q)

        On O, the stalks of J are the images of the ambient ideals.

        source
        theorem AnalyticSpace.stalkIdeal_comap_of_generators (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (J : Manifold.IdealSheaf (analyticSpaceOfOpen K n G).๐’ช) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (hg : โˆ€ (b : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hb : b โˆˆ O), QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace J b = Ideal.span (Set.range fun (i : Fin l) => (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ O b hb)) (g i))) {Y : KLocallyRingedSpace K} (ฯ† : Y โŸถ analyticSpaceOfOpen K n G) (hฯ† : โˆ€ (p : โ†‘โ†‘Y.toPresheafedSpace), (CategoryTheory.ConcreteCategory.hom (โ†‘ฯ†).base) p โˆˆ O) (p : โ†‘โ†‘Y.toPresheafedSpace) :
        (QuotientSpace.comap (โ†‘ฯ†) J).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘(CategoryTheory.CategoryStruct.comp ฯ† ((affine K n).ofRestrict G))) p)) (ambientIdealOf K n G O g ((CategoryTheory.ConcreteCategory.hom (โ†‘(CategoryTheory.CategoryStruct.comp ฯ† ((affine K n).ofRestrict G))).base) p))

        The pull-back of J along a K-morphism into (G, ๐’œ_G) landing in O.

        source
        theorem AnalyticSpace.traceIncl_base_mem (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' โ‰ค G) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : โˆ€ (p : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace), p โˆˆ O โ†” โ†‘p โˆˆ G') (p : โ†‘โ†‘(analyticSpaceOfOpen K n G').toPresheafedSpace) :
        (CategoryTheory.ConcreteCategory.hom (โ†‘(traceIncl K n G hG O hO)).base) p โˆˆ O
        source
        theorem AnalyticSpace.transportIdeal_restrictIdeal_eq_modelIdeal (K : Type) [RCLike K] (n : โ„•) (G : TopologicalSpace.Opens (Kn K n)) {G' : TopologicalSpace.Opens (Kn K n)} (hG : G' โ‰ค G) (O : TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hO : โˆ€ (p : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace), p โˆˆ O โ†” โ†‘p โˆˆ G') (J : Manifold.IdealSheaf (analyticSpaceOfOpen K n G).๐’ช) {l : โ„•} (g : Fin l โ†’ โ†‘((analyticSpaceOfOpen K n G).presheaf.obj (Opposite.op O))) (hg : โˆ€ (b : โ†‘โ†‘(analyticSpaceOfOpen K n G).toPresheafedSpace) (hb : b โˆˆ O), QuotientSpace.stalkIdeal (analyticSpaceOfOpen K n G).toLocallyRingedSpace J b = Ideal.span (Set.range fun (i : Fin l) => (CategoryTheory.ConcreteCategory.hom ((analyticSpaceOfOpen K n G).presheaf.germ O b hb)) (g i))) :
        KLocallyRingedSpace.transportIdeal (traceIso K n G hG O hO).symm ((analyticSpaceOfOpen K n G).restrictIdeal J O) = modelIdeal K n G' (generatorsOn K n G hG O hO g)

        A finite-type ideal sheaf on (G, ๐’œ_G), restricted to the trace open O of G' and transported along the trace isomorphism, is the model ideal of its local generators read on G'.

        source
        theorem AnalyticSpace.quotient_locallyModel {K : Type} [RCLike K] (X : AnalyticSpace K) (J : Manifold.IdealSheaf X.๐’ช) (y : โ†‘โ†‘(X.quotient J).toPresheafedSpace) :
        โˆƒ (U : TopologicalSpace.Opens โ†‘โ†‘(X.quotient J).toPresheafedSpace) (_ : y โˆˆ U) (n : โ„•) (k : โ„•) (G : TopologicalSpace.Opens (Kn K n)) (f : Fin k โ†’ AnalyticFun K n G) (W : TopologicalSpace.Opens โ†‘โ†‘(localModel K n G f).toPresheafedSpace), Nonempty (((X.quotient J).restrictOpen U).KIso ((localModel K n G f).restrictOpen W))

        The local-model clause for a closed subspace: every point of the quotient of X by a finite-type ideal sheaf has a neighbourhood K-isomorphic to (an open of) a local analytic K-space โ€” the model of X at the point, cut out further by the ambient lifts of local generators of the ideal sheaf.