`k`-acyclic types

Content created by Tom de Jong.

Created on 2023-11-27.
Last modified on 2023-12-04.

module synthetic-homotopy-theory.truncated-acyclic-types where

Imports

open import foundation.connected-types
open import foundation.contractible-types
open import foundation.equivalences
open import foundation.propositions
open import foundation.retracts-of-types
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.functoriality-suspensions
open import synthetic-homotopy-theory.suspensions-of-types

Idea

A type A is said to be k-acyclic if its suspension is k-connected.

Definition

module _
  {l : Level} (k : 𝕋) (A : UU l)
  where

  is-truncated-acyclic-Prop : Prop l
  is-truncated-acyclic-Prop = is-connected-Prop k (suspension A)

  is-truncated-acyclic : UU l
  is-truncated-acyclic = type-Prop is-truncated-acyclic-Prop

  is-prop-is-truncated-acyclic : is-prop is-truncated-acyclic
  is-prop-is-truncated-acyclic = is-prop-type-Prop is-truncated-acyclic-Prop

We use the name is-truncated-acyclic instead of is-truncation-acyclic, because the latter, in line with is-truncation-equivalence, might suggest that it is the truncation of a type that is acyclic which is not the notion we’re interested in.

Properties

Being `k`-acyclic is invariant under equivalence

is-truncated-acyclic-equiv :
  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} →
  A ≃ B → is-truncated-acyclic k B → is-truncated-acyclic k A
is-truncated-acyclic-equiv {k = k} {B = B} e ac =
  is-connected-equiv (equiv-suspension e) ac

is-truncated-acyclic-equiv' :
  {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} →
  A ≃ B → is-truncated-acyclic k A → is-truncated-acyclic k B
is-truncated-acyclic-equiv' e = is-truncated-acyclic-equiv (inv-equiv e)

`k`-acyclic types are closed under retracts

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

  is-truncated-acyclic-retract-of :
    A retract-of B →
    is-truncated-acyclic k B →
    is-truncated-acyclic k A
  is-truncated-acyclic-retract-of R ac =
    is-connected-retract-of
      ( retract-of-suspension-retract-of R)
      ( ac)

Every `k`-connected type is `(k+1)`-acyclic

module _
  {l : Level} {k : 𝕋} {A : UU l}
  where

  is-truncated-acyclic-succ-is-connected :
    is-connected k A → is-truncated-acyclic (succ-𝕋 k) A
  is-truncated-acyclic-succ-is-connected =
    is-connected-succ-suspension-is-connected

Contractible types are `k`-acyclic for any `k`

is-truncated-acyclic-is-contr :
  {l : Level} {k : 𝕋} (A : UU l) → is-contr A → is-truncated-acyclic k A
is-truncated-acyclic-is-contr {k = k} A c =
  is-connected-is-contr k (is-contr-suspension-is-contr c)

is-truncated-acyclic-unit : {k : 𝕋} → is-truncated-acyclic k unit
is-truncated-acyclic-unit = is-truncated-acyclic-is-contr unit is-contr-unit

Every `(k+1)`-acyclic type is `k`-acyclic

module _
  {l : Level} {k : 𝕋} {A : UU l}
  where

  is-truncated-acyclic-is-truncated-acyclic-succ :
    is-truncated-acyclic (succ-𝕋 k) A → is-truncated-acyclic k A
  is-truncated-acyclic-is-truncated-acyclic-succ =
    is-connected-is-connected-succ-𝕋 k

Recent changes

2023-12-04. Tom de Jong. k-acyclic maps/types closure properties (#967).
2023-12-01. Tom de Jong. A type is 1-acyclic if and only if it is 0-connected (#956).
2023-11-29. Tom de Jong. Suspensions increase connectedness and relating k-acyclic maps, k-equivalences and k-connected maps (#951).
2023-11-29. Tom de Jong. Comment on the name is-truncated-acyclic (#950).
2023-11-27. Tom de Jong. k-acyclic types (#948).

agda-unimath