Documentation

Mathlib.AlgebraicGeometry.Restrict

Restriction of Schemes and Morphisms #

Main definition #

Open subset of a scheme as a scheme.

Equations
  • U = X.restrict
Instances For
    Equations
    • AlgebraicGeometry.Scheme.Opens.instCoeOut = { coe := AlgebraicGeometry.Scheme.Opens.toScheme }
    @[simp]
    theorem AlgebraicGeometry.Scheme.Opens.ι_val_base_apply {X : AlgebraicGeometry.Scheme} (U : X.Opens) (self : U) :
    U.val.base self = self

    The restriction of a scheme to an open subset.

    Equations
    • U = X.ofRestrict
    Instances For
      theorem AlgebraicGeometry.Scheme.Opens.toScheme_carrier {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      (↑U).toPresheafedSpace = U
      theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) :
      (↑U).presheaf.obj (Opposite.op V) = X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V))
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (TopologicalSpace.Opens (↑U).toPresheafedSpace)ᵒᵖ} {W : (TopologicalSpace.Opens (↑U).toPresheafedSpace)ᵒᵖ} (i : V W) :
      (↑U).presheaf.map i = X.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).map i.unop).op
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.ι_app {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : X.Opens) :
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.ι_appLE {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : X.Opens) (W : (↑U).Opens) (e : W (TopologicalSpace.Opens.map U.val.base).obj V) :
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.range_ι {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      Set.range U.val.base = U
      theorem AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} {W : (↑U).Opens} (e : (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V = (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj W) :
      X.presheaf.map (CategoryTheory.eqToHom e).op = (↑U).presheaf.map (CategoryTheory.eqToHom ).op
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.nonempty_iff {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      Nonempty (↑U).toPresheafedSpace (↑U).Nonempty
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.topIso_hom {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      U.topIso.hom = X.presheaf.map (CategoryTheory.eqToHom ).op
      @[simp]
      theorem AlgebraicGeometry.Scheme.Opens.topIso_inv {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      U.topIso.inv = X.presheaf.map (CategoryTheory.eqToHom ).op
      def AlgebraicGeometry.Scheme.Opens.topIso {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
      (↑U).presheaf.obj (Opposite.op ) X.presheaf.obj (Opposite.op U)

      The global sections of the restriction is isomorphic to the sections on the open set.

      Equations
      Instances For
        def AlgebraicGeometry.Scheme.Opens.stalkIso {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : U) :
        (↑U).presheaf.stalk x X.presheaf.stalk x

        The stalks of an open subscheme are isomorphic to the stalks of the original scheme.

        Equations
        • U.stalkIso x = X.restrictStalkIso x
        Instances For
          @[simp]
          theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} (x : U) (hx : x V) {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
          CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) (CategoryTheory.CategoryStruct.comp (U.stalkIso x).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V) x ) h
          @[simp]
          theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} (x : U) (hx : x V) :
          CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) (U.stalkIso x).hom = X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V) x
          theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) (x : U) (hx : x V) {Z : CommRingCat} (h : (↑U).presheaf.stalk x Z) :
          CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V) x ) (CategoryTheory.CategoryStruct.comp (U.stalkIso x).inv h) = CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) h
          theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) (x : U) (hx : x V) :
          CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj V) x ) (U.stalkIso x).inv = (↑U).presheaf.germ V x hx
          @[simp]
          theorem AlgebraicGeometry.Scheme.openCoverOfISupEqTop_J {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sX.Opens) (hU : ⨆ (i : s), U i = ) :
          (X.openCoverOfISupEqTop U hU).J = s
          @[simp]
          theorem AlgebraicGeometry.Scheme.openCoverOfISupEqTop_map {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sX.Opens) (hU : ⨆ (i : s), U i = ) (i : s) :
          (X.openCoverOfISupEqTop U hU).map i = (U i)
          @[simp]
          theorem AlgebraicGeometry.Scheme.openCoverOfISupEqTop_obj {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sX.Opens) (hU : ⨆ (i : s), U i = ) (i : s) :
          (X.openCoverOfISupEqTop U hU).obj i = (U i)
          def AlgebraicGeometry.Scheme.openCoverOfISupEqTop {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sX.Opens) (hU : ⨆ (i : s), U i = ) :
          X.OpenCover

          If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

          Equations
          • X.openCoverOfISupEqTop U hU = { J := s, obj := fun (i : s) => (U i), map := fun (i : s) => (U i), f := fun (x : X.toPresheafedSpace) => .choose, covers := , IsOpen := }
          Instances For
            @[deprecated AlgebraicGeometry.Scheme.openCoverOfISupEqTop]
            def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sX.Opens) (hU : ⨆ (i : s), U i = ) :
            X.OpenCover

            Alias of AlgebraicGeometry.Scheme.openCoverOfISupEqTop.


            If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

            Equations
            Instances For
              @[simp]
              theorem AlgebraicGeometry.opensRestrict_apply_coe_coe {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
              ∀ (a : (↑U).Opens), ((AlgebraicGeometry.opensRestrict U) a) = U.val.base '' a
              @[simp]
              theorem AlgebraicGeometry.opensRestrict_symm_apply_coe {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
              ∀ (a : { V : X.Opens // V U }), ((AlgebraicGeometry.opensRestrict U).symm a) = U.val.base ⁻¹' ((Equiv.subtypeEquivProp ).symm a)
              def AlgebraicGeometry.opensRestrict {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
              (↑U).Opens { V : X.Opens // V U }

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

              Equations
              Instances For
                theorem AlgebraicGeometry.Scheme.map_basicOpen' {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ((↑U).presheaf.obj (Opposite.op ))) :
                (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj ((↑U).basicOpen r) = X.basicOpen ((X.presheaf.map (CategoryTheory.eqToHom ).op) r)
                theorem AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ((↑U).presheaf.obj (Opposite.op ))) :
                (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj ((↑U).basicOpen r) = X.basicOpen r
                theorem AlgebraicGeometry.Scheme.map_basicOpen_map {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : (X.presheaf.obj (Opposite.op U))) :
                (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj ((↑U).basicOpen (U.topIso.inv r)) = X.basicOpen r

                The functor taking open subsets of X to open subschemes of X.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
                  (X.restrictFunctor.obj U).left = U
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
                  (X.restrictFunctor.obj U).hom = U
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U V) :
                  (X.restrictFunctor.map i).left = AlgebraicGeometry.IsOpenImmersion.lift V U

                  This is not a simp lemma, as (X.restricFunctor.map i).left is used as the simp normal-form for the induced morphism U.toScheme ⟶ V.toScheme.

                  theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U V) :
                  CategoryTheory.CategoryStruct.comp (X.restrictFunctor.map i).left V = U
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U V) :
                  (X.restrictFunctor.map i).left.val.base = (TopologicalSpace.Opens.toTopCat X.toPresheafedSpace).map i
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U V) (W : (↑V).Opens) :
                  (AlgebraicGeometry.Scheme.Hom.opensFunctor U).obj ((TopologicalSpace.Opens.map (X.restrictFunctor.map i).left.val.base).obj W) (AlgebraicGeometry.Scheme.Hom.opensFunctor V).obj W
                  theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : X.Opens} (i : U V) (W : (↑V).Opens) :
                  AlgebraicGeometry.Scheme.Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (CategoryTheory.homOfLE ).op
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app {X : AlgebraicGeometry.Scheme} (X : X✝.Opensᵒᵖ) :
                  AlgebraicGeometry.Scheme.restrictFunctorΓ.hom.app X = X✝.presheaf.map (CategoryTheory.eqToHom )
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app {X : AlgebraicGeometry.Scheme} (X : X✝.Opensᵒᵖ) :
                  AlgebraicGeometry.Scheme.restrictFunctorΓ.inv.app X = X✝.presheaf.map (CategoryTheory.eqToHom )

                  The functor that restricts to open subschemes and then takes global section is isomorphic to the structure sheaf.

                  Equations
                  Instances For
                    noncomputable def AlgebraicGeometry.Scheme.restrictRestrictComm (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : X.Opens) :
                    ((TopologicalSpace.Opens.map U.val.base).obj V) ((TopologicalSpace.Opens.map V.val.base).obj U)

                    X ∣_ U ∣_ V is isomorphic to X ∣_ V ∣_ U

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      noncomputable def AlgebraicGeometry.Scheme.restrictRestrict (X : AlgebraicGeometry.Scheme) (U : X.Opens) (V : (↑U).Opens) :

                      If V is an open subset of U, then X ∣_ U ∣_ V is isomorphic to X ∣_ V.

                      Equations
                      Instances For
                        noncomputable def AlgebraicGeometry.Scheme.restrictIsoOfEq (X : AlgebraicGeometry.Scheme) {U : X.Opens} {V : X.Opens} (e : U = V) :
                        U V

                        If U = V, then X ∣_ U is isomorphic to X ∣_ V.

                        Equations
                        Instances For
                          @[reducible, inline]
                          noncomputable abbrev AlgebraicGeometry.Scheme.restrictMapIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [CategoryTheory.IsIso f] (U : Y.Opens) :
                          ((TopologicalSpace.Opens.map f.val.base).obj U) U

                          The restriction of an isomorphism onto an open set.

                          Equations
                          Instances For

                            Given a morphism f : X ⟶ Y and an open set U ⊆ Y, we have X ×[Y] U ≅ X |_{f ⁻¹ U}

                            Equations
                            Instances For

                              The restriction of a morphism X ⟶ Y onto X |_{f ⁻¹ U} ⟶ Y |_ U.

                              Equations
                              Instances For

                                the notation for restricting a morphism of scheme to an open subset of the target scheme

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem AlgebraicGeometry.morphismRestrict_base_coe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : Y.Opens) (x : (↑((TopologicalSpace.Opens.map f.val.base).obj U)).toPresheafedSpace) :
                                  Coe.coe ((f ∣_ U).val.base x) = f.val.base x
                                  theorem AlgebraicGeometry.morphismRestrict_val_base {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : Y.Opens) :
                                  (f ∣_ U).val.base = U.carrier.restrictPreimage f.val.base

                                  Restricting a morphism onto the image of an open immersion is isomorphic to the base change along the immersion.

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

                                    The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.

                                    Equations
                                    Instances For

                                      Restricting a morphism twice is isomorphic to one restriction.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def AlgebraicGeometry.morphismRestrictRestrictBasicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : Y.Opens) (r : (Y.presheaf.obj (Opposite.op U))) :
                                        CategoryTheory.Arrow.mk (f ∣_ U ∣_ (↑U).basicOpen ((Y.presheaf.map (CategoryTheory.eqToHom ).op) r)) CategoryTheory.Arrow.mk (f ∣_ Y.basicOpen r)

                                        Restricting a morphism twice onto a basic open set is isomorphic to one restriction.

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

                                          The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def AlgebraicGeometry.Scheme.Hom.resLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (U : Y.Opens) (V : X.Opens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U) :
                                            V U

                                            The restriction of a morphism f : X ⟶ Y to open sets on the source and target.

                                            Equations
                                            Instances For
                                              theorem AlgebraicGeometry.Scheme.Hom.resLE_id {X : AlgebraicGeometry.Scheme} {V : X.Opens} {V' : X.Opens} (i : V V') :
                                              AlgebraicGeometry.Scheme.Hom.resLE (CategoryTheory.CategoryStruct.id X) V' V = (X.restrictFunctor.map i).left
                                              @[simp]
                                              theorem AlgebraicGeometry.Scheme.Hom.map_resLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {V : X.Opens} {V' : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : V' V) :
                                              @[simp]
                                              theorem AlgebraicGeometry.Scheme.Hom.resLE_map_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : U U') {Z : AlgebraicGeometry.Scheme} (h : (Y.restrictFunctor.obj U').left Z) :
                                              @[simp]
                                              theorem AlgebraicGeometry.Scheme.Hom.resLE_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : U U') :
                                              theorem AlgebraicGeometry.Scheme.Hom.resLE_congr {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} {V' : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (e₁ : U = U') (e₂ : V = V') (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) :
                                              theorem AlgebraicGeometry.Scheme.Hom.resLE_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (O : (↑U).Opens) :
                                              theorem AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens) :

                                              f.resLE U V induces f.appLE U V on global sections.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem AlgebraicGeometry.Scheme.OpenCover.restrict_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) :
                                                ∀ (x : 𝒰.J), (𝒰.restrict U).obj x = ((TopologicalSpace.Opens.map (𝒰.map x).val.base).obj U)
                                                @[simp]
                                                theorem AlgebraicGeometry.Scheme.OpenCover.restrict_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) :
                                                (𝒰.restrict U).J = 𝒰.J
                                                @[simp]
                                                theorem AlgebraicGeometry.Scheme.OpenCover.restrict_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) :
                                                ∀ (x : 𝒰.J), (𝒰.restrict U).map x = 𝒰.map x ∣_ U
                                                noncomputable def AlgebraicGeometry.Scheme.OpenCover.restrict {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) :
                                                (↑U).OpenCover

                                                The restriction of an open cover to an open subset.

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