0-acyclic maps

Content created by Tom de Jong.

Created on 2023-12-01.
Last modified on 2023-12-01.

module synthetic-homotopy-theory.0-acyclic-maps where
Imports 
open import foundation.epimorphisms-with-respect-to-sets
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.truncation-levels
open import foundation.universe-levels

open import synthetic-homotopy-theory.truncated-acyclic-maps

Idea

A 0-acyclic map is a map whose fibers are 0-acyclic types, meaning that their suspension is 0-connected.

We can characterize the 0-acyclic maps as the surjective maps.

Definition

The predicate of being a 0-acyclic map

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-0-acyclic-map-Prop : (A → B) → Prop (l1 ⊔ l2)
  is-0-acyclic-map-Prop = is-truncated-acyclic-map-Prop (zero-𝕋)

  is-0-acyclic-map : (A → B) → UU (l1 ⊔ l2)
  is-0-acyclic-map f = type-Prop (is-0-acyclic-map-Prop f)

  is-prop-is-0-acyclic-map :
    (f : A → B) → is-prop (is-0-acyclic-map f)
  is-prop-is-0-acyclic-map f =
    is-prop-type-Prop (is-0-acyclic-map-Prop f)

Properties

A map is 0-acyclic if and only if it is surjective

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

  is-surjective-is-0-acyclic-map :
    is-0-acyclic-map f → is-surjective f
  is-surjective-is-0-acyclic-map ac =
    is-surjective-is-epimorphism-Set
      ( is-epimorphism-is-truncated-acyclic-map-Truncated-Type f ac)

  is-0-acyclic-map-is-surjective :
    is-surjective f → is-0-acyclic-map f
  is-0-acyclic-map-is-surjective s =
    is-truncated-acyclic-map-is-epimorphism-Truncated-Type f
      ( is-epimorphism-is-surjective-Set s)

See also

Recent changes