A monomorphism is a left-cancellable morphism. A strong monomorphism has the right lifting property against every epimorphism: from a commutative square
with epic, one obtains satisfying and . A regular monomorphism is an equalizer of a parallel pair.
Suppose equalizes . In the square above,
Since is epic, , so the universal property of the equalizer gives the required . Thus every regular monomorphism is strong.
Let be strong for , and let . Given a lifting square against , compose its top map with each projection. Strength of produces maps with . The pair has equal composites to , hence induces . Therefore intersections of strong subobjects are strong.
Call a morphism anodyne when it is both monic and epic, and call an object saturated when it is injective with respect to every such morphism. Let be a strong subobject of a saturated object. Given an anodyne and , saturation of extends to some . Strength of applied to lifts to with . Hence is saturated.
Now embed as a subobject of a saturated object . Since the category is well-powered, the strong subobjects of through which factors form a set; completeness supplies their intersection . The same coordinatewise lifting argument used for two factors shows that is strong, so is saturated.
The induced map is monic. To prove it epic, let satisfy . Their equalizer is regular and hence strong. Composites of strong monomorphisms are strong, so is a strong subobject containing . Minimality of the intersection forces to factor through , which implies . Thus is epic and therefore anodyne.
For every saturated , each map extends across to a map . This extension is unique because is epic. Consequently is left adjoint to the inclusion of saturated objects: the full subcategory is reflective. This is the saturated reflection from a strong-subobject intersection.
It remains to prove that is balanced. First let be epic in . If are morphisms in the ambient category, embed into a saturated object . Equality then implies equality after composing with ; epicity in the full subcategory gives equality there, and monicity of gives . Thus is epic in the ambient category.
If is also monic in , it is monic in the ambient category as well. Indeed, for with , reflect by an anodyne map . Saturation extends and to ; ambient epicity of and monicity of inside give , hence . Therefore is anodyne in the ambient category. Saturation of extends across to a retraction . Since is epic, implies , so is an isomorphism. Hence is balanced.