equivalences in/of $(\infty,1)$-categories
Let $C$ be an (∞,1)-category and $f : A \to B$ and $g : X \to Y$ two morphisms in $C$. Write $C_{A\sslash Y}$ for the under-over-(∞,1)-category.
We say that $f$ is left orthogonal to $g$ and that $g$ is right orthogonal to $f$ and write
if for every commuting diagram
in $C$ we have that $C_{A\sslash Y}(B,X) \simeq *$ is contractible.
Note that the notation $C_{A\sslash Y}(B,X)$ subtly includes the given commuting diagram, since $C_{A\sslash Y}$ is only defined relative to a particular given morphism $A\to Y$. Here we take that to be the common composite of the given commuting square, with $B$ and $X$ regarded as objects of $C_{A\sslash Y}$ via the resulting commuting triangles.
Let $C$ be an (∞,1)-category. An orthogonal factorization system on $C$ is a pair $(S_L, S_R)$ of classes of morphisms in $C$ that satisfy the following axioms.
Both classes are stable under retracts.
Every morphism in $S_L$ is left orthogonal to every morphism in $S_R$;
For every morphism $h : X \to Z$ in $C$ there exists a commuting triangle
with $f \in S_L$ and $g \in S_R$.
For $(L,R)$ a factorization system in an (∞,1)-category $\mathcal{C}$, the full sub-(∞,1)-category of the arrow category $Func(\Delta^1, \mathcal{C})$ on the morphisms in $R$ is closed under (∞,1)-limits of shapes that exist in $\mathcal{C}$. Similarly the full subcategory on $L$ is closed under (∞,1)-colimits that exist in $\mathcal{C}$.
This is (Lurie, prop. 5.2.8.6 (7), (8)).
Let $(L,R)$ be an orthogonal factorization system on an $(\infty,1)$-category $\mathcal{C}$. Write $\mathcal{C}^I_R \hookrightarrow \mathcal{C}^I$ for the full sub-(∞,1)-category of the arrow category on the morphisms in $R$.
Then
this is a reflective sub-(∞,1)-category
The adjunction units $\eta_f : f \to \bar f$ are of the form
(In words: the reflection into $\mathcal{C}^I_R$ is given by the factorization in $(L,R)$).
This is (Lurie, lemma 5.2.8.19).
In an (∞,1)-topos the classe of n-connected and that of n-truncated morphisms form an orthogonal factorization system, for all $(-2) \leq n \leq \infty$.
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 January 28, 2019 at 01:52:57. See the history of this page for a list of all contributions to it.