For an elementary topos, existence of products in a category indexed by a fixed set is equivalent to existence of the corresponding coproducts in a category. The power-object monadicity equivalence gives the forward direction because Eilenberg-Moore categories create limits. For the converse, the diagonal into the pointwise product category is a logical functor. A coproduct is its left adjoint; the adjoint lifting theorem for monad algebra functors, applied through power-object monadicity, then gives its right adjoint, namely the product. The required reflexive coequalizers on the algebra side are opposites of finite equalizers in the topos.
Articles by others on the same topic
There are currently no matching articles.