Filter Quotient Model Structures

This paper establishes that the filter quotient construction preserves model structures under suitable conditions, demonstrating that while the resulting model inherits properties like being simplicial or proper, it may not remain cofibrantly generated, and further proves its compatibility with filter quotient $\infty$-categories.

The Gist

Here is an explanation of Nima Rasekh's paper, "Filter Quotient Model Structures," translated into simple, everyday language with creative analogies.

The Big Picture: Building New Worlds from Old Ones

Imagine you are an architect who designs "universes" for mathematics. In this paper, the author is introducing a new, powerful tool to build these universes.

To understand the tool, we first need to understand the materials:

1. Model Categories: Think of these as highly organized rulebooks for a specific type of mathematical universe. They tell you what counts as "the same" (equivalence), what counts as "solid" (cofibrations), and what counts as "stable" (fibrations). These rulebooks are essential for doing advanced math, especially in fields like topology (shapes) and computer science (type theory).
2. The Problem: Usually, to build a new rulebook, you need a very specific, tidy foundation. You need the universe to be "locally presentable" or "cofibrantly generated." In plain English, this means the universe must be built from a manageable, finite set of Lego bricks. If your universe is too big, too messy, or doesn't have a clear "smallest building block," the standard construction methods fail. You can't build a new rulebook for it.
3. The Goal: The author wants to build rulebooks for these "messy" universes that don't have those tidy, finite foundations.

The Solution: The "Filter Quotient"

The author introduces a construction called the Filter Quotient. Let's break this down with an analogy.

The Analogy: The "Focus Group" Universe

Imagine you have a massive library of books (your original mathematical universe). Some books are perfect, some are messy, and some are just drafts.

Now, imagine you have a Filter. A filter is like a very strict Focus Group or a Censor.

• The filter says: "We only care about the parts of the library that appear in these specific chapters."
• If two books look different in general, but they look exactly the same in the chapters the filter cares about, the filter says: "They are the same book."

The Filter Quotient is the new library you create by taking the old library and merging everything that the filter considers "the same." You are essentially zooming in on a specific perspective and ignoring the rest of the noise.

What This Paper Proves

For a long time, mathematicians thought that if you took a messy universe and applied this "Focus Group" filter, the resulting new universe would lose its structure. It would become too chaotic to have a proper rulebook (model structure).

Rasekh's big discovery is:

"No! If you start with a well-organized universe and apply a specific kind of filter, the new, filtered universe keeps its rulebook intact."

He proves that the new universe still has:

• Equivalences: You can still tell what is "the same."
• Limits and Colimits: You can still combine things and break them apart logically.
• Properness: The rules for stability still work.
• Simplicial Structure: It still works well with the specific type of geometry used in modern math (like shapes made of triangles).

Why Does This Matter? (The "Type Theory" Connection)

The paper mentions Type Theory and Proof Assistants (like Lean).

• The Analogy: Think of Type Theory as the "operating system" for modern mathematics. It's how we write proofs that computers can check.
• The Issue: Many interesting mathematical ideas (especially in Homotopy Type Theory) live in "messy" universes that don't fit the standard "Lego brick" requirements. Because they don't fit the standard requirements, we couldn't prove they were valid models for the computer to check.
• The Impact: This paper provides a way to construct valid models for these messy, complex ideas. It opens the door for computers to verify proofs in areas of math that were previously too "unruly" to handle.

What Doesn't Work? (The Trade-off)

The paper is honest about the limitations. While the new universe keeps most of its good properties, it loses some specific "superpowers":

• It's not "Cofibrantly Generated": The new universe is too big to be built from a small, finite list of Lego bricks. It's a "giant" universe.
• It's not "Locally Presentable": It doesn't have a nice, tidy list of all its possible shapes.

The Metaphor:
Imagine you have a small, perfectly organized garden (the old model). You use a filter to create a new garden that focuses only on the flowers that bloom in the summer.

• Good news: The new garden still has soil, water, and sunlight (the model structure). You can still grow things there.
• Bad news: The new garden is now so vast and wild that you can't count every single flower or organize them into neat rows anymore (it's not cofibrantly generated).

The "Filter Product" (A Special Case)

The paper also looks at a specific type of filter called a Filter Product.

• Analogy: Imagine you have 1,000 identical copies of a movie. You use a filter to say, "We only care about the scenes that appear in at least 90% of the copies."
• The result is a new movie that is a "super-version" of the original, combining the best parts of all 1,000 copies.
• Rasekh shows that even if you do this with 1,000 copies of a mathematical universe, the result is still a valid mathematical universe with a working rulebook.

Summary

Nima Rasekh has found a way to build mathematical rulebooks for "messy" worlds that were previously thought to be impossible to organize.

By using a "Filter Quotient" (a way of zooming in on specific parts of a universe and ignoring the rest), he proves that these new, complex worlds still follow the laws of homotopy theory. This is a huge step forward for Homotopy Type Theory, allowing mathematicians and computers to explore and verify proofs in much larger, more complex mathematical landscapes than ever before.

Technical Summary

Here is a detailed technical summary of the paper "Filter Quotient Model Structures" by Nima Rasekh.

1. Problem Statement

The construction of new model structures typically relies on "small generation" assumptions, such as local presentability of the underlying category or cofibrant generation (e.g., Cisinski model structures, transferred model structures, Bousfield localizations). These methods fail for categories that are too large to satisfy finiteness conditions yet lack the "small generation" properties required by standard techniques.

