Power object of a subobject

ID: power-object-of-a-subobject

For a monomorphism in a Cartesian category, intersect the universal membership relation on with . The resulting subobject is classified by , and . The equalizer of and the identity represents precisely families of subobjects of contained in , hence is a power object for . This construction only requires the power object of and finite limits.

New to topics? Read the docs here!