We prove the orthogonality of final functors and discrete fibrations. For , finality supplies an object of . Lift through the discrete fibration , obtaining
If in the comma category, then , and is a lift of with codomain . Uniqueness of that lift makes its domain equal to . Thus ; since the comma category is a connected category, equality propagates along every zigzag. Define to be this common object.
For , choose . Lift into , obtaining . Then lifts into , so its domain is by the preceding construction. Define . The unique lifting property of a discrete fibration proves and , and gives .
At , use ; its lift is , so . Both and are lifts of with the same codomain, hence agree. Therefore .
If is another filling functor, its arrow is the same unique lift of , forcing . Its arrows are likewise forced by their codomains and images under . The diagonal functor exists and is unique.
Use the connected-component presheaf of a functor. For , define to have objects , where is a categorical connected component of . An arrow is an arrow such that , where precomposition induces . Identity and composition follow from precomposition, so this is a category.
The projection is a discrete fibration: the unique lift of with codomain has domain .
Define by
For , the objects and lie in the same component of , proving this is well-defined. Clearly .
For , the objects and arrows of are exactly the objects and arrows of the component of . Indeed, an arrow is with , and its commuting triangles are precisely those in the original comma category. This category is nonempty and connected. Hence is a final functor, proving the final-discrete-fibration factorization
Suppose are two final-discrete-fibration factorizations. Apply the orthogonality of final functors and discrete fibrations to the square with left side , top , bottom and right side . It gives a unique satisfying and . Reversing the roles gives .
Both and fill the same square for , so uniqueness gives ; similarly . This proves the uniqueness of a final-discrete-fibration factorization: the connecting functor is a canonical isomorphism, not just a noncanonical equivalence.

Articles by others on the same topic (0)

There are currently no matching articles.