Documentation

Mathlib.Geometry.RingedSpace.SheafedSpace

Sheafed spaces #

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

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

A SheafedSpace C is a topological space equipped with a sheaf of Cs.

Instances For

    Extract the sheaf C (X : Top) from a SheafedSpace C.

    Equations
    Instances For
      theorem AlgebraicGeometry.SheafedSpace.mk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) (h : presheaf.IsSheaf) :
      { carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier

      Not @[simp] since it already reduces to carrier = carrier.

      The trivial unit-valued sheaf on any topological space.

      Equations
      Instances For

        Constructor for isomorphisms in the category SheafedSpace C.

        Equations
        Instances For

          The forgetful functor from SheafedSpace to Top.

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

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

            Equations
            Instances For

              The map from the restriction of a presheafed space.

              Equations
              Instances For

                The restriction of a sheafed space X to the top subspace is isomorphic to X itself.

                Equations
                Instances For