nLab
Barr's theorem

Contents

Idea

Barr’s theorem was originally conjectured by William Lawvere as an infinitary generalization of the Deligne completeness theorem for coherent toposes which can be expressed as the existence of a surjection 𝒮/K\mathcal{S}/K\to\mathcal{E} for a coherent topos \mathcal{E} with set of points KK. General toposes \mathcal{E} may fail to have enough points but Michael Barr showed that a surjection from a suitable Boolean topos still exists.

As surjections permit the transfer of logical properties, Barr’s theorem has the following important consequence:

If a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in constructive mathematics.

The proof of Barr’s theorem itself, however, is highly non-constructive.

Statement

Theorem

If \mathcal{E} is a Grothendieck topos, then there is a surjective geometric morphism

\mathcal{F} \to \mathcal{E}

where \mathcal{F} satisfies the axiom of choice.

References

Extensive discussion of the context of Barr’s theorem is in chapter 7 of:

  • P. T. Johnstone, Topos Theory , Academic Press New York 1977 (Dover reprint 2014).

For a discussion of the importance of this theorem in constructive algebra see

  • Gavin Wraith, Intuitionistic algebra: some recent developments in topos theory In Proceedings of the International Congress of Mathematicians (Helsinki, 1978), pages 331–337, Helsinki, 1980. Acad. Sci. Fennica. (pdf)

See also the following MO discussion: (link)

Revised on October 30, 2014 18:57:17 by Thomas Holder (89.204.137.190)