Skip to content

Commit

Permalink
The acyclic maps are exactly the epimorphisms (#894)
Browse files Browse the repository at this point in the history
  • Loading branch information
tomdjong authored Oct 30, 2023
1 parent 9743045 commit e4b0e89
Showing 1 changed file with 35 additions and 0 deletions.
35 changes: 35 additions & 0 deletions src/synthetic-homotopy-theory/acyclic-maps.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,17 @@ module synthetic-homotopy-theory.acyclic-maps where
<details><summary>Imports</summary>

```agda
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.epimorphisms
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.propositions
open import foundation.universe-levels

open import synthetic-homotopy-theory.acyclic-types
open import synthetic-homotopy-theory.codiagonals-of-maps
open import synthetic-homotopy-theory.suspensions-of-types
```

</details>
Expand Down Expand Up @@ -41,6 +47,35 @@ module _
is-prop-is-acyclic-map f = is-prop-type-Prop (is-acyclic-map-Prop f)
```

## Properties

### A map is acyclic if and only if it is an [epimorphism](foundation.epimorphisms.md)

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

is-acyclic-map-is-epimorphism : is-epimorphism f is-acyclic-map f
is-acyclic-map-is-epimorphism e b =
is-contr-equiv
( fiber (codiagonal-map f) b)
( equiv-fiber-codiagonal-map-suspension-fiber f b)
( is-contr-map-is-equiv
( is-equiv-codiagonal-map-is-epimorphism f e)
( b))

is-epimorphism-is-acyclic-map : is-acyclic-map f is-epimorphism f
is-epimorphism-is-acyclic-map ac =
is-epimorphism-is-equiv-codiagonal-map f
( is-equiv-is-contr-map
( λ b
is-contr-equiv
( suspension (fiber f b))
( inv-equiv (equiv-fiber-codiagonal-map-suspension-fiber f b))
( ac b)))
```

## See also

- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
Expand Down

0 comments on commit e4b0e89

Please sign in to comment.