Discrete objects in sheaf categories.

This file defines the notion of a discrete object in a sheaf category. A discrete sheaf in this context is a sheaf F such that the counit (F(*))^cst ⟶ F is an isomorphism. Here * denotes a particular chosen terminal object of the defining site, and cst denotes the constant sheaf.

It is convenient to take an arbitrary terminal object; one might want to use this construction to talk about discrete sheaves on a site which has a particularly convenient terminal object, such as the one element space in CompHaus.

Main results

• isDiscrete_iff_mem_essImage : A sheaf is discrete if and only if it is in the essential image of the constant sheaf functor.
• isDiscrete_iff_of_equivalence : The property of a sheaf of being discrete is invariant under equivalence of sheaf categories.
• isDiscrete_iff_forget : Given a "forgetful" functor U : A ⥤ B a sheaf F : Sheaf J A is discrete if and only if the sheaf given by postcomposition with U is discrete.

Future work

• Use isDiscrete_iff_forget to prove that a condensed module is discrete if and only if its underlying condensed set is discrete.

@[reducible, inline]

abbrev CategoryTheory.Sheaf.IsDiscrete {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.HasWeakSheafify J A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) (F : CategoryTheory.Sheaf J A) : Prop

A sheaf is discrete if it is a discrete object of the "underlying object" functor from the sheaf category to the target category.

Equations

• CategoryTheory.Sheaf.IsDiscrete J ht F = CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J A ht).counit.app F)

theorem CategoryTheory.Sheaf.isDiscrete_of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {F : CategoryTheory.Sheaf J A} {X : A} (i : F ≅ (CategoryTheory.constantSheaf J A).obj X) : CategoryTheory.Sheaf.IsDiscrete J ht F

theorem CategoryTheory.Sheaf.isDiscrete_iff_mem_essImage {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) (F : CategoryTheory.Sheaf J A) : CategoryTheory.Sheaf.IsDiscrete J ht F ↔ F ∈ (CategoryTheory.constantSheaf J A).essImage

theorem CategoryTheory.Sheaf.isDiscrete_iff_mem_essImage' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {L : CategoryTheory.Functor A (CategoryTheory.Sheaf J A)} (adj : L ⊣ (CategoryTheory.sheafSections J A).obj (Opposite.op t)) (F : CategoryTheory.Sheaf J A) : CategoryTheory.Sheaf.IsDiscrete J ht F ↔ F ∈ L.essImage

theorem CategoryTheory.Sheaf.isDiscrete_iff_isIso_counit_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {L : CategoryTheory.Functor A (CategoryTheory.Sheaf J A)} (adj : L ⊣ (CategoryTheory.sheafSections J A).obj (Opposite.op t)) (F : CategoryTheory.Sheaf J A) : CategoryTheory.Sheaf.IsDiscrete J ht F ↔ CategoryTheory.IsIso (adj.counit.app F)

