Ingo Blechschmidt, University of Augsburg

Revisiting divisible, injective and flabby abelian groups from a
constructive point of view

Following Hilbert's program, computing cohomology in concrete situations should
not require fixing a universe of sets first. Does it?

Foundational to the classical approach to cohomology is the result that every
abelian group embeds into an injective abelian group. The standard textbook
proof uses a criterion by Baer to connect injectivity with the more elementary
auxiliary notion of divisible groups and appeals to the transfinite by
employing both Zorn's lemma and the law of excluded middle, hence requires the
full power of the axiom of choice.

Can there be a more informative proof? Already in 1979, Andreas Blass analyzed
the dependence of this result on the axiom of choice and observed: No, it is
consistent with Zermelo–Fraenkel set theory that there are no nontrivial
injective abelian groups at all. However, his analysis was over ZF with its law
of excluded middle, hence couldn't be sensitive to the difference between
Zorn's lemma and the axiom of choice. The former is constructively neutral,
being valid in many models of constructive mathematics, while the latter is a
constructive taboo in view of entailing the law of excluded middle.

The talk recalls the motivation for these notions and then presents a refined
analysis: We show that, while there is an ample supply of divisible abelian
groups in constructive mathematics, they are deficient for the purposes of
obtaining injective groups. In view of this negative result, we study an
appropriate larger class of groups; constructively, every abelian group
canonically maps to a group of this kind, and assuming Zorn's lemma only, these
canonical maps are injective and groups of this kind are injective. The
construction relies on an intricate use of the powerset axiom and on
well-adapted modal operators.

As a result, the existence of enough injective abelian groups is constructively
neutral and is available in sheaf toposes over topological spaces and
locales, but does require fixing a universe of sets beforehand. The talk closes
with a proposed strategy resolving this issue and rendering cohomology
predicative.