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.

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

      The trivial unit valued sheaf on any topological space.

      Instances For
        theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
        ∀ {X Y : CategoryTheory.InducedCategory (AlgebraicGeometry.PresheafedSpace C) AlgebraicGeometry.SheafedSpace.toPresheafedSpace} (f : X Y), f = f
        theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (self : AlgebraicGeometry.SheafedSpace C) :
        AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace
        instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
        CategoryTheory.Full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
        theorem AlgebraicGeometry.SheafedSpace.congr_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.SheafedSpace C} {Y : AlgebraicGeometry.SheafedSpace C} {α : X Y} {β : X Y} (h : α = β) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
        α U = CategoryTheory.CategoryStruct.comp (β U) ( (CategoryTheory.eqToHom (_ : ( β.base).op.obj U = ( α.base).op.obj U)))

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

        Instances For

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

          Instances For
            theorem AlgebraicGeometry.SheafedSpace.Γ_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
            AlgebraicGeometry.SheafedSpace.Γ = CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op AlgebraicGeometry.PresheafedSpace.Γ
            theorem AlgebraicGeometry.SheafedSpace.Γ_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (X : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ) :
            AlgebraicGeometry.SheafedSpace.Γ.obj X = X.unop.presheaf.obj (Opposite.op )
            theorem AlgebraicGeometry.SheafedSpace.Γ_obj_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) :
            AlgebraicGeometry.SheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op )
            theorem AlgebraicGeometry.SheafedSpace.Γ_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ} {Y : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ} (f : X Y) :
            AlgebraicGeometry.SheafedSpace.Γ.map f = (Opposite.op )
            theorem AlgebraicGeometry.SheafedSpace.Γ_map_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.SheafedSpace C} {Y : AlgebraicGeometry.SheafedSpace C} (f : X Y) :
            AlgebraicGeometry.SheafedSpace.Γ.map f.op = (Opposite.op )