Documentation

Mathlib.AlgebraicGeometry.OpenImmersion

Open immersions of schemes #

@[reducible, inline]

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

Equations
Instances For

    To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

    Equations
    Instances For
      @[deprecated AlgebraicGeometry.IsOpenImmersion.isOpen_range]

      Alias of AlgebraicGeometry.IsOpenImmersion.isOpen_range.

      The image of an open immersion as an open set.

      Equations
      • f.opensRange = { carrier := Set.range f.val.base, is_open' := }
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For

          Pretty printer defined by notation3 command.

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

            f ''ᵁ U is notation for the image (as an open set) of U under an open immersion f.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem AlgebraicGeometry.Scheme.Hom.image_le_image_of_le {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} {V : X.Opens} (e : U V) :
              f.opensFunctor.obj U f.opensFunctor.obj V
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) :
              (TopologicalSpace.Opens.map f.val.base).obj (f.opensFunctor.obj U) = U
              def AlgebraicGeometry.Scheme.Hom.appIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) :
              Y.presheaf.obj (Opposite.op (f.opensFunctor.obj U)) X.presheaf.obj (Opposite.op U)

              The isomorphism Γ(Y, f(U)) ≅ Γ(X, U) induced by an open immersion f : X ⟶ Y.

              Equations
              Instances For
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} {V : X.Opens} (i : Opposite.op U Opposite.op V) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj V)) Z) :
                CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (CategoryTheory.CategoryStruct.comp (f.appIso V).inv h) = CategoryTheory.CategoryStruct.comp (f.appIso U).inv (CategoryTheory.CategoryStruct.comp (Y.presheaf.map (f.opensFunctor.op.map i)) h)
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} {V : X.Opens} (i : Opposite.op U Opposite.op V) :
                CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (f.appIso V).inv = CategoryTheory.CategoryStruct.comp (f.appIso U).inv (Y.presheaf.map (f.opensFunctor.op.map i))
                theorem AlgebraicGeometry.Scheme.Hom.appIso_hom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) :
                (f.appIso U).hom = CategoryTheory.CategoryStruct.comp (f.app (f.opensFunctor.obj U)) (X.presheaf.map (CategoryTheory.eqToHom ).op)
                theorem AlgebraicGeometry.Scheme.Hom.appIso_hom' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) :
                (f.appIso U).hom = f.appLE (f.opensFunctor.obj U) U
                @[simp]
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (hU : U f.opensRange) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.val.base).obj U))) Z) :
                theorem AlgebraicGeometry.Scheme.Hom.app_invApp' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens) (hU : U f.opensRange) :
                CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((TopologicalSpace.Opens.map f.val.base).obj U)).inv = Y.presheaf.map (CategoryTheory.eqToHom ).op

                A variant of app_invApp that gives an eqToHom instead of homOfLE.

                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.val.base).obj (f.opensFunctor.obj U))) Z) :
                CategoryTheory.CategoryStruct.comp (f.appIso U).inv (CategoryTheory.CategoryStruct.comp (f.app (f.opensFunctor.obj U)) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ).op) h
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) (x : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (Opposite.op U))) :
                (f.app (f.opensFunctor.obj U)) ((f.appIso U).inv x) = (X.presheaf.map (CategoryTheory.eqToHom )) x
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) :
                CategoryTheory.CategoryStruct.comp (f.appIso U).inv (f.app (f.opensFunctor.obj U)) = X.presheaf.map (CategoryTheory.eqToHom ).op

                The open sets of an open subscheme corresponds to the open sets containing in the image.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset {X : AlgebraicGeometry.Scheme} {x : X.toPresheafedSpace} {U : X.Opens} (hxU : x U) :
                  ∃ (R : CommRingCat) (f : AlgebraicGeometry.Spec R X), AlgebraicGeometry.IsOpenImmersion f x Set.range f.val.base Set.range f.val.base U

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

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

                    The restriction of a Scheme along an open embedding.

                    Equations
                    Instances For
                      theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                      (X.restrict h).toPresheafedSpace = X.restrict h
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.ofRestrict_val_base {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                      (X.ofRestrict h).val.base = f
                      theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
                      (X.ofRestrict h).val.c.app V = X.presheaf.map (.adjunction.counit.app (Opposite.unop V)).op
                      def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                      X.restrict h X

                      The canonical map from the restriction to the subspace.

                      Equations
                      • X.ofRestrict h = X.ofRestrict h
                      Instances For
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.ofRestrict_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (V : X.Opens) :
                        AlgebraicGeometry.Scheme.Hom.app (X.ofRestrict h) V = X.presheaf.map (.adjunction.counit.app V).op
                        instance AlgebraicGeometry.IsOpenImmersion.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                        Equations
                        • =
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.ofRestrict_appLE {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (V : X.Opens) (W : (X.restrict h).Opens) (e : W (TopologicalSpace.Opens.map (X.ofRestrict h).val.base).obj V) :
                        AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ).op
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.ofRestrict_appIso {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U✝ TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (U : (X.restrict h).Opens) :
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (V : (TopologicalSpace.Opens (X.restrict h).toPresheafedSpace)ᵒᵖ) (W : (TopologicalSpace.Opens (X.restrict h).toPresheafedSpace)ᵒᵖ) (i : V W) :
                        (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ).op

                        An open immersion induces an isomorphism from the domain onto the image

                        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
                          Instances For

                            Two open immersions with equal range are isomorphic.

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

                              If f is an open immersion X ⟶ Y, the global sections of X are naturally isomorphic to the sections of Y over the image of f.

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

                                Given an open immersion f : U ⟶ X, the isomorphism between global sections of U and the sections of X at the image of f.

                                Equations
                                Instances For