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
    Equations
    Equations

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

    Equations
    • X.sheaf = { val := X.presheaf, cond := }
    Instances For
      theorem AlgebraicGeometry.SheafedSpace.mk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier) (h : { carrier := carrier, presheaf := presheaf }.presheaf.IsSheaf) :
      { carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier
      Equations
      • X.instTopologicalSpaceαCarrier = (↑X.toPresheafedSpace).str

      The trivial unit valued sheaf on any topological space.

      Equations
      Instances For
        def AlgebraicGeometry.SheafedSpace.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (e : X.toPresheafedSpace Y.toPresheafedSpace) :
        X Y

        Constructor for isomorphisms in the category SheafedSpace C.

        Equations
        Instances For
          @[simp]
          theorem AlgebraicGeometry.SheafedSpace.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (e : X.toPresheafedSpace Y.toPresheafedSpace) :
          @[simp]
          theorem AlgebraicGeometry.SheafedSpace.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (e : X.toPresheafedSpace Y.toPresheafedSpace) :

          Forgetting the sheaf condition is a functor from SheafedSpace C to PresheafedSpace C.

          Equations
          Instances For
            @[simp]
            theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.SheafedSpace C) :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace
            @[simp]
            theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.InducedCategory (AlgebraicGeometry.PresheafedSpace C) AlgebraicGeometry.SheafedSpace.toPresheafedSpace} (f : X✝ Y✝) :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f = f
            theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u} [CategoryTheory.Category.{v, u} C] :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Full
            theorem AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Faithful
            theorem AlgebraicGeometry.SheafedSpace.congr_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} {α β : X Y} (h : α = β) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
            α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map (CategoryTheory.eqToHom ))

            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
              • X.restrict h = { toPresheafedSpace := X.restrict h, IsSheaf := }
              Instances For
                def AlgebraicGeometry.SheafedSpace.ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                X.restrict h X

                The map from the restriction of a presheafed space.

                Equations
                • X.ofRestrict h = X.ofRestrict h
                Instances For
                  @[simp]
                  theorem AlgebraicGeometry.SheafedSpace.ofRestrict_c_app {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
                  (X.ofRestrict h).c.app V = X.presheaf.map (.adjunction.counit.app (Opposite.unop V)).op
                  @[simp]
                  theorem AlgebraicGeometry.SheafedSpace.ofRestrict_base {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U X.toPresheafedSpace} (h : Topology.IsOpenEmbedding f) :
                  (X.ofRestrict h).base = f

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

                  Equations
                  Instances For

                    The global sections, notated Gamma.

                    Equations
                    • AlgebraicGeometry.SheafedSpace.Γ = AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op.comp AlgebraicGeometry.PresheafedSpace.Γ
                    Instances For
                      theorem AlgebraicGeometry.SheafedSpace.Γ_def {C : Type u} [CategoryTheory.Category.{v, u} C] :
                      AlgebraicGeometry.SheafedSpace.Γ = AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op.comp AlgebraicGeometry.PresheafedSpace.Γ
                      @[simp]
                      theorem AlgebraicGeometry.SheafedSpace.Γ_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ) :
                      AlgebraicGeometry.SheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op )
                      theorem AlgebraicGeometry.SheafedSpace.Γ_obj_op {C : Type u} [CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C) :
                      AlgebraicGeometry.SheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op )
                      @[simp]
                      theorem AlgebraicGeometry.SheafedSpace.Γ_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ} (f : X Y) :
                      AlgebraicGeometry.SheafedSpace.Γ.map f = f.unop.c.app (Opposite.op )
                      theorem AlgebraicGeometry.SheafedSpace.Γ_map_op {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X Y) :
                      AlgebraicGeometry.SheafedSpace.Γ.map f.op = f.c.app (Opposite.op )
                      Equations
                      • One or more equations did not get rendered due to their size.