Specifically, there is a gap in constructing model structures for filter quotient $\infty$-categories (introduced in [Ras21]). These structures are crucial for modeling certain type theories (specifically Homotopy Type Theory) but often lack countable colimits or accessibility, rendering standard combinatorial model category techniques inapplicable. The paper addresses the problem of constructing a valid model structure on a filter quotient category $M_\Phi$ derived from a model category $M$, without assuming local presentability or cofibrant generation.

2. Methodology

The author employs a direct construction approach based on the filter quotient mechanism from categorical logic and topos theory.

• Filter Quotient Construction: Given a category $\mathcal{C}$ with finite products and a filter $\Phi$ of subterminal objects, the filter quotient category $\mathcal{C}_\Phi$ is defined. Objects remain the same, but morphisms $X \to Y$ are equivalence classes of morphisms $X \times U \to Y$ for $U \in \Phi$. Two morphisms are equivalent if they agree on a "smaller" $W \in \Phi$.
• Model Filter Definition: To lift a model structure from $M$ to $M_\Phi$, the author defines a model filter $\Phi$. This is a filter of discrete homotopically subterminal objects (objects that are fibrant, subterminal, and have a weak equivalence diagonal) satisfying specific stability conditions:
  • The classes of cofibrations ($C$) and weak equivalences ($W$) must be $\Phi$-product stable. That is, if $f \in C$ (or $W$), then $f \times U \in C$ (or $W$) for all $U \in \Phi$.
• Lifting the Structure: The model structure on $M_\Phi$ is defined by declaring a morphism in $M_\Phi$ to be a fibration, cofibration, or weak equivalence if it is represented by a morphism in $M$ that belongs to the respective class after product with some $U \in \Phi$.
• Verification: The axioms of a model category (lifting, factorization, retracts, 2-out-of-3) are verified by reducing them to the corresponding properties in the original category $M$ via the projection functor $P_\Phi$.

3. Key Contributions

The paper makes several significant theoretical contributions:

1. Existence Theorem: It proves that if $M$ is a model category and $\Phi$ is a model filter, then the filter quotient $M_\Phi$ admits a model structure (Theorem 3.16). Crucially, this does not require $M$ to be cofibrantly generated or locally presentable.
2. Preservation of Properties: The paper establishes which model categorical properties are preserved under the filter quotient construction:
   • Preserved: Finite (co)limits, Cartesian closure, properness (left/right), and simplicial/enriched structures (under specific compatibility conditions).
   • Not Preserved: Infinite (co)limits (specifically infinite coproducts), local presentability, and cofibrant generation.
3. Compatibility with $\infty$-Categories: It proves that the underlying $\infty$-category of the filter quotient model category $M_\Phi$ is equivalent to the filter quotient $\infty$-category $Ho_\infty(M)_\Phi$ defined in prior work [Ras21]. This bridges the gap between model-categorical presentations and $\infty$-categorical definitions.
4. Filter Products: The paper introduces filter products ($\prod_\Phi M$) as a specific, highly applicable class of filter quotients where $\Phi$ is a filter of subsets of a set $I$. This construction preserves properness and enrichment while breaking cofibrant generation.

4. Key Results and Examples

• Theorem 3.16: The main result establishing the model structure on $M_\Phi$.
• Properness: If $M$ is right proper, $M_\Phi$ is right proper. If $M$ is left proper and the filter objects preserve pushouts, $M_\Phi$ is left proper (Propositions 4.3, 4.4).
• Enrichment: If $M$ is a compactly enriched model category and $\Phi$ is a "V-enriched model filter," then $M_\Phi$ retains the enriched structure (Theorem 4.15).
• Counterexamples to Generation:
  • Example 7.1: The filter product of simplicial sets ($sSet$) with the Fréchet filter on $\mathbb{N}$ yields a model category that is proper and simplicial but not cofibrantly generated and lacks countable coproducts.
  • Example 7.2: A similar result for topological spaces with the Serre model structure.
• New $\infty$-Cosmoi: The construction yields $\infty$-cosmoi (categories of fibrant objects in a model category) that are generated by the terminal object but are not locally presentable or accessible (Example 7.7). This expands the landscape of known $\infty$-categories beyond the standard presentable ones.
• Change of Models: The construction is stable under Quillen equivalences between different models of $(\infty, 1)$-categories (e.g., between quasi-categories and complete Segal spaces), allowing the transfer of filter quotient structures across different foundational models (Example 7.9).

5. Significance

This work is significant for several reasons:

• Foundations of Type Theory: It provides the necessary model-categorical machinery to construct models for Homotopy Type Theory (HoTT) that were previously inaccessible. Specifically, it allows for models arising from filter quotients, which are expected to correspond to specific logical properties in type theory that combinatorial models cannot capture.
• Beyond Combinatorics: It demonstrates that rich homotopical structures (proper, simplicial, Cartesian closed) can exist outside the realm of combinatorial model categories. This challenges the reliance on local presentability as a prerequisite for doing homotopy theory.
• Unification: It unifies the construction of filter quotient $\infty$-categories with classical model category theory, showing that the $\infty$-categorical limit construction has a concrete model-categorical realization.
• New Mathematical Objects: By generating non-presentable $\infty$-cosmoi, the paper opens new avenues for studying homotopy theory in contexts where standard "small object" arguments fail, potentially impacting the study of large categories and non-standard models of set theory.

In summary, Rasekh successfully extends the toolkit of model category theory to a broader class of categories, enabling the rigorous study of homotopy types in settings previously considered too "large" or "unstructured" for model-theoretic analysis.