Pushouts of Dwyer maps
======================

History:
* 2024-06-20: initial version

In [1], it is proved that in the category of categories, pushouts along Dwyer maps are preserved under the embedding into higher categories ((∞, 1)-categories).

[1] https://archive.mpim-bonn.mpg.de/4756/1/mpim-preprint_2022-39.pdf

We present an abstract, higher categorical argument, that replaces combinatorial reasoning with higher category theory.
Instead of asking whether the embedding of categories into higher categories preserves certain pushouts, we can equivalently ask if certain pushouts in higher categories preserve 1-categories (higher categories with 0-truncated homs).
In this approach, we only need certain abstract properties of Dwyer maps, and those are also satisfied by Cisinski's more general definition of Dwyer maps.

For a functor f : A → B of higher categories, write f_! ⊣ f^* for the induced adjunction between Psh(A) and Psh(B).

Consider a pushout of higher categories:
  A --[g]-> C
  ↓f        ↓p
  B --[q]-> D.

The following statement is the directed version of the statement that pushouts in homotopy types preserve monomorphisms and form pullback squares.
The proof is similar, using descent for right fibrations in categories instead of descent in spaces.
It is also a trivial case of David Wärn's more general zig-zag construction applied to higher categories instead of spaces.

Lemma 1.
Assume that f is fully faithful.
Then:
(a) p is fully faithful,
(b) the square is exact in the sense that the mate
      f_! g^* ---> q^* p_!
    is invertible.

Proof.
Consider a right fibration X → C.
Consider the cube with vertical right fibrations with back face
  g^* X -------> X
  ↓              ↓
  A -----------> C
and front face
  f_! g^* X ---> p_! X
  ↓              ↓
  B -----------> D.
The back square is a pullback by construction.
The left square is a pullback since f is fully faithful.
When left Kan extending the top square to right fibrations over D, its left and right maps become invertible, hence it becomes a pushout.
We can thus apply descent for right fibrations.
This makes the other vertical squares pullbacks.
From the right square being cartesian, we get (a).
From the front square being cartesian, we get (b).
□

The second part says that the canonical map
  ∫^{a:A} B(b₀, f(a)) × C(g(a), c₁) ---> D(q(b₀), p(c₁)).
is invertible for b₀ ∈ B and c₁ ∈ C.

The following statement intuitively says that pushouts along sieves are boring when looking at maps from objects that come from the complement of the sieve.

Lemma 2.
Assume that f is a sieve (fully faithful and a cartesian fibration).
For b₀ ∈ B, we have that b₀ is in the image of f or we have:
* for b₁ ∈ B, the map
    B(b₀, b₁) → D(q(b₀), q(b₁))
  is invertible,
* D(q(b₀), p(c₁)) is empty for c₁ ∈ C.
□

Recall that a map of presheaves is 0-truncated exactly if its components are 0-truncated.

Lemma 3.
Assume:
(1) f is a cosieve between 1-categories,
(2) f_! preserves 0-truncated presheaves,
If C is a 1-category, so is D.

Proof.
Note that the map B ⊔ C → D is surjective on objects.
Therefore, it suffices to show the following homotopy types are 0-truncated:
(CC) D(p(c₀), p(c₁)) for c₀ ∈ C and c₁ ∈ C,
(CB) D(p(c₀), q(b₁)) for c₀ ∈ C and b₁ ∈ B,
(BC) D(q(b₀), p(c₁)) for b₀ ∈ B and c₁ ∈ C,
(BB) D(q(b₀), q(b₁)) for b₀ ∈ B and b₁ ∈ B,

For (CC), we have
  D(p(c₀), p(c₁)) ≃ C(c₀, c₁)
by Lemma 1 (a), which is 0-truncated since C is a 1-category.

For (BC), we have
  D(q(b₀), p(c₁)) ≃ (q^* p_! y(c₁))(b₀) ≃ (f_! g^* y(c₁))(b₀),
by Lemma 1 (b), which is M-modal since C is a 1-category and using (2).

For (CB) and (BB), we apply Lemma 2 to the opposite pushout square (where f^op is a sieve).
If b₁ is in the image of f, then p(b₁) ≃ q(c₁) for some c₁ ∈ C, so we reduce to an instance of (CC) or (BC).
In the other cases, we are done since B is a 1-category and the initial presheaf is 0-truncated.
□

