Biseparated presheaves

On any category with a two Grothendieck topologies J and K, we define the category Bisep J K of all presheaves that are sheaves with respect to J and separated with respect to K, and show that it is a reflective subcategory (TODO). Important examples (though not worked out in this file) are the categories of diffeological spaces, quasitopological spaces and simplicial complexes.

See https://ncatlab.org/nlab/show/separated+presheaf#biseparated_presheaf and section C.2.2 of Sketches of an Elephant.

structure CategoryTheory.Bisep {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) : Type (max (max u v) (w + 1))

The category of biseparated presheaves with respect to J and K, i.e. of all presheaves that are sheaves with respect to J and separated with respect to K.

• val : Functor Cᵒᵖ (Type w)

  The underlying presheaf.

• isSheaf : Presheaf.IsSheaf J self.val

  The underlying presheaf is a sheaf with respect to J.

• isSeparated : Presieve.IsSeparated K self.val

  The underlying presheaf is separated with respect to K.

structure CategoryTheory.Bisep.Hom {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (X Y : Bisep J K) : Type (max u u_1)

Morphisms of biseparated presheaves are just morphisms of their underlying presheaves.

• val : X.val ⟶ Y.val

  The underlying morphism of presheaves.

theorem CategoryTheory.Bisep.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {J K : GrothendieckTopology C} {X Y : Bisep J K} {x y : X.Hom Y} : x = y ↔ x.val = y.val

theorem CategoryTheory.Bisep.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {J K : GrothendieckTopology C} {X Y : Bisep J K} {x y : X.Hom Y} (val : x.val = y.val) : x = y

instance CategoryTheory.Bisep.instCategory {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} : Category.{max u u_1, max (max (u_1 + 1) v) u} (Bisep J K)

Equations

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

@[simp]

theorem CategoryTheory.Bisep.comp_val {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} {X✝ Y✝ Z✝ : Bisep J K} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).val = CategoryStruct.comp f.val g.val

@[simp]

theorem CategoryTheory.Bisep.id_val {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (x✝ : Bisep J K) : (CategoryStruct.id x✝).val = CategoryStruct.id x✝.val

def CategoryTheory.Bisep.toSheaf {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (P : Bisep J K) : Sheaf J (Type w)

The sheaf (with respect to J) underlying a biseparated presheaf.

Equations

• P.toSheaf = { val := P.val, cond := ⋯ }

@[simp]

theorem CategoryTheory.Bisep.toSheaf_val {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (P : Bisep J K) : P.toSheaf.val = P.val

def CategoryTheory.bisepToSheaf {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) : Functor (Bisep J K) (Sheaf J (Type w))

The inclusion functor from biseparated presheaves to sheaves.

Equations

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

@[simp]

theorem CategoryTheory.bisepToSheaf_map_val {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) {X✝ Y✝ : Bisep J K} (f : X✝ ⟶ Y✝) : ((bisepToSheaf J K).map f).val = f.val

@[simp]

theorem CategoryTheory.bisepToSheaf_obj {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) (P : Bisep J K) : (bisepToSheaf J K).obj P = P.toSheaf

def CategoryTheory.fullyFaithfulBisepToSheaf {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) : (bisepToSheaf J K).FullyFaithful

The inclusion functor from biseparated presheaves to sheaves is fully faithful.

Equations

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

instance CategoryTheory.instFullBisepSheafTypeBisepToSheaf {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} : (bisepToSheaf J K).Full

instance CategoryTheory.instFaithfulBisepSheafTypeBisepToSheaf {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} : (bisepToSheaf J K).Faithful

instance CategoryTheory.instReflectsIsomorphismsBisepSheafTypeBisepToSheaf {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} : (bisepToSheaf J K).ReflectsIsomorphisms

noncomputable def CategoryTheory.Sheaf.toExpΩ' {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) (X : Sheaf J (Type (max u v))) : X ⟶ X ⟹ GrothendieckTopology.Ω' h

Equations

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

def CategoryTheory.Functor.chosenExp {C : Type u} [Category.{v, u} C] (F G : Functor Cᵒᵖ (Type (max u v))) : Functor Cᵒᵖ (Type (max u v))

A more concrete choice of exponential object in presheaf categories.

Equations

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

@[simp]

theorem CategoryTheory.Functor.chosenExp_map {C : Type u} [Category.{v, u} C] (F G : Functor Cᵒᵖ (Type (max u v))) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (g : MonoidalCategoryStruct.tensorObj F (uliftYoneda.{u, v, u}.obj (Opposite.unop X✝)) ⟶ G) : (F.chosenExp G).map f g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft F (uliftYoneda.{u, v, u}.map f.unop)) g

@[simp]

theorem CategoryTheory.Functor.chosenExp_obj {C : Type u} [Category.{v, u} C] (F G : Functor Cᵒᵖ (Type (max u v))) (X : Cᵒᵖ) : (F.chosenExp G).obj X = (MonoidalCategoryStruct.tensorObj F (uliftYoneda.{u, v, u}.obj (Opposite.unop X)) ⟶ G)

theorem CategoryTheory.uliftYonedaEquiv_naturality_symm {C : Type u} [Category.{v, u} C] {X Y : Cᵒᵖ} {F : Functor Cᵒᵖ (Type (max w v))} (x : F.obj X) (f : X ⟶ Y) : uliftYonedaEquiv.symm (F.map f x) = CategoryStruct.comp (uliftYoneda.{w, v, u}.map f.unop) (uliftYonedaEquiv.symm x)

noncomputable def CategoryTheory.Functor.expObjIsoChosenExp {C : Type u} [Category.{v, u} C] (F G : Functor Cᵒᵖ (Type (max u v))) : F ⟹ G ≅ F.chosenExp G

Isomorphism witnessing that in presheaf categories, exponential objects are indeed isomorphic to Functor.chosenExp.

Equations

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

theorem CategoryTheory.Presieve.IsSeparated.exp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F : Functor Cᵒᵖ (Type (max u v))} (hF : IsSeparated J F) (G : Functor Cᵒᵖ (Type (max u v))) : IsSeparated J (G ⟹ F)

theorem CategoryTheory.Presheaf.IsSheaf.exp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasSheafify J A] [CartesianMonoidalCategory A] [CartesianClosed (Functor Cᵒᵖ A)] {F : Functor Cᵒᵖ A} (hF : IsSheaf J F) (G : Functor Cᵒᵖ A) : IsSheaf J (G ⟹ F)

noncomputable def CategoryTheory.sheafToBisep {C : Type u} [Category.{v, u} C] (J K : GrothendieckTopology C) : Functor (Sheaf J (Type (max u v))) (Bisep J K)

Equations

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