4
$\begingroup$

Let $\mathfrak{X}$ be an $\infty$-topos and let $f\colon X\to Y$ be a morphism of $\mathfrak{X}$. We say that $f$ is a monomorphism if it is $(-1)$-truncated which means that for every $Z\in\mathfrak{X}$ the induced morphism on mapping spaces $f_\ast\colon\mathfrak{X}(Z,X)\to\mathfrak{X}(Z,Y)$ is a $(-1)$-truncated map of spaces, which means that its fibers are all either empty or contractible (equivalently, it means that $f_\ast$ induces an injection on $\pi_0$ and an isomorphism on $\pi_k$, for any basepoint, when $k>0$).

An object $W\in \mathfrak{X}$ is called $n$-truncated if $\mathfrak{X}(Z,W)$ is an $n$-truncated space for all $Z\in\mathfrak{X}$, i.e. $\pi_k(\mathfrak{X}(Z,W))\cong 0$ for all $k>n$. The inclusion of the full subcategory of such objects $i\colon \tau_{\leq n}\mathfrak{X}\hookrightarrow\mathfrak{X}$ has a left adjoint called the truncation functor, $\tau_{\leq n}\colon \mathfrak{X}\to\tau_{\leq n}\mathfrak{X}$.

The question is:

Is it true that if $f\colon X\to Y$ is a monomorphism in an $\infty$-topos $\mathfrak{X}$ then $\tau_{\leq 0}f\colon \tau_{\leq 0}X\to\tau_{\leq 0}Y$ is also a monomorphism (after including back into $\mathfrak{X}$)?

When $\mathfrak{X}=\mathcal{S}$, the $\infty$-topos of spaces, we can check that this is true just on homotopy groups. In that case $\tau_{\leq 0}X\simeq\pi_0(X)$ so certainly $\tau_{\leq 0}f$ remains an injection on $\pi_0$. Above $\pi_0$ it is an isomorphism from the trivial group to the trivial group. This suggests that one approach might be to write $\mathfrak{X}$ as a left exact localization of a presheaf $\infty$-topos and prove it there (since left exact localizations commute with truncation) but I have not been able to do that.

Improve this question
$\endgroup$
10
  • $\begingroup$ Would it suffice to prove, in homotopy type theory, that the 0-truncation of an embedding is an embedding? Because that should definitely be provable. $\endgroup$
    – Naïm Favier
    Commented Jul 10 at 19:06
  • $\begingroup$ @NaïmFavier I don't know. What's an embedding in homotopy type theory? $\endgroup$
    – Jonathan Beardsley
    Commented Jul 10 at 19:19
  • $\begingroup$ An embedding is a function with propositional fibres, which sounds a lot like your definition. They're also called $(-1)$-truncated maps in the HoTT book. An embedding between h-sets is just an injective function (in the sense that $f(x) = f(y) \to x = y$). $\endgroup$
    – Naïm Favier
    Commented Jul 10 at 19:22
  • $\begingroup$ I see, that sounds correct then. But this would need to happen in an arbitrary $\infty$-topos though. Does homotopy type theory work in the same way there? $\endgroup$
    – Jonathan Beardsley
    Commented Jul 10 at 19:29
  • 1
    $\begingroup$ It might be more useful to directly give a direct proof by informally following the HoTT proof rather than formally writing out the details of the interpretation. $\endgroup$
    – aws
    Commented Jul 10 at 19:49

1 Answer 1

Reset to default
2
$\begingroup$

I'm not an expert in ($\infty$-)topos theory, so someone would have to check that this really translates to a proof of what you want, but you can prove the following in homotopy type theory, which is supposed to be an internal language for $(\infty, 1)$-topoi:

Theorem. If $f : A \to B$ is an embedding (in the sense of HoTT book 4.6.1, equivalently a $(-1)$-truncated map), then $\|f\|_0 : \|A\|_0 \to \|B\|_0$ is also an embedding (where $\|\cdot\|_0$ is the 0-truncation or set truncation as defined in HoTT book 6.9).

Proof. Since $\|f\|_0$ is a function between sets, it suffices to prove that it is injective. Since this is a proposition (thus in particular a set), we may use the induction principle for the 0-truncation: that is, assuming $\|f\|_0(|x|_0) = \|f\|_0(|y|_0)$, we must show that $|x|_0 = |y|_0$. By definition of $\|f\|_0$, our assumption is that $|f(x)|_0 = |f(y)|_0$. Finally, using the equivalence $(|a|_0 = |b|_0) \simeq \|a = b\|_{-1}$ (HoTT book 7.3.12), it suffices to show that $\|f(x) = f(y)\|_{-1} \to \|x = y\|_{-1}$, which follows from the fact that $\mathrm{ap}_f$ has an inverse. $\square$

Improve this answer
$\endgroup$
3
  • $\begingroup$ Right, I think one issue here is that for an ∞-topos, ||f||₀ is not necessarily a set at all, which makes the idea of "injective" a bit complicated. But maybe that's handled by correctly "internalizing" the language. $\endgroup$
    – Jonathan Beardsley
    Commented Jul 10 at 19:54
  • 1
    $\begingroup$ You mean the 0-truncation of $B$ isn't necessarily 0-truncated‽ $\endgroup$
    – Naïm Favier
    Commented Jul 10 at 20:01
  • 5
    $\begingroup$ @JonathanBeardsley: That point is indeed handled by the internal language — 0-truncated objects of the ∞-topos are exactly the “sets” of its internal language. (Slightly more precisely: 0-truncated objects of its slices are the parametrised-families-of-sets of its internal languages.) And yes, the argument of this answer does indeed translate relatively directly, lemma-by-lemma, into a diagrammatic argument in an ∞-topos. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Jul 10 at 20:05

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .