Background
Basic concepts
equivalences in/of $(\infty,1)$-categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
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}$. Dually, the full subcategory on $L$ is closed under (∞,1)-colimits that exist in $\mathcal{C}$.
In fact:
The full sub-$\infty$-category of the arrow category on the right class is a reflective sub-$\infty$-category
Moreover, the adjunction units $\eta_f \colon f \to \bar f$ are of the form
(In words: the reflection into $\big(\mathcal{C}^{\Delta[1]}\big)_R$ is given by the factorization in $(L,R)$.)
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 November 2, 2021 at 14:55:10. See the history of this page for a list of all contributions to it.