Subobject classifiers in categories of sheaves

In this file we construct a subobject classifier in the category of sheaves of types on any site, as the sheaf that sends every object to the set of closed sieves on it. See https://ncatlab.org/nlab/show/subobject+classifier#in_a_sheaf_topos.

For Grothendieck topologies J ≤ K we also construct comparison maps between the corresponding subobject classifiers, both viewed as J-sheaves.

Main definitions / results

• ClosedSieve J X: the type of J-closed sieves on X
• J.Ω: the J-sheaf sending each X to the type of J-closed sieves on X
• J.classifier: the data making J.Ω into a subobject classifier
• J.Ω' h: K.Ω as a J-sheaf for h : J ≤ K
• J.ΩInclusionOfLE h: the inclusion J.Ω' h ⟶ J.Ω for h : J ≤ K
• J.ΩProjectionOfLE h: the projection J.Ω ⟶ J.Ω' h for h : J ≤ K

def CategoryTheory.Sieve.IsClosed {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {X : C} (S : Sieve X) : Prop

A sieve is called J-closed if it contains every morphism along which it pulls back to a J-covering sieve, i.e. if it contains every morphism it covers.

Equations

• CategoryTheory.Sieve.IsClosed J S = ∀ (Y : C) (f : Y ⟶ X), CategoryTheory.Sieve.pullback f S ∈ J Y → S.arrows f

theorem CategoryTheory.Sieve.IsClosed.pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} {S : Sieve X} (hS : IsClosed J S) {Y : C} (f : Y ⟶ X) : IsClosed J (Sieve.pullback f S)

theorem CategoryTheory.Sieve.IsClosed.anti {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} {S : Sieve X} (hS : IsClosed K S) : IsClosed J S

structure CategoryTheory.ClosedSieve {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (X : C) extends CategoryTheory.Sieve X : Type (max u v)

A sieve on X that is J-closed in the sense of Sieve.IsClosed, i.e. that contains every morphism along which it pulls back to a J-covering sieve.

• arrows : Presieve X
• downward_closed {Y Z : C} {f : Y ⟶ X} : self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryStruct.comp g f)
• isClosed : Sieve.IsClosed J self.toSieve

theorem CategoryTheory.ClosedSieve.ext {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S T : ClosedSieve J X) : S.toSieve = T.toSieve → S = T

theorem CategoryTheory.ClosedSieve.ext_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} {S T : ClosedSieve J X} : S = T ↔ S.toSieve = T.toSieve

theorem CategoryTheory.ClosedSieve.injective_toSieve {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} : Function.Injective toSieve

instance CategoryTheory.ClosedSieve.instPartialOrder {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} : PartialOrder (ClosedSieve J X)

Equations

• CategoryTheory.ClosedSieve.instPartialOrder = PartialOrder.lift CategoryTheory.ClosedSieve.toSieve ⋯

theorem CategoryTheory.ClosedSieve.le_def {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} {S T : ClosedSieve J X} : S ≤ T ↔ S.toSieve ≤ T.toSieve

def CategoryTheory.ClosedSieve.generate {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {X : C} (S : Sieve X) : ClosedSieve J X

The smallest J-closed sieve containing a given sieve S : Sieve X, given by all morphisms f : Y ⟶ X along which S pulls back to a covering sieve, i.e. "all morphisms that S covers".

Equations

• CategoryTheory.ClosedSieve.generate J S = { arrows := fun (Y : C) (f : Y ⟶ X) => CategoryTheory.Sieve.pullback f S ∈ J Y, downward_closed := ⋯, isClosed := ⋯ }

@[simp]

theorem CategoryTheory.ClosedSieve.generate_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {X : C} (S : Sieve X) (Y : C) (f : Y ⟶ X) : (generate J S).arrows f = (Sieve.pullback f S ∈ J Y)

theorem CategoryTheory.ClosedSieve.generate_le_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : Sieve X) (T : ClosedSieve J X) : generate J S ≤ T ↔ S ≤ T.toSieve

