Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
Let be an (∞,1)-category and and two morphisms in . Write for the under-over-(∞,1)-category.
We say that is left orthogonal to and that is right orthogonal to and write
if for every commuting diagram
in we have that is contractible.
Note that the notation subtly includes the given commuting diagram, since is only defined relative to a particular given morphism . Here we take that to be the common composite of the given commuting square, with and regarded as objects of via the resulting commuting triangles.
Let be an (∞,1)-category. An orthogonal factorization system on is a pair of classes of morphisms in that satisfy the following axioms.
Both classes are stable under retracts.
Every morphism in is left orthogonal to every morphism in ;
For every morphism in there exists a commuting triangle
with and .
For a factorization system in an (∞,1)-category , the full sub-(∞,1)-category of the arrow category on the morphisms in is closed under (∞,1)-limits of shapes that exist in . Dually, the full subcategory on is closed under (∞,1)-colimits that exist in .
In fact:
The full sub--category of the arrow category on the right class is a reflective sub--category
Moreover, the adjunction units are of the form
(In words: the reflection into is given by the factorization in .)
In an (∞,1)-topos the classe of n-connected and that of n-truncated morphisms form an orthogonal factorization system, for all .
factorization system in an (∞,1)-category
orthogonal factorization system in an (∞,1)-category
Section 5.2.8 of
Formalization in homotopy type theory is discussed in
Last revised on November 2, 2021 at 14:55:10. See the history of this page for a list of all contributions to it.