Base change of a pullback square
ID: base-change-of-a-pullback-square
Given a pullback in a category and a morphism , assume the indicated pullbacks in a category exist. The four base-changed objects form a pullback in a category. A compatible pair of morphisms into and gives morphisms into and a common morphism into . The first two morphisms factor uniquely through , and their common image in permits unique factorization through . This proves the displayed canonical isomorphism without an assumption that the whole category is complete.
New to topics? Read the docs here!