Elementary toposes

DefinitionElementary topos#✓fully proved

A category \(E\) is an elementary topos if it has all finite limits, it admits a cartesian monoidal structure for which it is monoidal closed (that is, \(E\) is cartesian closed), and it has a subobject classifier.

def IsTopos (E : Type*) [Category E] : Prop :=
  HasFiniteLimits E ∧
  ∃ cm : CartesianMonoidalCategory E,
    (letI : MonoidalCategory E := cm.toMonoidalCategory
     Nonempty (MonoidalClosed E)) ∧
    HasSubobjectClassifier E

Used by 1

Used byFundamental theorem of topos theory

TheoremFundamental theorem of topos theory#●ready to prove

If \(E\) is an elementary topos and \(X\) is an object of \(E\), then the slice category \(E/X\) of objects of \(E\) over \(X\) is again an elementary topos.

public theorem_wanted fundamental_topos_theory {E : Type*} [Category E]
    (hE : IsTopos E) (X : E) : IsTopos (Over X)

Sources

• F. W. Lawvere & M. Tierney (elementary topos, 1970); see S. Mac Lane & I. Moerdijk, Sheaves in Geometry and Logic, IV.7. Knill, Some fundamental theorems in mathematics, §54. Problem fundamental_topos_theory of the lean-eval benchmark.

Uses 1

Statement usesElementary topos

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.