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

• carrier : TopCat
• presheaf : TopCat.Presheaf C ↑s

A PresheafedSpace C is a topological space equipped with a presheaf of Cs.

instance AlgebraicGeometry.PresheafedSpace.coeCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CoeOut (AlgebraicGeometry.PresheafedSpace C) TopCat

instance AlgebraicGeometry.PresheafedSpace.instCoeSortPresheafedSpaceType {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] : CoeSort (AlgebraicGeometry.PresheafedSpace C) (Type u_2)

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

instance AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceαCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : TopologicalSpace ↑↑X

def AlgebraicGeometry.PresheafedSpace.const {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : TopCat) (Z : C) : AlgebraicGeometry.PresheafedSpace C

The constant presheaf on X with value Z.

instance AlgebraicGeometry.PresheafedSpace.instInhabitedPresheafedSpace {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [Inhabited C] : Inhabited (AlgebraicGeometry.PresheafedSpace C)

structure AlgebraicGeometry.PresheafedSpace.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) (Y : AlgebraicGeometry.PresheafedSpace C) : Type (max u_2 u_3)

• base : ↑X ⟶ ↑Y
• c : Y.presheaf ⟶ s.base _* X.presheaf

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.

theorem AlgebraicGeometry.PresheafedSpace.Hom.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : AlgebraicGeometry.PresheafedSpace.Hom X Y) (β : AlgebraicGeometry.PresheafedSpace.Hom X Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op)) X.presheaf) = β.c) : α = β

theorem AlgebraicGeometry.PresheafedSpace.hext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : AlgebraicGeometry.PresheafedSpace.Hom X Y) (β : AlgebraicGeometry.PresheafedSpace.Hom X Y) (w : α.base = β.base) (h : HEq α.c β.c) : α = β

def AlgebraicGeometry.PresheafedSpace.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : AlgebraicGeometry.PresheafedSpace.Hom X X

The identity morphism of a PresheafedSpace.

instance AlgebraicGeometry.PresheafedSpace.homInhabited {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : Inhabited (AlgebraicGeometry.PresheafedSpace.Hom X X)

def AlgebraicGeometry.PresheafedSpace.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (α : AlgebraicGeometry.PresheafedSpace.Hom X Y) (β : AlgebraicGeometry.PresheafedSpace.Hom Y Z) : AlgebraicGeometry.PresheafedSpace.Hom X Z

Composition of morphisms of PresheafedSpaces.

theorem AlgebraicGeometry.PresheafedSpace.comp_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (α : AlgebraicGeometry.PresheafedSpace.Hom X Y) (β : AlgebraicGeometry.PresheafedSpace.Hom Y Z) : (AlgebraicGeometry.PresheafedSpace.comp α β).c = CategoryTheory.CategoryStruct.comp β.c ((TopCat.Presheaf.pushforward C β.base).map α.c)

instance AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Category.{max u_2 u_3, max (max (u_3 + 1) u_2) u_1} (AlgebraicGeometry.PresheafedSpace C)

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.

theorem AlgebraicGeometry.PresheafedSpace.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (β : X ⟶ Y) (w : α.base = β.base) (h : CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op)) X.presheaf) = β.c) : α = β

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.id_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X

theorem AlgebraicGeometry.PresheafedSpace.id_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (CategoryTheory.CategoryStruct.id X).c = CategoryTheory.CategoryStruct.id X.presheaf

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.id_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) (U : (TopologicalSpace.Opens ↑↑X)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).c.app U = X.presheaf.map (CategoryTheory.CategoryStruct.id U)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.comp_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

instance AlgebraicGeometry.PresheafedSpace.instCoeFunHomPresheafedSpaceToQuiverToCategoryStructCategoryOfPresheafedSpacesForAllαTopologicalSpaceCarrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) (Y : AlgebraicGeometry.PresheafedSpace C) : CoeFun (X ⟶ Y) fun x => ↑↑X → ↑↑Y

theorem AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ) {Z : C} (h : ((CategoryTheory.CategoryStruct.comp α β).base _* X.presheaf).obj U ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).c.app U) h = CategoryTheory.CategoryStruct.comp (β.c.app U) (CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj U.unop))) h)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.comp_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp α β).c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj U.unop)))

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.

theorem AlgebraicGeometry.PresheafedSpace.congr_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {α : X ⟶ Y} {β : X ⟶ Y} (h : α = β) (U : (TopologicalSpace.Opens ↑↑Y)ᵒᵖ) : α.c.app U = CategoryTheory.CategoryStruct.comp (β.c.app U) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map β.base).op.obj U = (TopologicalSpace.Opens.map α.base).op.obj U)))

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.forget_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.forget C).obj X = ↑X

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.forget_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : ∀ {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y), (AlgebraicGeometry.PresheafedSpace.forget C).map f = f.base

def AlgebraicGeometry.PresheafedSpace.forget (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C) TopCat