Note that the above lemma works more generally with 0-truncatedness replaced by some Σ-closed subuniverse M of homotopy types that contains the empty homotopy type.
More generally, we only need the "attaching part" of the target of f : A → B to have 0-truncated homs.

We have the walking retract S:
  0 --[s]-> 1 --[r]-> 0.

An *(op)lax retract* of functors is a retract in Cat^[1]_(op)lax.

Lemma 4.
Dwyer maps (in the weak sense) are lax retracts of cosieves.

Proof.
Consider a Dwyer map i : A → B.
This means we have a lax retract diagram
  A --[u]-> W ---[v]-> A
  ↓i   =    ↓j    ↙    ↓i
  B ======= B ======== B
where j is a cosieve.
□

Lemma 5.
Consider
  α : S ---> Cat^[1]_(op)lax.
Then α₀ is a retract of α(r)₁ α₁ α(s)₀.

Proof.
By pasting of natural transformations.
□

Write Adj for the category of adjoint functors.
Here, a morphism from l₀ ⊣ r₀ and l₁ ⊣ r₁ is a natural transformation
  • -----> •
  ↓r₀  ↘   ↓r₁
  • -----> •,
equivalently a natural transformation
  • -----> •
  ↑l₀  ↙   ↑l₁
  • -----> •.
Formally, the forgetful functors
  R : Adj → Cat^[1]_lax
  L : Adj → Cat^[1]_oplax
to (op)lax arrow categories of the bicategory Cat are fully faithful.

Lemma 6.
Consider a retract
  S ---> Cat^[1]_{small,lax},
denoted
  A₀ --[A_s]-> A₁ --[A_r]-> A₀
  ↓F₀    ↗     ↓F₁    ↗     ↓F₀
  B₀ --[B_s]-> B₁ --[B_r]-> B₀.
Then F₀_! is a retract of B_s^* F₁_! A_r^*.

Proof.
Taking presheaf categories, we get
  S^op ---> Cat^[1]_lax.
This is:
  Psh(A₀) <-[A_s^*]-- Psh(A₁) <-[A_r^*]-- Psh(A₀)
  ↑F₀^*        ↙      ↑F₁^*        ↙      ↑F₀^*
  Psh(B₀) <-[B_s^*]-- Psh(B₁) <-[B_r^*]-- Psh(B₀).
We have left adjoints (F₀)_! ⊣ F₀^* and (F₁)_! ⊣ F₁^*.
This gives a lift
  S^op ∙∙∙> Adj
  ↓         ↓R
  S^op ---> Cat^[1]_lax
since R is fully faithful.
The claim follows by Lemma 5 applied to the composite
  S^op ---> Adj --[L]-> Cat^[1]_oplax,
which looks like this:
  Psh(A₀) <-[A_s^*]-- Psh(A₁) <-[A_r^*]-- Psh(A₀)
  ↓(F₀)_!      ↘      ↓(F₁)_!      ↘      ↓(F₀)_!
  Psh(B₀) <-[B_s^*]-- Psh(B₁) <-[B_r^*]-- Psh(B₀).
□

Corollary 7.
Consider a lax retract f of a right fibration with 0-truncated fibers.
Then f_! preserves 0-truncated presheaves.

Proof.
By Lemma 6, we have that f_! is a retract of
  v^* g_! u^*
for a sieve g and functors u, v.
The restrictions u^* and v^* preserve 0-truncatedness as it is a fiberwise property.
Left Kan extension with the right fibration g is just given by postcomposition.
Since right fibrations with 0-truncated fibers are closed under composition, g_! preserves 0-truncatedness.
Finally, retracts preserve 0-truncatedness.
□

Corollary 8.
Assume that f is a Dwyer map.
If C is a 1-category, so is D.

Proof.
Since f is a Dwyer map, f^op is a cosieve and a lax retract of a sieve by Lemma 4.
By Corollary 7, (f^op)_! preserves 0-truncated presheaves.
The claim follows by Lemma 3 applied to the opposite pushout square.
□