Combinatorial proof that some model categories are monoidal/enriched?

Question

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.

Answer 1

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.

Answer 2

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.