nLab
constructive model structure on simplicial sets

Contents

Context

Model category theory

model category

Definitions

Morphisms

Universal constructions

Refinements

Producing new model structures

Presentation of (,1)(\infty,1)-categories

Model structures

for \infty-groupoids

for ∞-groupoids

for rational \infty-groupoids

for nn-groupoids

for \infty-groups

for \infty-algebras

general

specific

for stable/spectrum objects

for (,1)(\infty,1)-categories

for stable (,1)(\infty,1)-categories

for (,1)(\infty,1)-operads

for (n,r)(n,r)-categories

for (,1)(\infty,1)-sheaves / \infty-stacks

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Constructivism, Realizability, Computability

Contents

Idea

A model structure on simplicial sets valid in constructive mathematics that reduced to the classical model structure on simplicial sets in presence of the law of excluded middle and axiom of choice.

The original proofs of the existence of the classical model structure on simplicial sets are based in classical mathematics as they use the principle of excluded middle and the axiom of choice, and are hence not valid in constructive mathematics. This becomes more than a philosophical issue with the relevance of this model category-structure in homotopy type theory, where internalization into the type theory requires constructive methods for interpreting proofs as programs.

A constructively valid model structure on simplicial sets and coinciding with the classical model structure if excluded middle and axiom of choice are assumed was found in Henry 19. Alternative simpler proofs were found in Gambino-Sattler-Szumiło 19

Properties

Fibrations and lifting properties

Fibrations? and acyclic fibrations

are defined using the right lifting property with respect to the usual sets of horn inclusions? and boundary inclusions?. However, the meaning of this definition is more refined: due to the constructive nature of the existential quantifier, being an (acyclic) fibration means we have a section of the map from the set of solutions to lifting problems to the set of lifting problems.

Weak equivalences

Simplicial weak equivalences? must also be defined more carefully.

We follow GambinoSattlerSzumilo19. Suppose f:XYf\colon X\to Y is a simplicial map.

  • If XX and YY are cofibrant Kan complexes, then ff is a weak equivalence if it is a simplicial homotopy equivalence;
  • If XX and YY are Kan complexes, then ff is a weak equivalence if there is a simplicial map f:XYf'\colon X'\to Y' and acyclic fibrations with cofibrant domains XXX'\to X and YYY'\to Y such that ff' is a weak equivalence in the previous sense and the square with ff and ff' commutes;
  • If XX and YY are cofibrant, then ff is a weak equivalence if for any Kan complex KK the map Hom(f,K)Hom(f,K) is a weak equivalence in the previous sense (notice that its domain and codomain are Kan complexes);
  • If XX and YY are arbitrary, then ff is a weak equivalence if it has a replacement f:XYf'\colon X'\to Y' like above, with ff' being a weak equivalence in the previous sense.

Cofibrant objects

While in the classical model structure on simplicial sets all objects (simplicial sets) are cofibrant, a simplicial set is cofibrant in the constructive model structure if and only if the inclusion of degenerate nn-simplices into all nn-simplices is a decidable inclusion of sets.

Likewise, cofibrations ABA\to B are simplicial maps such that A nB nA_n\to B_n is a decidable inclusion of sets and the inclusion of degenerate nn-simplices as a subset into B nA nB_n\setminus A_n is also a decidable inclusion.

Since not all objects are cofibrant, left properness is no longer automatic, but can still be established through nontrivial arguments.

This model structure is also right proper.

See Henry 19 and Gambino-Sattler-Szumiło 19 for a proof of these claims.

References

Last revised on April 13, 2020 at 14:58:32. See the history of this page for a list of all contributions to it.