Documentation

Mathlib.Geometry.RingedSpace.OpenImmersion

Open immersions of structured spaces #

We say that a morphism of presheafed spaces f : X ⟶ Y is an open immersion if the underlying map of spaces is an open embedding f : X ⟶ U ⊆ Y, and the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Abbreviations are also provided for SheafedSpace, LocallyRingedSpace and Scheme.

Main definitions #

Main results #

An open immersion of PresheafedSpaces is an open embedding f : X ⟶ U ⊆ Y of the underlying spaces, such that the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Instances

    the underlying continuous map of underlying spaces from the source to an open subset of the target.

    the underlying sheaf morphism is an isomorphism on each open subset

    @[reducible, inline]

    A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism of PresheafedSpaces

    Equations
    Instances For
      @[reducible, inline]

      A morphism of LocallyRingedSpaces is an open immersion if it is an open immersion as a morphism of SheafedSpaces

      Equations
      Instances For

        An open immersion f : X ⟶ Y induces an isomorphism X ≅ Y|_{f(X)}.

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

          For an open immersion f : X ⟶ Y and an open set U ⊆ X, we have the map X(U) ⟶ Y(U).

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

            (Implementation.) The projection map when constructing the pullback along an open immersion.

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

              We construct the pullback along an open immersion via restricting along the pullback of the maps of underlying spaces (which is also an open embedding).

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

                (Implementation.) Any cone over cospan f g indeed factors through the constructed cone.

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

                  The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

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

                    Two open immersions with equal range is isomorphic.

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

                      If X ⟶ Y is an open immersion, and Y is a SheafedSpace, then so is X.

                      Equations
                      Instances For

                        If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a SheafedSpace, we can upgrade it into a morphism of SheafedSpaces.

                        Equations
                        Instances For

                          If X ⟶ Y is an open immersion, and Y is a LocallyRingedSpace, then so is X.

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

                            If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a LocallyRingedSpace, we can upgrade it into a morphism of LocallyRingedSpace.

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

                              Suppose X Y : SheafedSpace C, where C is a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then a morphism X ⟶ Y that is a topological open embedding is an open immersion iff every stalk map is an iso.

                              @[reducible, inline]

                              The functor Opens X ⥤ Opens Y associated with an open immersion f : X ⟶ Y.

                              Equations
                              Instances For
                                theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat} {f : Y TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (U : TopologicalSpace.Opens (X.restrict h).toPresheafedSpace) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj ((X.restrict h).presheaf.obj (Opposite.op U))) :
                                @[simp]
                                theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat} {f : Y TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (U : TopologicalSpace.Opens (X.restrict h).toPresheafedSpace) :
                                theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) (j : CategoryTheory.Discrete ι) (h : i j) (U : TopologicalSpace.Opens (F.obj i).toPresheafedSpace) :
                                (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι (F.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace) j).base).obj ((TopologicalSpace.Opens.map (CategoryTheory.preservesColimitIso AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace F).inv.base).obj (.functor.obj U)) =

                                An explicit pullback cone over cospan f g if f is an open immersion.

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

                                  The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

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

                                    An open immersion is isomorphic to the induced open subscheme on its image.

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

                                      Suppose X Y : SheafedSpace C, where C is a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then a morphism X ⟶ Y that is a topological open embedding is an open immersion iff every stalk map is an iso.

                                      theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (U : TopologicalSpace.Opens (X.restrict h).toPresheafedSpace) (x : (CategoryTheory.forget CommRingCat).obj ((X.restrict h).presheaf.obj (Opposite.op U))) :
                                      @[simp]