theorem CategoryTheory.ClosedSieve.le_toSieve_generate {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : Sieve X) : S ≤ (generate J S).toSieve

def CategoryTheory.ClosedSieve.giGenerate {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} : GaloisInsertion (generate J) toSieve

The Galois insertion given by ClosedSieve.generate : Sieve X → ClosedSieve J X.

Equations

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

@[simp]

theorem CategoryTheory.ClosedSieve.generate_toSieve {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : ClosedSieve J X) : generate J S.toSieve = S

instance CategoryTheory.ClosedSieve.instCompleteLattice {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} : CompleteLattice (ClosedSieve J X)

Equations

• CategoryTheory.ClosedSieve.instCompleteLattice = CategoryTheory.ClosedSieve.giGenerate.liftCompleteLattice

def CategoryTheory.ClosedSieve.pullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X Y : C} (f : Y ⟶ X) (S : ClosedSieve J X) : ClosedSieve J Y

Equations

• CategoryTheory.ClosedSieve.pullback f S = { toSieve := CategoryTheory.Sieve.pullback f S.toSieve, isClosed := ⋯ }

@[simp]

theorem CategoryTheory.ClosedSieve.pullback_toSieve {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X Y : C} (f : Y ⟶ X) (S : ClosedSieve J X) : (pullback f S).toSieve = Sieve.pullback f S.toSieve

@[simp]

theorem CategoryTheory.ClosedSieve.pullback_id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : ClosedSieve J X) : pullback (CategoryStruct.id X) S = S

theorem CategoryTheory.ClosedSieve.pullback_comp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : ClosedSieve J X) {Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} : pullback (CategoryStruct.comp g f) S = pullback g (pullback f S)

theorem CategoryTheory.ClosedSieve.pullback_monotone {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X Y : C} {f : Y ⟶ X} : Monotone (pullback f)

theorem CategoryTheory.ClosedSieve.pullback_generate {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) : pullback f (generate J S) = generate J (Sieve.pullback f S)

def CategoryTheory.ClosedSieve.inclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} (S : ClosedSieve K X) : ClosedSieve J X

The inclusion of K-closed sieves into J-closed sieves for J ≤ K.

Equations

• CategoryTheory.ClosedSieve.inclusionOfLE h S = { toSieve := S.toSieve, isClosed := ⋯ }

@[simp]

theorem CategoryTheory.ClosedSieve.inclusionOfLE_toSieve {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} (S : ClosedSieve K X) : (inclusionOfLE h S).toSieve = S.toSieve

def CategoryTheory.ClosedSieve.toClosedSieve {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (K : GrothendieckTopology C) {X : C} (S : ClosedSieve J X) : ClosedSieve K X

The K-closed sieve generated by the sieve underlying a J-closed sieve. For J ≤ K, this is left adjoint to inclusionOfLE : ClosedSieve K X → ClosedSieve J X.

Equations

• CategoryTheory.ClosedSieve.toClosedSieve K S = CategoryTheory.ClosedSieve.generate K S.toSieve

@[simp]

theorem CategoryTheory.ClosedSieve.toClosedSieve_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (K : GrothendieckTopology C) {X : C} (S : ClosedSieve J X) (Y : C) (f : Y ⟶ X) : (toClosedSieve K S).arrows f = (Sieve.pullback f S.toSieve ∈ K Y)

theorem CategoryTheory.ClosedSieve.toClosedSieve_le_iff_le_inclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} (S : ClosedSieve J X) (T : ClosedSieve K X) : toClosedSieve K S ≤ T ↔ S ≤ inclusionOfLE h T

theorem CategoryTheory.ClosedSieve.le_inclusionOfLE_toClosedSieve {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} (S : ClosedSieve J X) : S ≤ inclusionOfLE h (toClosedSieve K S)

def CategoryTheory.ClosedSieve.giInclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} : GaloisInsertion (toClosedSieve K) (inclusionOfLE h)

The galois insertion given by inclusionOfLE h : ClosedSieve K X → ClosedSieve J X.

Equations

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

