(Elementary) Sheaf Topos

We define a subobject classifier for categories of sheaves of (large enough) types.

Main definitions

Let C refer to a category with (when relevant) Grothendieck topology J.

• Presheaf.classifier C is a construction of a subobject classifier in Cᵒᵖ ⥤ Type (max u v).
• Sheaf.classifier J is a construction of a subobject classifier in Sheaf J (Type (max u v)).
• inferInstance : HasClassifier (Cᵒᵖ ⥤ Type w) says that Cᵒᵖ ⥤ Type w has a subobject classifier if C is w-essentially small.
• inferInstance : HasClassifier (Sheaf J (Type w)) says that Sheaf J (Type w) has a subobject classifier if C is w-essentially small.

Main results

• Any category of sheaves of types has a subobject classifier if the site is essentially small.
• As a consequence, (because categories of sheaves are cartesian monoidal and have finite limits,) such categories are Elementary Topoi.

TODOS:

• generalize Presheaf.isClosed_χ_app_apply_of to only assuming G is separated

def CategoryTheory.Presheaf.truth (C : Type u) [Category.{v, u} C] : (Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1} ⟶ Functor.sieves C

The truth morphism in the category of presheaves. At each component X : C, it is the constant map returning ⊤ : Sieve X.

Equations

• CategoryTheory.Presheaf.truth C = { app := fun (X : Cᵒᵖ) (x : ((CategoryTheory.Functor.const Cᵒᵖ).obj PUnit.{(max ?u.19 ?u.20) + 1}).obj X) => ⊤, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Presheaf.truth_app (C : Type u) [Category.{v, u} C] (X : Cᵒᵖ) (x✝ : ((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X) : (truth C).app X x✝ = ⊤

def CategoryTheory.Presheaf.χ {C : Type u} [Category.{v, u} C] {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) : G ⟶ Functor.sieves C

The characteristic map of an inclusion of presheaves. Given a monomorphism of sheaves m : F ⟶ G, an object X of the site, map an element x : G(X) to the (closed) sieve on X where f : Y → X is in the sieve iff ∃ a ∈ F(Y), G(f)(x) = m_Y(a)

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.χ_app {C : Type u} [Category.{v, u} C] {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) (X : Cᵒᵖ) (x : G.obj X) : (χ m).app X x = { arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) => ∃ (a : F.obj (Opposite.op Y)), G.map f.op x = m.app (Opposite.op Y) a, downward_closed := ⋯ }

theorem CategoryTheory.Presheaf.comp_χ_eq {C : Type u} [Category.{v, u} C] {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) : CategoryStruct.comp m (χ m) = CategoryStruct.comp ((Functor.isTerminalConst Cᵒᵖ Limits.Types.isTerminalPUnit).from F) (truth C)

theorem CategoryTheory.Presheaf.isPullback_χ_truth {C : Type u} [Category.{v, u} C] {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) [Mono m] : IsPullback m ((Functor.isTerminalConst Cᵒᵖ Limits.Types.isTerminalPUnit).from F) (χ m) (truth C)

theorem CategoryTheory.Presheaf.χ_unique {C : Type u} [Category.{v, u} C] {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) (χ' : G ⟶ Functor.sieves C) (hχ' : IsPullback m ((Functor.isTerminalConst Cᵒᵖ Limits.Types.isTerminalPUnit).from F) χ' (truth C)) : χ' = χ m

def CategoryTheory.Presheaf.classifier (C : Type u) [Category.{v, u} C] : Classifier (Functor Cᵒᵖ (Type (max u v)))

A construction of a subject classifier in a category of presheaves.

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.classifier_truth (C : Type u) [Category.{v, u} C] : (classifier C).truth = truth C

@[simp]

theorem CategoryTheory.Presheaf.classifier_χ (C : Type u) [Category.{v, u} C] {U✝ X✝ : Functor Cᵒᵖ (Type (max u v))} (m : U✝ ⟶ X✝) (x✝ : Mono m) : (classifier C).χ m = χ m

@[simp]

theorem CategoryTheory.Presheaf.classifier_Ω₀ (C : Type u) [Category.{v, u} C] : (classifier C).Ω₀ = (Functor.const Cᵒᵖ).obj PUnit.{max (u + 1) (v + 1)}

@[simp]

theorem CategoryTheory.Presheaf.classifier_χ₀ (C : Type u) [Category.{v, u} C] (Y : Functor Cᵒᵖ (Type (max u v))) : (classifier C).χ₀ Y = (Functor.isTerminalConst Cᵒᵖ Limits.Types.isTerminalPUnit).from Y

@[simp]

theorem CategoryTheory.Presheaf.classifier_Ω (C : Type u) [Category.{v, u} C] : (classifier C).Ω = Functor.sieves C

instance CategoryTheory.instHasClassifierFunctorOppositeTypeOfEssentiallySmall {C : Type u} [Category.{v, u} C] [EssentiallySmall.{w, v, u} C] : HasClassifier (Functor Cᵒᵖ (Type w))

Presheaf categories on an essentially small domain have a subobject classifier.

theorem CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) [Mono m] (hF : Presieve.IsSheaf J F) (hG : Presieve.IsSeparated J G) (X : Cᵒᵖ) (x : G.obj X) : J.IsClosed ((Presheaf.χ m).app X x)

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

The sheaf of closed sieves w/r/t J. See also Functor.closedSieves and Sheaf.classifier

Equations

• CategoryTheory.Sheaf.Ω J = { obj := (CategoryTheory.Functor.closedSieves J).toFunctor, property := ⋯ }

@[simp]

theorem CategoryTheory.Sheaf.Ω_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : (Ω J).obj = (Functor.closedSieves J).toFunctor

def CategoryTheory.Sheaf.truth {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : terminal J Limits.Types.isTerminalPUnit ⟶ Ω J

The morphism t : 1 ⟶ Ω which picks out the maximal sieve

Equations

• CategoryTheory.Sheaf.truth J = { hom := CategoryTheory.Subfunctor.lift (CategoryTheory.Presheaf.truth C) ⋯ }

@[simp]

theorem CategoryTheory.Sheaf.truth_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : (truth J).hom = Subfunctor.lift (Presheaf.truth C) ⋯

def CategoryTheory.Sheaf.χ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))} (m : F ⟶ G) [Mono m] : G ⟶ Ω J

