Documentation

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

The category of locally ringed spaces #

We define (bundled) locally ringed spaces (as SheafedSpace CommRing along with the fact that the stalks are local rings), and morphisms between these (morphisms in SheafedSpace with is_local_ring_hom on the stalk maps).

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

  • carrier : TopCat
  • presheaf : TopCat.Presheaf CommRingCat self.toPresheafedSpace
  • IsSheaf : self.presheaf.IsSheaf
  • localRing : ∀ (x : self.toPresheafedSpace), LocalRing (self.presheaf.stalk x)

    Stalks of a locally ringed space are local rings.

Instances For
    theorem AlgebraicGeometry.LocallyRingedSpace.localRing (self : AlgebraicGeometry.LocallyRingedSpace) (x : self.toPresheafedSpace) :
    LocalRing (self.presheaf.stalk x)

    Stalks of a locally ringed space are local rings.

    An alias for to_SheafedSpace, where the result type is a RingedSpace. This allows us to use dot-notation for the RingedSpace namespace.

    Equations
    • X.toRingedSpace = X.toSheafedSpace
    Instances For

      The underlying topological space of a locally ringed space.

      Equations
      • X.toTopCat = X.toPresheafedSpace
      Instances For

        The structure sheaf of a locally ringed space.

        Equations
        • X.𝒪 = X.sheaf
        Instances For

          A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

          Instances For

            the underlying morphism induces a local ring homomorphism on stalks

            The stalk of a locally ringed space, just as a CommRing.

            Equations
            • X.stalk x = X.presheaf.stalk x
            Instances For
              Equations
              • =
              noncomputable def AlgebraicGeometry.LocallyRingedSpace.stalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X Y) (x : X.toTopCat) :
              Y.stalk (f.val.base x) X.stalk x

              A morphism of locally ringed spaces f : X ⟶ Y induces a local ring homomorphism from Y.stalk (f x) to X.stalk x for any x : X.

              Equations
              Instances For

                The identity morphism on a locally ringed space.

                Equations
                Instances For
                  Equations
                  • X.instInhabitedHom = { default := X.id }

                  Composition of morphisms of locally ringed spaces.

                  Equations
                  Instances For

                    The category of locally ringed spaces.

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

                    The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

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

                      Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to a morphism X ⟶ Y as locally ringed spaces.

                      See also iso_of_SheafedSpace_iso.

                      Equations
                      Instances For

                        Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to an isomorphism X ⟶ Y as locally ringed spaces.

                        This is related to the property that the functor forget_to_SheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem AlgebraicGeometry.LocallyRingedSpace.restrict_carrier {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U X.toTopCat} (h : OpenEmbedding f) :
                          (X.restrict h).toPresheafedSpace = U
                          @[simp]
                          theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U X✝.toTopCat} (h : OpenEmbedding f) (X : (TopologicalSpace.Opens U)ᵒᵖ) :
                          (X✝.restrict h).presheaf.obj X = X✝.presheaf.obj (Opposite.op (.functor.obj (Opposite.unop X)))
                          @[simp]
                          theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U X.toTopCat} (h : OpenEmbedding f) :
                          ∀ {X_1 Y : (TopologicalSpace.Opens U)ᵒᵖ} (f_1 : X_1 Y), (X.restrict h).presheaf.map f_1 = X.presheaf.map (.functor.map f_1.unop).op

                          The restriction of a locally ringed space along an open embedding.

                          Equations
                          • X.restrict h = { toSheafedSpace := X.restrict h, localRing := }
                          Instances For

                            The canonical map from the restriction to the subspace.

                            Equations
                            • X.ofRestrict h = { val := X.ofRestrict h, prop := }
                            Instances For

                              The restriction of a locally ringed space X to the top subspace is isomorphic to X itself.

                              Equations
                              Instances For

                                The empty locally ringed space.

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

                                  The canonical map from the empty locally ringed space.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • AlgebraicGeometry.LocallyRingedSpace.instUniqueHomEmptyCollection = { default := X.emptyTo, uniq := }
                                    theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X Y) {U : TopologicalSpace.Opens Y.toTopCat} (s : (Y.presheaf.obj (Opposite.op U))) :
                                    (TopologicalSpace.Opens.map f.val.base).obj (Y.toRingedSpace.basicOpen s) = X.toRingedSpace.basicOpen ((f.val.c.app (Opposite.op U)) s)
                                    @[simp]
                                    theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens X.toPresheafedSpace) (f : (X.presheaf.obj (Opposite.op U))) (hf : IsNilpotent f) :
                                    X.toRingedSpace.basicOpen f =
                                    Equations
                                    • =