@[simp]

theorem CategoryTheory.ClosedSieve.toClosedSieve_inclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X : C} (S : ClosedSieve K X) : toClosedSieve K (inclusionOfLE h S) = S

def CategoryTheory.GrothendieckTopology.Ω {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Sheaf J (Type (max u v))

A specific choice of subobject classifier in the sheaf topos Sheaf J (Type max u v): the sheaf that associates to each X : C the type of all J-closed sieves on X. The data that makes this a subobject classifier can be found in GrothendieckTopology.classifier.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.Ω_val_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (X : Cᵒᵖ) : J.Ω.val.obj X = ClosedSieve J (Opposite.unop X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Ω_val_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (S : ClosedSieve J (Opposite.unop X✝)) : J.Ω.val.map f S = ClosedSieve.pullback f.unop S

theorem CategoryTheory.Subpresheaf.isSheaf_range {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F F' : Sheaf J (Type w)} (f : F ⟶ F') [Mono f] : Presieve.IsSheaf J (range f.val).toPresheaf

theorem CategoryTheory.Subpresheaf.sieveOfSection_eq_top_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {U : Cᵒᵖ} {s : F.obj U} : G.sieveOfSection s = ⊤ ↔ s ∈ G.obj U

theorem CategoryTheory.Subpresheaf.pullback_sieveOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {U V : Cᵒᵖ} (f : U ⟶ V) (s : F.obj U) : Sieve.pullback f.unop (G.sieveOfSection s) = G.sieveOfSection (F.map f s)

theorem CategoryTheory.Subpresheaf.isClosed_sieveOfSection {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F : Functor Cᵒᵖ (Type w)} (hF : Presieve.IsSheaf J F) {G : Subpresheaf F} (hG : Presieve.IsSheaf J G.toPresheaf) {U : Cᵒᵖ} (s : F.obj U) : Sieve.IsClosed J (G.sieveOfSection s)

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalObj_functor {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasLimits D] {F : Functor C D} (hF : IsTerminal F) (X : C) : IsTerminal (F.obj X)

Evaluating a terminal functor yields terminal objects. TODO: move somewhere else

Equations

• hF.isTerminalObj_functor X = CategoryTheory.Limits.IsTerminal.isTerminalObj ((CategoryTheory.evaluation C D).obj X) F hF

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalSheafVal {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasLimits A] {X : Sheaf J A} (hX : IsTerminal X) : IsTerminal X.val

A terminal sheaf is also terminal as a presheaf.

Equations

• hX.isTerminalSheafVal = CategoryTheory.Limits.IsTerminal.isTerminalObj (CategoryTheory.sheafToPresheaf J A) X hX

noncomputable def CategoryTheory.Limits.IsTerminal.isTerminalSheafValObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [HasLimits A] {X : Sheaf J A} (hX : IsTerminal X) (Y : Cᵒᵖ) : IsTerminal (X.val.obj Y)

Sections of a terminal sheaf are terminal objects.

Equations

• hX.isTerminalSheafValObj Y = hX.isTerminalSheafVal.isTerminalObj_functor Y

noncomputable instance CategoryTheory.Sheaf.instUniqueTerminalValObjForget {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u₂} [Category.{v₂, u₂} A] [Limits.HasLimits A] [HasForget A] [Limits.PreservesLimit (Functor.empty A) (forget A)] (Y : Cᵒᵖ) : Unique ((forget A).obj ((⊤_ Sheaf J A).val.obj Y))

For sheaves valued in a concrete category whose terminal object is a point, sections of the terminal sheaf are unique.

Equations

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

noncomputable def CategoryTheory.Limits.IsTerminal.unique {X : Type u} (h : IsTerminal X) : Unique X

Terminal types are singletons.

Equations

• h.unique = (CategoryTheory.Limits.Types.isTerminalEquivUnique X) h

noncomputable instance CategoryTheory.Sheaf.instUniqueTerminalValObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Y : Cᵒᵖ) : Unique ((⊤_ Sheaf J (Type w)).val.obj Y)

Sections of the terminal sheaf are unique.

Equations

• CategoryTheory.Sheaf.instUniqueTerminalValObj Y = (CategoryTheory.Limits.terminalIsTerminal.isTerminalSheafValObj Y).unique

noncomputable def CategoryTheory.GrothendieckTopology.classifier {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Classifier (Sheaf J (Type (max u v)))

A specific choice of subobject classifier in the sheaf topos Sheaf J (Type max u v), given by J.Ω and the morphism ⊤_ C ⟶ J.Ω that picks the maximal sieve on each object.

Equations

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

instance CategoryTheory.GrothendieckTopology.hasClassifier {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : HasClassifier (Sheaf J (Type (max u v)))

theorem CategoryTheory.Presheaf.isSheaf_of_le {C : Type u} [Category.{v, u} C] {A : Type u₂} [Category.{v₂, u₂} A] {P : Functor Cᵒᵖ A} {J K : GrothendieckTopology C} (h : J ≤ K) (hP : IsSheaf K P) : IsSheaf J P

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

The subobject classifier sheaf K.Ω : Sheaf K (Type max u v) as a J-sheaf for J ≤ K.

Equations

• CategoryTheory.GrothendieckTopology.Ω' h = { val := K.Ω.val, cond := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Ω'_val_obj {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) (X : Cᵒᵖ) : (GrothendieckTopology.Ω' h).val.obj X = ClosedSieve K (Opposite.unop X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Ω'_val_map_apply {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (S : ClosedSieve K (Opposite.unop X✝)) (x✝ : C) (sl : x✝ ⟶ Opposite.unop Y✝) : ((GrothendieckTopology.Ω' h).val.map f S).arrows sl = S.arrows (CategoryStruct.comp sl f.unop)

def CategoryTheory.GrothendieckTopology.ΩInclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) : GrothendieckTopology.Ω' h ⟶ J.Ω

The inclusion of J.Ω' h, the subobject classifier of K-sheaves viewed as a J-sheaf, into J.Ω, the subobject classifier of J-sheaves. In components this is simply the inclusion of K-closed sieves into J-closed sieves.

Equations

• CategoryTheory.GrothendieckTopology.ΩInclusionOfLE h = { val := { app := fun (X : Cᵒᵖ) => CategoryTheory.ClosedSieve.inclusionOfLE h, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.GrothendieckTopology.ΩInclusionOfLE_val_app {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) (X : Cᵒᵖ) (S : ClosedSieve K (Opposite.unop X)) : (ΩInclusionOfLE h).val.app X S = ClosedSieve.inclusionOfLE h S

def CategoryTheory.GrothendieckTopology.ΩProjectionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) : J.Ω ⟶ GrothendieckTopology.Ω' h

The projection of J.Ω, the subobject classifier of J-sheaves, onto J.Ω' h, the subobject classifier of K-sheaves viewed as a J-sheaf. In components this generates K-closed sieves from J-closed sieves.

Equations

• CategoryTheory.GrothendieckTopology.ΩProjectionOfLE h = { val := { app := fun (X : Cᵒᵖ) => CategoryTheory.ClosedSieve.toClosedSieve K, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.GrothendieckTopology.ΩProjectionOfLE_val_app {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) (X : Cᵒᵖ) (S : ClosedSieve J (Opposite.unop X)) : (ΩProjectionOfLE h).val.app X S = ClosedSieve.toClosedSieve K S

@[simp]

theorem CategoryTheory.GrothendieckTopology.ΩInclusionOfLE_comp_ΩProjectionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) : CategoryStruct.comp (ΩInclusionOfLE h) (ΩProjectionOfLE h) = CategoryStruct.id (GrothendieckTopology.Ω' h)

instance CategoryTheory.GrothendieckTopology.instMonoSheafTypeΩInclusionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) : Mono (ΩInclusionOfLE h)

instance CategoryTheory.GrothendieckTopology.instEpiSheafTypeΩProjectionOfLE {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) : Epi (ΩProjectionOfLE h)