noncomputable def CategoryTheory.Sheaf.equivCommuteConstant {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_5, u_2} A] [CategoryTheory.HasWeakSheafify J A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify K A] (G : CategoryTheory.Functor C D) [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (ht' : CategoryTheory.Limits.IsTerminal (G.obj t)) : let e := CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A; (CategoryTheory.constantSheaf J A).comp e.functor ≅ CategoryTheory.constantSheaf K A

The constant sheaf functor commutes up to isomorphism with any equivalence of sheaf categories.

This is an auxiliary definition used to prove Sheaf.isDiscrete_iff below, which says that the property of a sheaf of being a discrete object is invariant under equivalence of sheaf categories.

Equations

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

noncomputable def CategoryTheory.Sheaf.equivCommuteConstant' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{u_5, u_2} A] [CategoryTheory.HasWeakSheafify J A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify K A] (G : CategoryTheory.Functor C D) [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (ht' : CategoryTheory.Limits.IsTerminal (G.obj t)) : let e := CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A; CategoryTheory.constantSheaf J A ≅ (CategoryTheory.constantSheaf K A).comp e.inverse

The constant sheaf functor commutes up to isomorphism with any equivalence of sheaf categories.

This is an auxiliary definition used to prove Sheaf.isDiscrete_iff below, which says that the property of a sheaf of being a discrete object is invariant under equivalence of sheaf categories.

Equations

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

theorem CategoryTheory.Sheaf.isDiscrete_iff_of_equivalence {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] [CategoryTheory.HasWeakSheafify J A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify K A] (G : CategoryTheory.Functor C D) [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (ht' : CategoryTheory.Limits.IsTerminal (G.obj t)) [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] (F : CategoryTheory.Sheaf K A) : let e := CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G J K A; CategoryTheory.Sheaf.IsDiscrete J ht (e.inverse.obj F) ↔ CategoryTheory.Sheaf.IsDiscrete K ht' F

The property of a sheaf of being a discrete object is invariant under equivalence of sheaf categories.

@[simp]

theorem CategoryTheory.Sheaf.constantCommuteCompose_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : A) (X : Cᵒᵖ) : ((CategoryTheory.Sheaf.constantCommuteCompose J U).inv.app X✝).val.app X = CategoryTheory.CategoryStruct.comp (((CategoryTheory.presheafToSheaf J B).map ((CategoryTheory.Functor.compConstIso Cᵒᵖ U).hom.app X✝)).val.app X) (((CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).hom.app ((CategoryTheory.Functor.const Cᵒᵖ).obj X✝)).val.app X)

@[simp]

theorem CategoryTheory.Sheaf.constantCommuteCompose_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : A) (X : Cᵒᵖ) : ((CategoryTheory.Sheaf.constantCommuteCompose J U).hom.app X✝).val.app X = CategoryTheory.CategoryStruct.comp (((CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).inv.app ((CategoryTheory.Functor.const Cᵒᵖ).obj X✝)).val.app X) (((CategoryTheory.presheafToSheaf J B).map ((CategoryTheory.Functor.compConstIso Cᵒᵖ U).inv.app X✝)).val.app X)

noncomputable def CategoryTheory.Sheaf.constantCommuteCompose {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] : (CategoryTheory.constantSheaf J A).comp (CategoryTheory.sheafCompose J U) ≅ U.comp (CategoryTheory.constantSheaf J B)

The constant sheaf functor commutes with sheafCompose up to isomorphism.

Equations

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

theorem CategoryTheory.Sheaf.sheafComposeNatIso_app_counit {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (P : CategoryTheory.Sheaf J A) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.sheafComposeNatIso J U (CategoryTheory.sheafificationAdjunction J A) (CategoryTheory.sheafificationAdjunction J B)).hom.app ((CategoryTheory.sheafToPresheaf J A).obj P)) ((CategoryTheory.sheafCompose J U).map ((CategoryTheory.sheafificationAdjunction J A).counit.app P)) = (CategoryTheory.sheafificationAdjunction J B).counit.app ((CategoryTheory.sheafCompose J U).obj P)

theorem CategoryTheory.Sheaf.constantCommuteComposeApp_comp_counit {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J A) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.constantCommuteCompose J U).app (F.val.obj (Opposite.op t))).hom ((CategoryTheory.constantSheafAdj J B ht).counit.app ((CategoryTheory.sheafCompose J U).obj F)) = (CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J A ht).counit.app F)

theorem CategoryTheory.Sheaf.sheafCompose_reflects_discrete {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {B : Type u_3} [CategoryTheory.Category.{u_5, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J A) [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] [CategoryTheory.Sheaf.IsDiscrete J ht ((CategoryTheory.sheafCompose J U).obj F)] : CategoryTheory.Sheaf.IsDiscrete J ht F

instance CategoryTheory.Sheaf.instIsDiscreteObjSheafCompose {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_5, u_2} A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {B : Type u_3} [CategoryTheory.Category.{u_6, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J A) [h : CategoryTheory.Sheaf.IsDiscrete J ht F] : CategoryTheory.Sheaf.IsDiscrete J ht ((CategoryTheory.sheafCompose J U).obj F)

Equations

• ⋯ = ⋯

theorem CategoryTheory.Sheaf.isDiscrete_iff_forget {C : Type u_1} [CategoryTheory.Category.{u_6, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] {t : C} (ht : CategoryTheory.Limits.IsTerminal t) {B : Type u_3} [CategoryTheory.Category.{u_5, u_3} B] (U : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [(CategoryTheory.constantSheaf J A).Faithful] [(CategoryTheory.constantSheaf J A).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J A) [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] : CategoryTheory.Sheaf.IsDiscrete J ht F ↔ CategoryTheory.Sheaf.IsDiscrete J ht ((CategoryTheory.sheafCompose J U).obj F)