Documentation

Mathlib.AlgebraicGeometry.Restrict

Restriction of Schemes and Morphisms #

Main definition #

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 (Opens.map f.1.base).obj U, the preimage of an open set U under f.

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

      X ∣_ᵤ U is notation for X.restrict U.openEmbedding, the restriction of X to an open set U of X.

      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
          @[reducible, inline]
          abbrev AlgebraicGeometry.Scheme.ιOpens {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens X.toPresheafedSpace) :
          X ∣_ᵤ U X

          The restriction of a scheme to an open subset.

          Equations
          Instances For
            theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app_self {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens X.toPresheafedSpace) :
            (X.ofRestrict ).val.c.app { unop := U } = X.presheaf.map (CategoryTheory.eqToHom ).op
            theorem AlgebraicGeometry.Scheme.eq_restrict_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens X.toPresheafedSpace) {V : TopologicalSpace.Opens U} {W : TopologicalSpace.Opens U} (e : .functor.obj V = .functor.obj W) :
            X.presheaf.map (CategoryTheory.eqToHom e).op = (X ∣_ᵤ U).presheaf.map (CategoryTheory.eqToHom ).op
            instance AlgebraicGeometry.ΓRestrictAlgebra {X : AlgebraicGeometry.Scheme} {Y : TopCat} {f : Y X.toPresheafedSpace} (hf : OpenEmbedding f) :
            Algebra (AlgebraicGeometry.Scheme.Γ.obj { unop := X }) (AlgebraicGeometry.Scheme.Γ.obj { unop := X.restrict hf })
            Equations
            theorem AlgebraicGeometry.Scheme.map_basicOpen' (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (r : (AlgebraicGeometry.Scheme.Γ.obj { unop := X ∣_ᵤ U })) :
            .functor.obj ((X ∣_ᵤ U).basicOpen r) = X.basicOpen ((X.presheaf.map (CategoryTheory.eqToHom ).op) r)
            theorem AlgebraicGeometry.Scheme.map_basicOpen (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (r : (AlgebraicGeometry.Scheme.Γ.obj { unop := X ∣_ᵤ U })) :
            .functor.obj ((X ∣_ᵤ U).basicOpen r) = X.basicOpen r
            theorem AlgebraicGeometry.Scheme.map_basicOpen_map (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (r : (X.presheaf.obj { unop := U })) :
            .functor.obj ((X ∣_ᵤ U).basicOpen ((X.presheaf.map (CategoryTheory.eqToHom ).op) 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 : TopologicalSpace.Opens X.toPresheafedSpace) :
              (X.restrictFunctor.obj U).left = X ∣_ᵤ U
              @[simp]
              theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (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 : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : U V) (W : TopologicalSpace.Opens V) :
              .functor.obj ((X.restrictFunctor.map i).left⁻¹ᵁ W) .functor.obj W
              theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : U V) (W : TopologicalSpace.Opens V) :
              (X.restrictFunctor.map i).left.val.c.app { unop := W } = X.presheaf.map (CategoryTheory.homOfLE ).op
              @[simp]
              theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app (X : AlgebraicGeometry.Scheme) (X : (TopologicalSpace.Opens X✝.toPresheafedSpace)ᵒᵖ) :
              X✝.restrictFunctorΓ.hom.app X = X✝.presheaf.map (CategoryTheory.eqToHom )
              @[simp]
              theorem AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app (X : AlgebraicGeometry.Scheme) (X : (TopologicalSpace.Opens X✝.toPresheafedSpace)ᵒᵖ) :
              X✝.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
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def AlgebraicGeometry.Scheme.restrictRestrictComm (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens X.toPresheafedSpace) :
                X ∣_ᵤ U ∣_ᵤ AlgebraicGeometry.Scheme.ιOpens U⁻¹ᵁ V X ∣_ᵤ V ∣_ᵤ AlgebraicGeometry.Scheme.ιOpens V⁻¹ᵁ 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 : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens (X ∣_ᵤ U).toPresheafedSpace) :
                  X ∣_ᵤ U ∣_ᵤ V X ∣_ᵤ .functor.obj V

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def AlgebraicGeometry.Scheme.restrictIsoOfEq (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (e : U = V) :
                    X ∣_ᵤ U X ∣_ᵤ 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 : TopologicalSpace.Opens Y.toPresheafedSpace) :
                      X ∣_ᵤ f⁻¹ᵁ U Y ∣_ᵤ 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
                          def AlgebraicGeometry.morphismRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) :
                          X ∣_ᵤ f⁻¹ᵁ U Y ∣_ᵤ U

                          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 : TopologicalSpace.Opens Y.toPresheafedSpace) (x : (CategoryTheory.forget TopCat).obj (X ∣_ᵤ f⁻¹ᵁ 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 : TopologicalSpace.Opens Y.toPresheafedSpace) :
                              (f ∣_ U).val.base = U.carrier.restrictPreimage f.val.base
                              theorem AlgebraicGeometry.image_morphismRestrict_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) (V : TopologicalSpace.Opens U) :
                              .functor.obj ((f ∣_ U)⁻¹ᵁ V) = f⁻¹ᵁ .functor.obj V
                              theorem AlgebraicGeometry.morphismRestrict_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) (V : TopologicalSpace.Opens U) :
                              (f ∣_ U).val.c.app { unop := V } = CategoryTheory.CategoryStruct.comp (f.val.c.app { unop := .functor.obj V }) (X.presheaf.map (CategoryTheory.eqToHom ).op)

                              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
                                  def AlgebraicGeometry.morphismRestrictRestrict {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) (V : TopologicalSpace.Opens (Y ∣_ᵤ U).toPresheafedSpace) :

                                  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 : TopologicalSpace.Opens Y.toPresheafedSpace) (r : (Y.presheaf.obj { unop := U })) :
                                    CategoryTheory.Arrow.mk (f ∣_ U ∣_ (Y ∣_ᵤ 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