module Elephant where

Sketching the elephant🔗

Though the 1Lab is not purely a formalization of category theory, it does aim to be a useful reference on the subject. However, the 1Lab organizes content in a highly non-linear fashion; this can make it somewhat difficult to use as a companion to more traditional resources.

This page attempts to (somewhat) rectify this situation by gathering all of the results from “Sketches of an Elephant – A Topos Theory Compendium” (Johnstone 2002) in a single place.¹

A. Toposes as categories🔗

A1 Regular and cartesian closed categories🔗

A1.1 Preliminary assumptions🔗

• Lemma 1.1.1: FG-iso→is-reflective
• Lemma 1.1.2: crude-monadicity
• Lemma 1.1.4: lambek
• Proposition 1.1.7: ∫
• Lemma 1.1.8: Karoubi-is-completion

A1.2 Cartesian Categories🔗

• Lemma 1.2.1:
  1. Finitely-complete→is-finitely-complete
  2. with-equalisers
  3. with-pullbacks

A1.3 Regular Categories🔗

• Proposition 1.3.4: is-strong-epi→is-regular-epi
• Definition 1.3.6: is-congruence

A1.4 Coherent Categories🔗

A1.5 Cartesian closed categories🔗

• Lemma 1.5.2:
  1. (⇐) exponentiable→constant-family⊣product
• Corollary 1.5.3: (⇒) dependent-product→lcc (⇐) lcc→dependent-product

A1.6 Subobject classifiers🔗

C Toposes as spaces🔗

C2 Sheaves on a site🔗

C2.1 Sites and coverages🔗

• Definition 2.1.1: Coverage
• Definition 2.1.2:
  • Compatible families: Patch
  • Separated presheaves: is-separated₁
  • Sheaves on a site: is-sheaf, is-separated
• Lemma 2.1.5: is-sheaf-maximal
• Lemma 2.1.6: is-sheaf-factor
• Lemma 2.1.7: is-sheaf-transitive, though see the warning there.
• Example 2.1.12, (universally) effective-epimorphic sieves: is-colim, is-universal-colim

C2.2 The topos of sheaves🔗

See topos of sheaves.

• Proposition 2.2.6:
  • Reflectivity: Sheafification-is-reflective
  • Completeness: Sh[]-is-complete
  • Cocompleteness: Sh[]-is-cocomplete
  • Cartesian closure: Sh[]-cc