Effective epimorphisms detected on zero-truncation
Lemma 3.13. (Key lemma)
Let \(T\) be a topos.
The map \(X \to \tau_0 X\) is an effective epimorphism for every \(X \in T\).
A morphism \(f\colon Y \to X\) is an effective epimorphism if and only if the map \(\tau_0 Y \to \tau_0 X\) is an effective epimorphism.
Proof
(1) Factor the map \(X \to \tau_0 X\) into an effective epimorphism followed by a monomorphism:
\[X \twoheadrightarrow U \hookrightarrow \tau_0 X.\]
We must show that the second map is an isomorphism. Since it is a monomorphism (\((-1)\)-truncated) and \(\tau_0 X\) is \(0\)-truncated, Lemma 3.7 implies that \(U\) is also \(0\)-truncated.
More explicitly, the terminal map \(\tau_0 X \to *\) is \(0\)-truncated, while the monomorphism \(U \to \tau_0 X\) is \((-1)\)-truncated and hence also \(0\)-truncated. Part (1) of Lemma 3.7, applied to \(U \to \tau_0 X \to *\), therefore shows that \(U \to *\) is \(0\)-truncated.
In the notation of that lemma, take \(f\colon U \to \tau_0 X\), \(g\colon \tau_0 X \to *\), and \(n=0\). Since both \(f\) and \(g\) are \(0\)-truncated, the implication from the truncatedness of \(f\) to that of \(gf\) says exactly that \(U\) is \(0\)-truncated.
By definition, \(\tau_0 X\) is the initial \(0\)-truncated object equipped with a map from \(X\). Therefore the map \(U \hookrightarrow \tau_0 X\) admits a section \(\tau_0 X \to U\).
Writing \(\eta_X\colon X \to \tau_0 X\) for the unit, the effective epimorphism \(X \to U\) factors uniquely through \(\eta_X\) because \(U\) is \(0\)-truncated. This gives \(s\colon \tau_0 X \to U\). The endomorphisms \(ms\) and \(\id_{\tau_0 X}\) agree after precomposition with \(\eta_X\), so the same universal property gives \(ms=\id_{\tau_0 X}\).
Reflection into \(T_{\leq 0}\) gives an equivalence \(\Hom_T(\tau_0 X,U) \iso \Hom_T(X,U)\) for every \(0\)-truncated object \(U\). The section is the unique inverse image of \(X \to U\) under this equivalence.
This is the universal property of truncation used throughout the discussion of truncation and connectivity in Lurie (2009, Chapters 6 and 7).
In particular, it is an isomorphism by Corollary 2.39.(2) The “only if” direction is clear from the commutative diagram: Indeed, by part (1) the map \(X \to \tau_0 X\) is an effective epimorphism. If \(f\) is also an effective epimorphism, then so is the composite \(Y \to \tau_0 X\) by Lemma 2.37. Then \(\tau_0 Y \to \tau_0 X\) is also an effective epimorphism by Lemma 2.40.
Naturality of the unit gives \(\eta_X f=(\tau_0 f)\eta_Y\). Thus the effective epimorphism \(Y \to \tau_0 X\) factors as \(Y \to \tau_0 Y \xrightarrow{\tau_0 f} \tau_0 X\), and cancellation applies to this factorization.
Conversely, assume that \(\tau_0 f\) is an effective epimorphism. Consider the epi–mono factorization \(Y \twoheadrightarrow U \hookrightarrow X\) of \(f\) and the induced diagram By Lemma 3.12, the map \(\tau_0 U \to \tau_0 X\) is again a monomorphism, and the right-hand square is a pullback square. Since the composite \(\tau_0 Y \to \tau_0 U \to \tau_0 X\) is an effective epimorphism by assumption, Lemma 2.40 implies that \(\tau_0 U \to \tau_0 X\) is an effective epimorphism.
Here functoriality identifies the displayed composite with \(\tau_0 f=(\tau_0 i)(\tau_0 e)\), where \(i\colon U \hookrightarrow X\) is the monomorphism in the factorization of \(f\). Cancellation is applied before the mono-plus-effective-epi criterion.
The hypothesis says that the composite \(\tau_0 f\) is an effective epimorphism, not immediately that its second factor \(\tau_0 i\) is one. The latter conclusion is exactly the content supplied by Lemma 2.40.
Since it is also a monomorphism, it is an isomorphism by Corollary 2.39. Since the right-hand square is a pullback square, \(U \to X\) is also an isomorphism, as desired.
Indeed, pullbacks preserve isomorphisms, and \(U \to X\) is the pullback of \(\tau_0 U \to \tau_0 X\).
Claim.
The pullback of an isomorphism is an isomorphism.
An inverse to the lower horizontal map pulls back to a morphism \(X \to U\). The two inverse identities follow from the uniqueness clause in the pullback universal property.
References
Jacob Lurie. Higher topos theory. Ann. Math. Stud. 170, Princeton, NJ: Princeton University Press. 2009.
