Documentation

Mathlib.Geometry.RingedSpace.PresheafedSpace

Presheafed spaces #

Introduces the category of topological spaces equipped with a presheaf (taking values in an arbitrary target category C.)

We further describe how to apply functors and natural transformations to the values of the presheaves.

structure AlgebraicGeometry.PresheafedSpace (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
Type (max (max u_1 u_2) (u_3 + 1))

A PresheafedSpace C is a topological space equipped with a presheaf of Cs.

Instances For
    Equations
    Equations
    theorem AlgebraicGeometry.PresheafedSpace.mk_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) :
    { carrier := carrier, presheaf := presheaf } = carrier

    The constant presheaf on X with value Z.

    Equations
    Instances For

      A morphism between presheafed spaces X and Y consists of a continuous map f between the underlying topological spaces, and a (notice contravariant!) map from the presheaf on Y to the pushforward of the presheaf on X via f.

      Instances For
        theorem AlgebraicGeometry.PresheafedSpace.hext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X.Hom Y) (β : X.Hom Y) (w : α.base = β.base) (h : HEq α.c β.c) :
        α = β

        The identity morphism of a PresheafedSpace.

        Equations
        Instances For
          Equations
          • X.homInhabited = { default := X.id }

          Composition of morphisms of PresheafedSpaces.

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

            The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map from the presheaf on the target to the pushforward of the presheaf on the source.

            Equations
            Equations
            • X.instCoeFunHomForallαTopologicalSpaceCarrier Y = { coe := fun (f : X Y) => f.base }
            @[simp]

            Sometimes rewriting with comp_c_app doesn't work because of dependent type issues. In that case, erw comp_c_app_assoc might make progress. The lemma comp_c_app_assoc is also better suited for rewrites in the opposite direction.

            The forgetful functor from PresheafedSpace to TopCat.

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

              An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.

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

                Isomorphic PresheafedSpaces have naturally isomorphic presheaves.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem AlgebraicGeometry.PresheafedSpace.restrict_presheaf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U X} (h : OpenEmbedding f) :
                  (X.restrict h).presheaf = .functor.op.comp X.presheaf

                  The restriction of a presheafed space along an open embedding into the space.

                  Equations
                  • X.restrict h = { carrier := U, presheaf := .functor.op.comp X.presheaf }
                  Instances For
                    @[simp]
                    @[simp]
                    theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U X} (h : OpenEmbedding f) (V : (TopologicalSpace.Opens X)ᵒᵖ) :
                    (X.ofRestrict h).c.app V = X.presheaf.map (.adjunction.counit.app (Opposite.unop V)).op

                    The map from the restriction of a presheafed space.

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

                      The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.

                      Equations
                      Instances For

                        The isomorphism from the restriction to the top subspace.

                        Equations
                        • X.restrictTopIso = { hom := X.ofRestrict , inv := X.toRestrictTop, hom_inv_id := , inv_hom_id := }
                        Instances For
                          @[simp]
                          theorem AlgebraicGeometry.PresheafedSpace.Γ_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                          ∀ {X Y : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ} (f : X Y), AlgebraicGeometry.PresheafedSpace.Γ.map f = f.unop.c.app (Opposite.op )
                          @[simp]
                          theorem AlgebraicGeometry.PresheafedSpace.Γ_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ) :
                          AlgebraicGeometry.PresheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op )

                          The global sections, notated Gamma.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem AlgebraicGeometry.PresheafedSpace.Γ_obj_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) :
                            AlgebraicGeometry.PresheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op )

                            We can apply a functor F : C ⥤ D to the values of the presheaf in any PresheafedSpace C, giving a functor PresheafedSpace C ⥤ PresheafedSpace D

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

                              A natural transformation induces a natural transformation between the map_presheaf functors.

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