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.

      • base : X Y
      • c : Y.presheaf s.base _* X.presheaf
      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
        @[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
          @[simp]

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

          Equations
          Instances For

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

            Equations
            Instances For

              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
                • One or more equations did not get rendered due to their size.
                Instances For

                  The isomorphism from the restriction to the top subspace.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem AlgebraicGeometry.PresheafedSpace.Γ_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ) :
                    AlgebraicGeometry.PresheafedSpace.Γ.obj X = X.unop.presheaf.obj (Opposite.op )
                    @[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 )

                    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