Commit 2021-07-12 06:15 92d0dd89

feat(category_theory/limits): monomorphisms from initial (#8099) Defines a class for categories where every morphism from initial is a monomorphism. If the category has a terminal object, this is equivalent to saying the unique morphism from initial to terminal is a monomorphism, so this is essentially a "zero_le_one" for categories. I'm happy to change the name of this class! This axiom does not appear to have a common name, though it is (equivalent to) the second of Freyd's AT axioms: specifically it is a property shared by abelian categories and pretoposes. The main advantage to this class is that it is the precise condition required for the subobject lattice to have a bottom element, resolving the discussion here: https://github.com/leanprover-community/mathlib/pull/6278#discussion_r577702542 I've also made some minor changes to later parts of this file, essentially de-duplicating arguments, and moving the comparison section up so that all the results about terminal objects in index categories of limits are together rather than split in two.