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.Scheme.Hom.isOpenEmbedding (since := "2024-10-18")]

      Alias of AlgebraicGeometry.Scheme.Hom.isOpenEmbedding.

      def AlgebraicGeometry.Scheme.Hom.opensRange {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] :
      Y.Opens

      The image of an open immersion as an open set.

      Equations
      • f.opensRange = { carrier := Set.range f.base, is_open' := }
      Instances For
        @[simp]
        theorem AlgebraicGeometry.Scheme.Hom.coe_opensRange {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] :
        f.opensRange = Set.range f.base
        @[reducible, inline]
        abbrev AlgebraicGeometry.Scheme.Hom.opensFunctor {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] :
        CategoryTheory.Functor X.Opens Y.Opens

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

        Equations
        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

            Pretty printer defined by notation3 command.

            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 Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {U V : X.Opens} (e : U V) :
              f.opensFunctor.obj U f.opensFunctor.obj V
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {U V : X.Opens} (e : U V) :
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] :
              f.opensFunctor.obj = f.opensRange
              @[simp]
              theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) :
              (TopologicalSpace.Opens.map f.base).obj (f.opensFunctor.obj U) = U
              theorem AlgebraicGeometry.Scheme.Hom.image_le_image_iff {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U U' : X.Opens) :
              (opensFunctor f).obj U (opensFunctor f).obj U' U U'
              theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) :
              f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U) = f.opensRange U
              theorem AlgebraicGeometry.Scheme.Hom.image_injective {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] :
              Function.Injective fun (x : X.Opens) => f.opensFunctor.obj x
              theorem AlgebraicGeometry.Scheme.Hom.image_iSup {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {ι : Sort u_1} (s : ιX.Opens) :
              f.opensFunctor.obj (⨆ (i : ι), s i) = ⨆ (i : ι), f.opensFunctor.obj (s i)
              theorem AlgebraicGeometry.Scheme.Hom.image_iSup₂ {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {ι : Sort u_1} {κ : ιSort u_2} (s : (i : ι) → κ iX.Opens) :
              f.opensFunctor.obj (⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), f.opensFunctor.obj (s i j)
              def AlgebraicGeometry.Scheme.Hom.appIso {X Y : Scheme} (f : X.Hom Y) [H : 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 {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {U 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))
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {U 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)
                theorem AlgebraicGeometry.Scheme.Hom.appIso_hom {X Y : Scheme} (f : X.Hom Y) [H : 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 Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) :
                (f.appIso U).hom = f.appLE (f.opensFunctor.obj U) U
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) :
                CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.homOfLE ).op
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) Z) :
                theorem AlgebraicGeometry.Scheme.Hom.app_invApp' {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U f.opensRange) :
                CategoryTheory.CategoryStruct.comp (f.app U) (f.appIso ((TopologicalSpace.Opens.map f.base).obj U)).inv = Y.presheaf.map (CategoryTheory.eqToHom ).op

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

                theorem AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : Y.Opens) (hU : U f.opensRange) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (f.opensFunctor.obj ((TopologicalSpace.Opens.map f.base).obj U))) Z) :
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) :
                CategoryTheory.CategoryStruct.comp (f.appIso U).inv (f.app (f.opensFunctor.obj U)) = X.presheaf.map (CategoryTheory.eqToHom ).op
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.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
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply {X Y : Scheme} (f : X.Hom Y) [H : 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 ).op) x
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply' {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) (x : (X.presheaf.obj (Opposite.op U))) :
                (f.app (f.opensFunctor.obj U)).hom ((f.appIso U).inv.hom x) = (X.presheaf.map (CategoryTheory.eqToHom ).op).hom x

                elementwise generates the HasForget.instFunLike lemma, we want CommRingCat.Hom.hom.

                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv {X Y : Scheme} (f : X Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.base).obj U) :
                CategoryTheory.CategoryStruct.comp (appLE f U V e) (appIso f V).inv = Y.presheaf.map (CategoryTheory.homOfLE ).op
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc {X Y : Scheme} (f : X Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.base).obj U) {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op ((opensFunctor f).obj V)) Z) :
                theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply {X Y : Scheme} (f : X Y) [IsOpenImmersion f] {U : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.base).obj U) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) :
                (appIso f V).inv ((appLE f U V e) x) = (Y.presheaf.map (CategoryTheory.homOfLE ).op) x
                @[simp]
                theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE {X Y : Scheme} (f : X Y) [IsOpenImmersion f] {U V : X.Opens} (e : V (TopologicalSpace.Opens.map f.base).obj ((opensFunctor f).obj U)) :
                CategoryTheory.CategoryStruct.comp (appIso f U).inv (appLE f ((opensFunctor f).obj U) V e) = X.presheaf.map (CategoryTheory.homOfLE ).op
                @[simp]
                def AlgebraicGeometry.IsOpenImmersion.opensEquiv {X Y : Scheme} (f : X Y) [IsOpenImmersion f] :
                X.Opens { U : Y.Opens // U Scheme.Hom.opensRange f }

                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
                  @[simp]
                  theorem AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U : { U : Y.Opens // U Scheme.Hom.opensRange f }) :
                  (opensEquiv f).symm U = (TopologicalSpace.Opens.map f.base).obj U
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset {X : Scheme} {x : X.toPresheafedSpace} {U : X.Opens} (hxU : x U) :
                  ∃ (R : CommRingCat) (f : Spec R X), IsOpenImmersion f x Set.range f.base Set.range f.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
                    @[simp]
                    theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace {X : PresheafedSpace CommRingCat} (Y : Scheme) (f : X Y.toPresheafedSpace) [H : IsOpenImmersion f] :
                    (toScheme Y f).toLocallyRingedSpace = toLocallyRingedSpace Y.toLocallyRingedSpace f

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

                    Equations
                    Instances For
                      theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq {X Y : Scheme} (H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace) :
                      X = Y
                      def AlgebraicGeometry.Scheme.restrict {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :

                      The restriction of a Scheme along an open embedding.

                      Equations
                      • X.restrict h = { toPresheafedSpace := X.restrict h, IsSheaf := , isLocalRing := , local_affine := }
                      Instances For
                        theorem AlgebraicGeometry.Scheme.restrict_carrier {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                        (X.restrict h).toPresheafedSpace = U
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.restrict_presheaf_obj {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (X✝ : (TopologicalSpace.Opens U)ᵒᵖ) :
                        (X.restrict h).presheaf.obj X✝ = X.presheaf.obj (Opposite.op (.functor.obj (Opposite.unop X✝)))
                        theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                        (X.restrict h).toPresheafedSpace = X.restrict h
                        def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                        X.restrict h X

                        The canonical map from the restriction to the subspace.

                        Equations
                        • X.ofRestrict h = { toHom_1 := X.ofRestrict h }
                        Instances For
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                          (Hom.toLRSHom (X.ofRestrict h)).base = f
                          theorem AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
                          (Hom.toLRSHom (X.ofRestrict h)).c.app V = X.presheaf.map (.adjunction.counit.app (Opposite.unop V)).op
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.ofRestrict_app {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (V : X.Opens) :
                          Hom.app (X.ofRestrict h) V = X.presheaf.map (.adjunction.counit.app V).op
                          instance AlgebraicGeometry.IsOpenImmersion.ofRestrict {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                          IsOpenImmersion (X.ofRestrict h)
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.ofRestrict_appLE {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (V : X.Opens) (W : (X.restrict h).Opens) (e : W (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V) :
                          Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ).op
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.ofRestrict_appIso {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (U✝ : (X.restrict h).Opens) :
                          Hom.appIso (X.ofRestrict h) U✝ = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((Hom.opensFunctor (X.ofRestrict h)).obj U✝)))
                          @[simp]
                          theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (V W : (TopologicalSpace.Opens (X.restrict h).toPresheafedSpace)ᵒᵖ) (i : V W) :
                          (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ).op
                          theorem AlgebraicGeometry.IsOpenImmersion.of_stalk_iso {X Y : Scheme} (f : X Y) (hf : Topology.IsOpenEmbedding f.base) [∀ (x : X.toPresheafedSpace), CategoryTheory.IsIso (Scheme.Hom.stalkMap f x)] :
                          instance AlgebraicGeometry.IsOpenImmersion.stalk_iso {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (x : X.toPresheafedSpace) :
                          def AlgebraicGeometry.IsOpenImmersion.isoRestrict {X Z : Scheme} (f : X Z) [H : IsOpenImmersion f] :
                          X Z.restrict

                          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
                            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.
                            theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right {X Y Z : Scheme} (f : X Z) (g : Y Z) [H : IsOpenImmersion f] :
                            Set.range (CategoryTheory.Limits.pullback.fst g f).base = ((TopologicalSpace.Opens.map g.base).obj { carrier := Set.range f.base, is_open' := }).carrier
                            def AlgebraicGeometry.IsOpenImmersion.lift {X Y Z : Scheme} (f : X Z) (g : Y Z) [H : IsOpenImmersion f] (H' : Set.range g.base Set.range f.base) :
                            Y X

                            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
                              @[simp]
                              theorem AlgebraicGeometry.IsOpenImmersion.lift_fac {X Y Z : Scheme} (f : X Z) (g : Y Z) [H : IsOpenImmersion f] (H' : Set.range g.base Set.range f.base) :
                              theorem AlgebraicGeometry.IsOpenImmersion.lift_uniq {X Y Z : Scheme} (f : X Z) (g : Y Z) [H : IsOpenImmersion f] (H' : Set.range g.base Set.range f.base) (l : Y X) (hl : CategoryTheory.CategoryStruct.comp l f = g) :
                              l = lift f g H'
                              def AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq {X Y Z : Scheme} (f : X Z) (g : Y Z) [H : IsOpenImmersion f] [IsOpenImmersion g] (e : Set.range f.base = Set.range g.base) :
                              X Y

                              Two open immersions with equal range are isomorphic.

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

                                The fg argument is to avoid nasty stuff about dependent types.

                                noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIso {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U : Y.Opens) :
                                X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) Y.presheaf.obj (Opposite.op (Scheme.Hom.opensRange f U))

                                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
                                  @[simp]
                                  theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_inv {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U : Y.Opens) :
                                  theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U : Y.Opens) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) :
                                  (Scheme.Hom.appLE f (Scheme.Hom.opensRange f U) ((TopologicalSpace.Opens.map f.base).obj U) ) ((Y.presheaf.map (CategoryTheory.homOfLE ).op) x) = (Scheme.Hom.app f U) x
                                  theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map_apply {X Y : Scheme} (f : X Y) [IsOpenImmersion f] (U : Y.Opens) (x : (CategoryTheory.forget CommRingCat).obj (Y.presheaf.obj (Opposite.op U))) :
                                  (ΓIso f U).hom ((Scheme.Hom.app f U) x) = (Y.presheaf.map (CategoryTheory.homOfLE ).op) x
                                  noncomputable def AlgebraicGeometry.IsOpenImmersion.ΓIsoTop {X Y : Scheme} (f : X Y) [IsOpenImmersion f] :
                                  X.presheaf.obj (Opposite.op ) Y.presheaf.obj (Opposite.op (Scheme.Hom.opensRange f))

                                  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
                                    instance AlgebraicGeometry.IsOpenImmersion.instLift {X Y Z : Scheme} (f : X Z) (g : Y Z) [IsOpenImmersion f] (H' : Set.range g.base Set.range f.base) [IsOpenImmersion g] :
                                    theorem AlgebraicGeometry.Scheme.image_basicOpen {X Y : Scheme} (f : X Y) [H : IsOpenImmersion f] {U : X.Opens} (r : (X.presheaf.obj (Opposite.op U))) :
                                    (Hom.opensFunctor f).obj (X.basicOpen r) = Y.basicOpen ((Hom.appIso f U).inv.hom r)