Cellular maps

Content created by Egbert Rijke.

Created on 2023-11-23.
Last modified on 2023-11-23.

module orthogonal-factorization-systems.cellular-maps where
Imports 
open import foundation.connected-maps
open import foundation.truncation-levels
open import foundation.universe-levels

open import orthogonal-factorization-systems.mere-lifting-properties

Idea

A map f : A → B is said to be k-cellular if it satisfies the left mere lifting propery with respect to k-connected maps. In other words, a map f is k-cellular if the pullback-hom

  ⟨ f , g ⟩

with any k-connected map g is surjective. The terminology k-cellular comes from the fact that the k-connected maps are precisely the maps that satisfy the right mere lifting property wtih respect to the spheres

  Sⁱ → unit

for all -1 ≤ i ≤ k. In this sense, k-cellular maps are "built out of spheres". Alternatively, k-cellular maps might also be called k-projective maps. This emphasizes the condition that k-projective maps lift against k-connected maps.

In the topos of spaces, the k-cellular maps are the left class of an external weak factorization system on spaces of which the right class is the class of k-connected maps, but there is no such weak factorization system definable internally.

Definitions

The predicate of being a k-cellular map

module _
  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
  where

  is-cellular-map : UUω
  is-cellular-map =
    {l3 l4 : Level} {X : UU l3} {Y : UU l4} (g : X → Y) →
    is-connected-map k g → mere-diagonal-lift f g

Recent changes