Given a monomorphism of sheaves η : F ⟶ G, an object X of the site, map an element x : G(X) to the (closed) sieve on X where f : Y → X is in the sieve iff ∃ a ∈ F(Y), G(f)(x) = η_Y(a)

Equations

• CategoryTheory.Sheaf.χ m = { hom := CategoryTheory.Subfunctor.lift (CategoryTheory.Presheaf.χ m.hom) ⋯ }

@[simp]

theorem CategoryTheory.Sheaf.χ_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))} (m : F ⟶ G) [Mono m] : (χ m).hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯

theorem CategoryTheory.Sheaf.isPullback_χ_truth {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))} (m : F ⟶ G) [Mono m] : IsPullback m ((isTerminalTerminal J Limits.Types.isTerminalPUnit).from F) (χ m) (truth J)

theorem CategoryTheory.Sheaf.χ_unique {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type (max u v))} (m : F ⟶ G) [Mono m] (χ' : G ⟶ Ω J) (hχ' : IsPullback m ((isTerminalTerminal J Limits.Types.isTerminalPUnit).from F) χ' (truth J)) : χ' = χ m

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

A construction of a subobject classifier for sheaf categories. Ω is the sheaf of closed sieves, and truth maps for each object X : C, an element of PUnit to the maximal Sieve X, which is always closed.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.classifier_truth {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : (classifier J).truth = truth J

@[simp]

theorem CategoryTheory.Sheaf.classifier_χ₀ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (Y : Sheaf J (Type (max u v))) : (classifier J).χ₀ Y = (isTerminalTerminal J Limits.Types.isTerminalPUnit).from Y

@[simp]

theorem CategoryTheory.Sheaf.classifier_Ω {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : (classifier J).Ω = Ω J

@[simp]

theorem CategoryTheory.Sheaf.classifier_χ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {U✝ X✝ : Sheaf J (Type (max u v))} (m : U✝ ⟶ X✝) (x✝ : Mono m) : (classifier J).χ m = χ m

@[simp]

theorem CategoryTheory.Sheaf.classifier_Ω₀ {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : (classifier J).Ω₀ = terminal J Limits.Types.isTerminalPUnit

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

Sheaf categories on essentially small sites have a subobject classifier.