Documentation

Hironaka.AnalyticSpace.Complexify

The complexification X(โ„‚) = (|X|, ๐’ช_X โŠ—_โ„ โ„‚) of a real-analytic space #

For a preanalytic โ„-space X = (X, ๐’ช_X), Hironaka defines X(โ„‚) as the โ„‚-local-ringed space (X, ๐’ช_X โŠ—_โ„ โ„‚) [Hir64, Ch. 0, ยง1, p. 120]. This file builds X(โ„‚) for every โ„-local-ringed space X whose residue fields are โ„ โ€” the property of the stalks of a (pre)analytic โ„-space that makes ๐’ช_{X,x} โŠ—_โ„ โ„‚ a local ring โ€” and complexifies โ„-morphisms (Hironaka's h_โ„‚).

Hironaka's complexifications (Y, f) of X, the analytic โ„‚-spaces receiving X(โ„‚) as a closed subspace, are defined in Hironaka/AnalyticSpace/Complexification.lean.

The functor A โ†ฆ A[i] and the presheaf ๐’ช_X โŠ—_โ„ โ„‚ #

source
def AnalyticSpace.complexifyFunctor :
CategoryTheory.Functor CommRingCat CommRingCat

The functor A โ†ฆ A โŠ—_โ„ โ„‚ = A[i] on commutative rings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AnalyticSpace.complexifyFunctor_obj (A : CommRingCat) :
    complexifyFunctor.obj A = โ†ง(Complexified โ†‘A)
    source
    @[simp]
    theorem AnalyticSpace.complexifyFunctor_map_apply {A B : CommRingCat} (f : A โŸถ B) (z : Complexified โ†‘A) :
    (CategoryTheory.ConcreteCategory.hom (complexifyFunctor.map f)) z = (Complexified.map (CommRingCat.Hom.hom f)) z
    source
    @[reducible, inline]
    abbrev AnalyticSpace.complexifyPresheaf {X : TopCat} (F : TopCat.Presheaf CommRingCat X) :
    TopCat.Presheaf CommRingCat X

    The presheaf ๐’ช_X โŠ—_โ„ โ„‚, U โ†ฆ ฮ“(U, ๐’ช_X)[i], of a presheaf of rings ๐’ช_X.

    Equations
    Instances For
      source
      theorem AnalyticSpace.complexifyPresheaf_obj {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
      (complexifyPresheaf F).obj U = โ†ง(Complexified โ†‘(F.obj U))
      source
      theorem AnalyticSpace.complexifyPresheaf_map_apply {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U V : (TopologicalSpace.Opens โ†‘X)แต’แต–} (i : U โŸถ V) (z : Complexified โ†‘(F.obj U)) :
      (CategoryTheory.ConcreteCategory.hom ((complexifyPresheaf F).map i)) z = (Complexified.map (CommRingCat.Hom.hom (F.map i))) z
      source
      theorem AnalyticSpace.isSheaf_complexifyPresheaf {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (hF : F.IsSheaf) :
      (complexifyPresheaf F).IsSheaf

      The presheaf U โ†ฆ ฮ“(U, ๐’ช_X)[i] of a sheaf of rings is a sheaf: a compatible family of pairs (a_j + b_j i) glues uniquely because the families (a_j) and (b_j) do.

      Stalks: (๐’ช_X โŠ—_โ„ โ„‚)_x = ๐’ช_{X,x}[i] #

      source
      noncomputable def AnalyticSpace.stalkToComplexified {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
      (complexifyPresheaf F).stalk x โŸถ complexifyFunctor.obj (F.stalk x)

      The canonical map from the stalk of ๐’ช_X[i] to ๐’ช_{X,x}[i]: the germ of a + b i goes to (germ a) + (germ b) i.

      Equations
      Instances For
        source
        theorem AnalyticSpace.stalkToComplexified_germ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) (U : TopologicalSpace.Opens โ†‘X) (hx : x โˆˆ U) (z : โ†‘((complexifyPresheaf F).obj (Opposite.op U))) :
        (CategoryTheory.ConcreteCategory.hom (stalkToComplexified F x)) ((CategoryTheory.ConcreteCategory.hom ((complexifyPresheaf F).germ U x hx)) z) = (Complexified.map (CommRingCat.Hom.hom (F.germ U x hx))) z
        source
        theorem AnalyticSpace.stalkToComplexified_surjective {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
        Function.Surjective โ‡‘(CommRingCat.Hom.hom (stalkToComplexified F x))
        source
        theorem AnalyticSpace.stalkToComplexified_injective {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
        Function.Injective โ‡‘(CommRingCat.Hom.hom (stalkToComplexified F x))
        source
        theorem AnalyticSpace.stalkToComplexified_bijective {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
        Function.Bijective โ‡‘(CommRingCat.Hom.hom (stalkToComplexified F x))
        source
        noncomputable def AnalyticSpace.stalkComplexifyEquiv {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
        โ†‘((complexifyPresheaf F).stalk x) โ‰ƒ+* Complexified โ†‘(F.stalk x)

        The stalk of ๐’ช_X โŠ—_โ„ โ„‚ at x is ๐’ช_{X,x} โŠ—_โ„ โ„‚ = ๐’ช_{X,x}[i].

        Equations
        Instances For
          source
          theorem AnalyticSpace.stalkComplexifyEquiv_germ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) (U : TopologicalSpace.Opens โ†‘X) (hx : x โˆˆ U) (z : โ†‘((complexifyPresheaf F).obj (Opposite.op U))) :
          (stalkComplexifyEquiv F x) ((CategoryTheory.ConcreteCategory.hom ((complexifyPresheaf F).germ U x hx)) z) = (Complexified.map (CommRingCat.Hom.hom (F.germ U x hx))) z
          source
          theorem AnalyticSpace.stalkToComplexified_germ' {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) (U : TopologicalSpace.Opens โ†‘X) (hx : x โˆˆ U) (z : โ†‘((complexifyPresheaf F).obj (Opposite.op U))) :
          (CommRingCat.Hom.hom (stalkToComplexified F x)) ((CommRingCat.Hom.hom ((complexifyPresheaf F).germ U x hx)) z) = (Complexified.map (CommRingCat.Hom.hom (F.germ U x hx))) z
          source
          instance AnalyticSpace.isIso_stalkToComplexified {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (x : โ†‘X) :
          CategoryTheory.IsIso (stalkToComplexified F x)

          Real residue fields #

          source
          class AnalyticSpace.KLocallyRingedSpace.HasRealResidueFields (X : KLocallyRingedSpace โ„) :
          Prop

          An โ„-local-ringed space has real residue fields when every element of every stalk is congruent modulo the maximal ideal to a constant โ€” the property of the stalks of a preanalytic โ„-space (quotients of โ„{z}) that makes ๐’ช_{X,x} โŠ—_โ„ โ„‚ a local ring [Hir64, Ch. 0, ยง1, p. 120].

          Instances
            source
            theorem AnalyticSpace.KLocallyRingedSpace.constAt_eq_germ (X : KLocallyRingedSpace โ„) (x : โ†‘โ†‘X.toPresheafedSpace) (c : โ„) :
            (X.constAt x) c = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ โŠค x trivial)) (X.algebraMap c)
            source
            theorem AnalyticSpace.KLocallyRingedSpace.exists_sub_constAt_mem_of_hom {X Y : KLocallyRingedSpace โ„} (f : X โŸถ Y) (x : โ†‘โ†‘X.toPresheafedSpace) (hX : โˆ€ (s : โ†‘(X.presheaf.stalk x)), โˆƒ (c : โ„), s - (X.constAt x) c โˆˆ IsLocalRing.maximalIdeal โ†‘(X.presheaf.stalk x)) (t : โ†‘(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x))) :
            โˆƒ (c : โ„), t - (Y.constAt ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x)) c โˆˆ IsLocalRing.maximalIdeal โ†‘(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x))

            The residue-field property passes from the source of an โ„-morphism with surjective base map to its target: the residue field of ๐’ช_{Y,f x} embeds into that of ๐’ช_{X,x} through the local homomorphism f_x^โ™ฏ, which carries constants to constants.

            source
            theorem AnalyticSpace.KLocallyRingedSpace.exists_sub_constAt_mem_of_surjective {X Y : KLocallyRingedSpace โ„} (f : X โŸถ Y) (x : โ†‘โ†‘X.toPresheafedSpace) (hf : Function.Surjective โ‡‘(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘f) x))) (hY : โˆ€ (t : โ†‘(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x))), โˆƒ (c : โ„), t - (Y.constAt ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x)) c โˆˆ IsLocalRing.maximalIdeal โ†‘(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x))) (s : โ†‘(X.presheaf.stalk x)) :
            โˆƒ (c : โ„), s - (X.constAt x) c โˆˆ IsLocalRing.maximalIdeal โ†‘(X.presheaf.stalk x)

            The residue-field property passes from the target of an โ„-morphism with surjective stalk map to its source.

            source
            theorem AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_of_hom_surjective {X Y : KLocallyRingedSpace โ„} (f : X โŸถ Y) (hf : โˆ€ (x : โ†‘X.toTopCat), Function.Surjective โ‡‘(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘f) x))) [Y.HasRealResidueFields] :
            X.HasRealResidueFields
            source
            theorem AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_of_hom_surjective_base {X Y : KLocallyRingedSpace โ„} (f : X โŸถ Y) (hf : Function.Surjective โ‡‘(CategoryTheory.ConcreteCategory.hom (โ†‘f).base)) [X.HasRealResidueFields] :
            Y.HasRealResidueFields
            source
            theorem AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_of_kIso {A B : KLocallyRingedSpace โ„} (e : A.KIso B) [B.HasRealResidueFields] :
            A.HasRealResidueFields

            Transport along a K-isomorphism.

            source
            instance AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_restrictOpen (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (U : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace) :
            (X.restrictOpen U).HasRealResidueFields

            The open subspace X | U of a space with real residue fields has real residue fields (the stalk maps of the open immersion are isomorphisms).

            source
            instance AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_quotient (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (J : Manifold.IdealSheaf X.๐’ช) :
            (X.quotient J).HasRealResidueFields

            The quotient by an ideal sheaf of a space with real residue fields has real residue fields (the stalk maps of the canonical morphism are the quotient maps, surjective).

            source
            theorem AnalyticSpace.KLocallyRingedSpace.exists_sub_constAt_mem_affine (n : โ„•) (q : Kn โ„ n) (s : โ†‘((affine โ„ n).presheaf.stalk q)) :
            โˆƒ (c : โ„), s - ((affine โ„ n).constAt q) c โˆˆ IsLocalRing.maximalIdeal โ†‘((affine โ„ n).presheaf.stalk q)

            A germ of ๐’œ_{โ„โฟ} is congruent modulo the maximal ideal to its value.

            source
            instance AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_affine (n : โ„•) :
            (affine โ„ n).HasRealResidueFields

            (โ„โฟ, ๐’œ_{โ„โฟ}) has real residue fields: a germ is congruent to its value.

            source
            instance AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_analyticSpaceOfOpen (n : โ„•) (G : TopologicalSpace.Opens (Kn โ„ n)) :
            (analyticSpaceOfOpen โ„ n G).HasRealResidueFields
            source
            instance AnalyticSpace.KLocallyRingedSpace.hasRealResidueFields_localModel (n : โ„•) (G : TopologicalSpace.Opens (Kn โ„ n)) {k : โ„•} (f : Fin k โ†’ AnalyticFun โ„ n G) :
            (localModel โ„ n G f).HasRealResidueFields
            source
            instance AnalyticSpace.hasRealResidueFields (X : AnalyticSpace โ„) :
            X.HasRealResidueFields

            Every analytic โ„-space has real residue fields: near every point it is โ„-isomorphic to a local model, whose stalks are quotients of ๐’œ_{โ„โฟ,q}.

            The complexification X(โ„‚) #

            source
            theorem AnalyticSpace.KLocallyRingedSpace.isLocalRing_stalk_complexified (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (x : โ†‘โ†‘X.toPresheafedSpace) :
            IsLocalRing (Complexified โ†‘(X.presheaf.stalk x))
            source
            theorem AnalyticSpace.KLocallyRingedSpace.isLocalRing_stalk_complexifyPresheaf (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (x : โ†‘โ†‘X.toPresheafedSpace) :
            IsLocalRing โ†‘((complexifyPresheaf X.presheaf).stalk x)
            source
            @[implicit_reducible]
            def AnalyticSpace.KLocallyRingedSpace.complexify (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] :
            KLocallyRingedSpace โ„‚

            The complexification X(โ„‚) = (|X|, ๐’ช_X โŠ—_โ„ โ„‚) of an โ„-local-ringed space with real residue fields [Hir64, Ch. 0, ยง1, p. 120], a โ„‚-local-ringed space; the โ„‚-structure sends c to Re c + Im c ยท i on the constants of X.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem AnalyticSpace.KLocallyRingedSpace.complexify_presheaf_obj (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (U : (TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace)แต’แต–) :
              X.complexify.presheaf.obj U = โ†ง(Complexified โ†‘(X.presheaf.obj U))
              source
              theorem AnalyticSpace.KLocallyRingedSpace.complexify_algebraMap (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (c : โ„‚) :
              X.complexify.algebraMap c = (Complexified.algebraMapComplex X.algebraMap) c
              source
              noncomputable def AnalyticSpace.KLocallyRingedSpace.complexifyStalkEquiv (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (x : โ†‘โ†‘X.toPresheafedSpace) :
              โ†‘(X.complexify.presheaf.stalk x) โ‰ƒ+* Complexified โ†‘(X.presheaf.stalk x)

              The stalk of X(โ„‚) at x is ๐’ช_{X,x} โŠ—_โ„ โ„‚.

              Equations
              Instances For

                Functoriality: Hironaka's h_โ„‚ #

                source
                def AnalyticSpace.KLocallyRingedSpace.complexifyHomAux {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) :
                X.complexify.toPresheafedSpace โŸถ Y.complexify.toPresheafedSpace

                The complexified sheaf map of a morphism, as a morphism of presheafed spaces.

                Equations
                Instances For
                  source
                  theorem AnalyticSpace.KLocallyRingedSpace.complexifyHomAux_c_app {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) (U : (TopologicalSpace.Opens โ†‘โ†‘Y.toPresheafedSpace)แต’แต–) (z : Complexified โ†‘(Y.presheaf.obj U)) :
                  (CategoryTheory.ConcreteCategory.hom ((complexifyHomAux f).c.app U)) z = (Complexified.map (CommRingCat.Hom.hom ((โ†‘f).c.app U))) z
                  source
                  theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_complexifyHomAux {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) (x : โ†‘โ†‘X.toPresheafedSpace) :
                  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (complexifyHomAux f) x) (stalkToComplexified X.presheaf x) = CategoryTheory.CategoryStruct.comp (stalkToComplexified Y.presheaf ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x)) (complexifyFunctor.map (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘f) x))

                  The stalk map of the complexified morphism is the complexified stalk map, through the identifications of the stalks.

                  source
                  theorem AnalyticSpace.KLocallyRingedSpace.isLocalHom_stalkMap_complexifyHomAux {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) (x : โ†‘โ†‘X.toPresheafedSpace) :
                  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (complexifyHomAux f) x))
                  source
                  def AnalyticSpace.KLocallyRingedSpace.complexifyHom {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) :
                  X.complexify โŸถ Y.complexify

                  The โ„‚-morphism h_โ„‚ : X(โ„‚) โŸถ Y(โ„‚) induced by an โ„-morphism h : X โŸถ Y [Hir64, Ch. 0, ยง1, p. 120]: the same base map, the complexified sheaf map.

                  Equations
                  Instances For
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.complexifyHom_val {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) :
                    (โ†‘(complexifyHom f)).toHom = complexifyHomAux f
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.complexifyHom_base {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) :
                    (โ†‘(complexifyHom f)).base = (โ†‘f).base
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.toFun_complexifyHom {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) :
                    Hom.toFun (complexifyHom f) = Hom.toFun f
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.complexifyHom_id {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] :
                    complexifyHom (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.complexify
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.complexifyHom_comp {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] {Z : KLocallyRingedSpace โ„} [Z.HasRealResidueFields] (f : X โŸถ Y) (g : Y โŸถ Z) :
                    complexifyHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (complexifyHom f) (complexifyHom g)
                    source
                    theorem AnalyticSpace.KLocallyRingedSpace.complexifyStalkEquiv_stalkMap_complexifyHom {X : KLocallyRingedSpace โ„} [X.HasRealResidueFields] {Y : KLocallyRingedSpace โ„} [Y.HasRealResidueFields] (f : X โŸถ Y) (x : โ†‘โ†‘X.toPresheafedSpace) (t : โ†‘(Y.complexify.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x))) :
                    (X.complexifyStalkEquiv x) ((CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘(complexifyHom f)) x)) t) = (Complexified.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (โ†‘f) x))) ((Y.complexifyStalkEquiv ((CategoryTheory.ConcreteCategory.hom (โ†‘f).base) x)) t)

                    The stalk map of h_โ„‚ at x is the complexified stalk map of h, through the stalk identifications.

                    Complexification commutes with open subspaces #

                    source
                    noncomputable def AnalyticSpace.KLocallyRingedSpace.complexifyRestrictIso (X : KLocallyRingedSpace โ„) [X.HasRealResidueFields] (U : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace) :
                    (X.restrictOpen U).complexify โ‰… X.complexify.restrictOpen U

                    X(โ„‚) | U = (X | U)(โ„‚): the two โ„‚-local-ringed spaces have the same carrier and structure sheaf; only the โ„‚-structures differ syntactically, and they agree.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For