The forgetful functor from PresheafedSpace to TopCat.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : H.hom _* X.presheaf ≅ Y.presheaf) : (AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).hom = { base := H.hom, c := α.inv }

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : H.hom _* X.presheaf ≅ Y.presheaf) : (AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).inv = { base := H.inv, c := TopCat.Presheaf.toPushforwardOfIso H α.hom }

def AlgebraicGeometry.PresheafedSpace.isoOfComponents {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : ↑X ≅ ↑Y) (α : H.hom _* X.presheaf ≅ Y.presheaf) : X ≅ Y

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y) : (AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).inv = TopCat.Presheaf.pushforwardToOfIso ((AlgebraicGeometry.PresheafedSpace.forget C).mapIso H).symm H.inv.c

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y) : (AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).hom = H.hom.c

def AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y) : Y.presheaf ≅ H.hom.base _* X.presheaf

Isomorphic PresheafedSpaces have naturally isomorphic presheaves.

instance AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.base

instance AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.c

theorem AlgebraicGeometry.PresheafedSpace.isIso_of_components {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) [CategoryTheory.IsIso f.base] [CategoryTheory.IsIso f.c] : CategoryTheory.IsIso f

This could be used in conjunction with CategoryTheory.NatIso.isIso_of_isIso_app.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrict_carrier {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) : ↑(AlgebraicGeometry.PresheafedSpace.restrict X h) = U

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrict_presheaf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) : (AlgebraicGeometry.PresheafedSpace.restrict X h).presheaf = CategoryTheory.Functor.comp (IsOpenMap.functor (_ : IsOpenMap ↑f)).op X.presheaf

def AlgebraicGeometry.PresheafedSpace.restrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) : AlgebraicGeometry.PresheafedSpace C

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

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) (V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ) : (AlgebraicGeometry.PresheafedSpace.ofRestrict X h).c.app V = X.presheaf.map ((IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit.app V.unop).op

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) : (AlgebraicGeometry.PresheafedSpace.ofRestrict X h).base = f

def AlgebraicGeometry.PresheafedSpace.ofRestrict {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ↑f) : AlgebraicGeometry.PresheafedSpace.restrict X h ⟶ X

The map from the restriction of a presheafed space.

instance AlgebraicGeometry.PresheafedSpace.ofRestrict_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) (f : U ⟶ ↑X) (hf : OpenEmbedding ↑f) : CategoryTheory.Mono (AlgebraicGeometry.PresheafedSpace.ofRestrict X hf)

theorem AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))).presheaf = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv _* X.presheaf

theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))).c = CategoryTheory.eqToHom (_ : X.presheaf = (AlgebraicGeometry.PresheafedSpace.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))).base _* (AlgebraicGeometry.PresheafedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))).presheaf)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_c {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.toRestrictTop X).c = CategoryTheory.eqToHom (_ : (AlgebraicGeometry.PresheafedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))).presheaf = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv _* X.presheaf)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.toRestrictTop_base {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.toRestrictTop X).base = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv

def AlgebraicGeometry.PresheafedSpace.toRestrictTop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : X ⟶ AlgebraicGeometry.PresheafedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))

The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.restrictTopIso X).inv = AlgebraicGeometry.PresheafedSpace.toRestrictTop X

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : (AlgebraicGeometry.PresheafedSpace.restrictTopIso X).hom = AlgebraicGeometry.PresheafedSpace.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤))

def AlgebraicGeometry.PresheafedSpace.restrictTopIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) : AlgebraicGeometry.PresheafedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤)) ≅ X

The isomorphism from the restriction to the top subspace.

@[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 ⊤)

def AlgebraicGeometry.PresheafedSpace.Γ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ C

The global sections, notated Gamma.

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 ⊤)

theorem AlgebraicGeometry.PresheafedSpace.Γ_map_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) : AlgebraicGeometry.PresheafedSpace.Γ.map f.op = f.c.app (Opposite.op ⊤)

def CategoryTheory.Functor.mapPresheaf {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C) (AlgebraicGeometry.PresheafedSpace D)

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

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_obj_X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) (X : AlgebraicGeometry.PresheafedSpace C) : ↑((CategoryTheory.Functor.mapPresheaf F).obj X) = ↑X

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_obj_presheaf {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) (X : AlgebraicGeometry.PresheafedSpace C) : ((CategoryTheory.Functor.mapPresheaf F).obj X).presheaf = CategoryTheory.Functor.comp X.presheaf F

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_map_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) : ((CategoryTheory.Functor.mapPresheaf F).map f).base = f.base

@[simp]

theorem CategoryTheory.Functor.mapPresheaf_map_c {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) : ((CategoryTheory.Functor.mapPresheaf F).map f).c = CategoryTheory.whiskerRight f.c F

def CategoryTheory.NatTrans.onPresheaf {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) : CategoryTheory.Functor.mapPresheaf G ⟶ CategoryTheory.Functor.mapPresheaf F

A natural transformation induces a natural transformation between the map_presheaf functors.