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.

  • carrier : TopCat
  • presheaf : TopCat.Presheaf C self.toPresheafedSpace
  • IsSheaf : self.presheaf.IsSheaf

    A sheafed space is presheafed space which happens to be sheaf.

Instances For

    A sheafed space is presheafed space which happens to be sheaf.

    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
        Equations
        • AlgebraicGeometry.SheafedSpace.instCategory = let_fun this := inferInstance; this

        Constructor for isomorphisms in the category SheafedSpace C.

        Equations
        Instances For
          @[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
          @[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

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

          Equations
          Instances For
            instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full {C : Type u} [CategoryTheory.Category.{v, u} C] :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Full
            Equations
            • =
            instance AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] :
            AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Faithful
            Equations
            • =
            theorem AlgebraicGeometry.SheafedSpace.congr_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : AlgebraicGeometry.SheafedSpace C} {Y : AlgebraicGeometry.SheafedSpace C} {α : X Y} {β : 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 = let __src := X.restrict h; { toPresheafedSpace := __src, IsSheaf := }
              Instances For
                @[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 : OpenEmbedding f) :
                (X.ofRestrict h).base = f
                @[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 : OpenEmbedding f) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
                (X.ofRestrict h).c.app V = X.presheaf.map (.adjunction.counit.app (Opposite.unop V)).op
                def AlgebraicGeometry.SheafedSpace.ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U X.toPresheafedSpace} (h : OpenEmbedding f) :
                X.restrict h X

                The map from the restriction of a presheafed space.

                Equations
                • X.ofRestrict h = X.ofRestrict h
                Instances For

                  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 : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ} {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 : AlgebraicGeometry.SheafedSpace C} {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.