Combinatorial proof that some model categories are monoidal/enriched?

I'm looking for examples of proofs that some Quillen model categories are monoidal, or enriched over an other model category, which are based on explicit computation of the "pushout product" of the generating cofirbations and generating trivial cofibrations, i.e. an explicit combinatorial proofs of a statement like: if $i:A \rightarrow C$ and $j:B \rightarrow D$ are respectively a generating cofibrations and a generating trivial cofibration then the "pushout-product" map:

$$i \otimes' j : C \otimes B \coprod_{A \otimes B} A \otimes D \rightarrow C \otimes D$$

is a composite of pushout of the generating trivial cofibrations (or maybe a retract of one of these). And same things for pushout-product of generating cofibrations.

I'm specifically interested in $\omega$-combinatorial model category, i.e. locally finitely presentable categories, with the generating cofibration and generating trivial cofibrations being maps between finitely presentable objects.

$\otimes$ above can either bi a monoidal structures or the tensoring for some enrichment. I also accept things that are not quite monoidal structure, as long as they are "bi-closed", so that this sort of condition does implies somethings (for example, the dendroidal "tensor product"), or things that are not quite model structures (like opetopic sets) if you have such combinatorial proof.

I already have some example where the condition are very easy to check:

• The model structure on ordinary category with cartesian product.
• Chain complexes.

In the literature I found such a proof for simplicial sets (both for the model structure for Kan complexes and for quasicategory) For Kan complex theorem 3.2.3 of Joyal & Tierney notes on simplicial homotopy theory does a special case, but it appears to be enough for deducing the general case by just playing around with the formal properties of the pushout-product. Similarly, Prop 2.3.2.1 of Lurie's Higher topos theory does a special case for the model structure for quasi-category, which also appears to be sufficient by formal property of the pushout-product.

In both case, the proof of the special case are pure combinatorics.

Cubical sets are also relatively easy to treat, but I still would prefer a reference if it exists.

I would be interested to see other examples of such direct combinatorics proof (like dendroidal sets, cellular sets, complicial sets, other algebraic structure , I assume no such things is known for opetopic sets but I would love to be wrong on that ).

Motivation : I'm finishing a paper about constructing some "weak" (like left & right semi structure) Quillen model structures in constructive mathematics. I have results which says that essentially when these kind of properties are verified then you can get some sort of weak model structure completely constructively. As these properties are purely combinatorial, there proof are generally constructive. I'd like to give as much example as I can, but proving myself that these conditions are indeed constructively valid is out of the scope of the paper if it takes more than five line. I can always invoke principle like Barr's covering theorem to say that constructive proof exists, but having a "clearly constructive proof" in the Litterature that I can quote is considerably better.

• I am a bit confused, the Joyal model structure is not a simplicial model category. Do you maybe mean the model structure on marked simplicial sets? Or do you mean a completely different thing and I am just misunderstanding? – Denis Nardin Mar 11 '18 at 15:11
• @DenisNardin : I don't mean it is enriched over simplicial sets. I just means its a cartesian model category (so it satisfies the pushout-product condition for the cartesian product against itself). – Simon Henry Mar 11 '18 at 16:09
• Oh and of course, I mean't it only in terms of a "pseudo-generating class" of trivial cofibrations (in the sense mentioned by Tim Campion below) for the Joyal model structure, as as far as I know we do not really have nice class of generating cofibrations to test this conditions. – Simon Henry Mar 14 '18 at 17:13

This is far from a comprehensive answer, but since you ask for references, here are two.

The result for simplicial sets is obtained by an explicit computation in Appendix H of Joyal's The Theory of Quasi-categories and Its Applications.

For $\Theta_2$-sets, there is Chapter 3 of Oury's Duality for Joyal's Category $\Theta$ and Homotopy Concepts for $\Theta_2$-sets.

I'll do you one better: you don't need a generating set of acyclic cofibrations. You just need what Simpson calls a pseudo-generating set, i.e. a set of acyclic cofibrations which suffices to detect fibrant objects and fibrations between fibrant objects (i.e. an object is fibrant iff it lifts against every morphism in your pseudo-generating set, and similarly for a map between fibrant objects being a fibration).

That is, I claim your observation still holds if you only check with the morphisms of a pseudo-generating set rather than an actual generating set of acyclic cofibrations.

Explicit generating sets of acyclic cofiberations are hard to find, but pseudo-generating sets abound. For example, the inner horns plus the endcap inclusion of the walking isomsomorphism form a pseudo-generating set for the Joyal model structure. A great source of them comes from Cisinski-Olschok theory: their construction $S \mapsto \Lambda(S)$ is a minimal way of getting a pseudo-generating set out of a set of morphisms. Because the construction of $\Lambda(S)$ is explicit and combinatorial, one can often show that $\Lambda(S)$ is in the cofibrant closure of $S$, so that $S$ was already a pseudo-generating set (and showing this is an essentially combinatorial exercise). For example, this works in the case of the Joyal model structure.

My impression is that everything that Cisinski/Olschok do is very explicit, and is probably constructive.

• This is indeed true, but I already know that. At this point, I'm really just looking for examples to which applies this kind of machinery, i.e. finitely presentable categories where we do have a direct proof that (at least some cases) of the pushout-product are verified. – Simon Henry Mar 11 '18 at 18:01
• I have some handwritten notes where I do this for complicial sets -- it's basically just a few more things to check on top of the quasicategory case. I don't know of anything in the literature. But I would say "most" combinatorial model categories in practice are naturally described via Cisinski-Olschok theory -- the only real restriction is that you need every object cofibrant, since the functorial cylinder is always there in practice. – Tim Campion Mar 11 '18 at 18:27
• So for example, it should be straightforward to churn out combinatorial proofs for existence and cartesianness of model structures on marked simplicial sets over a base, (iterated) complete Segal spaces, etc. But I suppose if your main concern is to be able to quote something, this isn't much help... – Tim Campion Mar 11 '18 at 18:27
• Well I would indeed prefer to find references, but that is still good to know. – Simon Henry Mar 11 '18 at 18:34
• Oh -- one more thing I wanted to say -- it seems that given a Cisinski-Olschok model structure with symmetric monoidal closed $\otimes$, the most natural way to prove that $\Lambda(S)$ is in the cofibrant closure of $S$ is often to prove more generally that $f \hat \otimes g$ is in the cofibrant closure of $S$ for $f \in S$ and $g$ a cofibration. So showing that $S$ is a pseudo-generating set and showing that the model structure is monoidal are done all at once. – Tim Campion Mar 12 '18 at 19:07