Structure

Implication details

Claim: If a category is an elementary topos and has a generating collection, then it has a cogenerating collection.

Proof: For an elementary topos T\T, the power object functor P:Top→TP : \T^{\op} \to \T is right adjoint to Pop:T→TopP^{\op} : \T \to \T^{\op} and moreover is faithful. The first statement is part of the proof that PP is monadic (Johnstone, 2.2.7) and the second is a corollary. Therefore, from Lemma 9 here, if FF is a generating collection of T\T, then P∗(F)P_*(F) is a cogenerating collection.

This implication has a dual.

Show 18 categories using this implication