Skip to content

Commit

Permalink
Closure properties of acyclic maps and types (#960)
Browse files Browse the repository at this point in the history
I also formalized that we have symmetric pushout squares (for pullbacks
this was already in the library), i.e. the pushout of two maps `f` and
`g` is also the pushout of `g` and `f`.
  • Loading branch information
tomdjong authored Dec 1, 2023
1 parent b088b24 commit f4e8b21
Show file tree
Hide file tree
Showing 4 changed files with 364 additions and 0 deletions.
234 changes: 234 additions & 0 deletions src/synthetic-homotopy-theory/acyclic-maps.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ module synthetic-homotopy-theory.acyclic-maps where

```agda
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.cones-over-cospans
open import foundation.constant-maps
open import foundation.contractible-maps
open import foundation.contractible-types
Expand All @@ -21,19 +23,30 @@ open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-fibers-of-maps
open import foundation.homotopies
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.precomposition-dependent-functions
open import foundation.precomposition-functions
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.pullbacks
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universal-property-cartesian-product-types
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.acyclic-types
open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.codiagonals-of-maps
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.suspensions-of-types
open import synthetic-homotopy-theory.universal-property-pushouts
```

</details>
Expand Down Expand Up @@ -289,6 +302,227 @@ module _
( is-epimorphism-is-acyclic-map f af))
```

### Acyclic maps are closed under pushouts

We give an outline of the proof before formalizing it.

Suppose we have a pushout square on the left in the diagram

```text
g j
S -------> B -------> C
| | |
f | | j | id
| | |
v ⌜ v v
A -------> C -------> C
i id
```

Then `j` is acyclic if and only if the right square is a pushout, which by
pushout pasting, is equivalent to the outer rectangle being a pushout. For an
arbitrary type `X` and `f` acyclic, we note that the following composite
computes to the identity:

```text
cocone-map f (j ∘ g)
(C X) ---------------------> cocone f (j ∘ g) X
̇= Σ (l : A X) , Σ (r : C X) , l ∘ f ~ r ∘ j ∘ g
(using the left square)
≃ Σ (l : A X) , Σ (r : C X) , l ∘ f ~ r ∘ i ∘ f
(since f is acyclic/epic)
≃ Σ (l : A X) , Σ (r : C X) , l ~ r ∘ i
≃ Σ (r : C X) , Σ (l : A X) , l ~ r ∘ i
(contracting at r ∘ i)
≃ (C X)
```

Therefore, `cocone-map f (j ∘ g)` is an equivalence and the outer rectangle is
indeed a pushout.

```agda
module _
{l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
{C : UU l4} (f : S A) (g : S B) (c : cocone f g C)
where

equiv-cocone-postcomp-vertical-map-cocone :
is-acyclic-map f
{l5 : Level} (X : UU l5)
cocone f (vertical-map-cocone f g c ∘ g) X ≃ (C X)
equiv-cocone-postcomp-vertical-map-cocone ac X =
equivalence-reasoning
cocone f (vertical-map-cocone f g c ∘ g) X
≃ cocone f (horizontal-map-cocone f g c ∘ f) X
by
equiv-tot
( λ u
equiv-tot
( λ v
equiv-concat-htpy'
( u ∘ f)
( λ s ap v (inv-htpy (coherence-square-cocone f g c) s))))
≃ Σ ( A X)
( λ u
Σ (C X) (λ v u ∘ f = v ∘ horizontal-map-cocone f g c ∘ f))
by equiv-tot ( λ u equiv-tot ( λ v equiv-eq-htpy))
≃ Σ (A X) (λ u Σ (C X) (λ v u = v ∘ horizontal-map-cocone f g c))
by
equiv-tot
( λ u
equiv-tot
( λ v
inv-equiv-ap-is-emb (is-epimorphism-is-acyclic-map f ac X)))
≃ Σ (C X) (λ v Σ (A X) (λ u u = v ∘ horizontal-map-cocone f g c))
by
equiv-left-swap-Σ
≃ (C X)
by
equiv-pr1 (λ v is-torsorial-path' (v ∘ horizontal-map-cocone f g c))

is-acyclic-map-vertical-map-cocone-is-pushout :
is-pushout f g c
is-acyclic-map f
is-acyclic-map (vertical-map-cocone f g c)
is-acyclic-map-vertical-map-cocone-is-pushout po ac =
is-acyclic-map-is-epimorphism
( vertical-map-cocone f g c)
( is-epimorphism-universal-property-pushout
( vertical-map-cocone f g c)
( universal-property-pushout-right-universal-property-pushout-rectangle
( f)
( g)
( vertical-map-cocone f g c)
( c)
( cocone-codiagonal-map (vertical-map-cocone f g c))
( universal-property-pushout-is-pushout f g c po)
( λ X
is-equiv-right-factor
( map-equiv (equiv-cocone-postcomp-vertical-map-cocone ac X))
( cocone-map f
( vertical-map-cocone f g c ∘ g)
( cocone-comp-horizontal f g
( vertical-map-cocone f g c)
( c)
( cocone-codiagonal-map (vertical-map-cocone f g c))))
( is-equiv-map-equiv
( equiv-cocone-postcomp-vertical-map-cocone ac X))
( is-equiv-id))))

module _
{l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
{C : UU l4} (f : S A) (g : S B) (c : cocone f g C)
where

is-acyclic-map-horizontal-map-cocone-is-pushout :
is-pushout f g c
is-acyclic-map g
is-acyclic-map (horizontal-map-cocone f g c)
is-acyclic-map-horizontal-map-cocone-is-pushout po =
is-acyclic-map-vertical-map-cocone-is-pushout g f
( swap-cocone f g C c)
( is-pushout-swap-cocone-is-pushout f g C c po)
```

### Acyclic maps are closed under pullbacks

```agda
module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
{X : UU l4} (f : A X) (g : B X) (c : cone f g C)
where

is-acyclic-map-vertical-map-cone-is-pullback :
is-pullback f g c
is-acyclic-map g
is-acyclic-map (vertical-map-cone f g c)
is-acyclic-map-vertical-map-cone-is-pullback pb ac a =
is-acyclic-equiv
( map-fiber-cone f g c a ,
is-fiberwise-equiv-map-fiber-cone-is-pullback f g c pb a)
( ac (f a))

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
{X : UU l4} (f : A X) (g : B X) (c : cone f g C)
where

is-acyclic-map-horizontal-map-cone-is-pullback :
is-pullback f g c
is-acyclic-map f
is-acyclic-map (horizontal-map-cone f g c)
is-acyclic-map-horizontal-map-cone-is-pullback pb =
is-acyclic-map-vertical-map-cone-is-pullback g f
( swap-cone f g c)
( is-pullback-swap-cone f g c pb)
```

### Acyclic types are closed under dependent pair types

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

is-acyclic-Σ :
is-acyclic A ((a : A) is-acyclic (B a)) is-acyclic (Σ A B)
is-acyclic-Σ ac-A ac-B =
is-acyclic-is-acyclic-map-terminal-map
( Σ A B)
( is-acyclic-map-comp
( terminal-map)
( pr1)
( is-acyclic-map-terminal-map-is-acyclic A ac-A)
( λ a is-acyclic-equiv (equiv-fiber-pr1 B a) (ac-B a)))
```

### Acyclic types are closed under binary products

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

is-acyclic-prod :
is-acyclic A is-acyclic B is-acyclic (A × B)
is-acyclic-prod ac-A ac-B =
is-acyclic-is-acyclic-map-terminal-map
( A × B)
( is-acyclic-map-comp
( terminal-map)
( pr2)
( is-acyclic-map-terminal-map-is-acyclic B ac-B)
( is-acyclic-map-horizontal-map-cone-is-pullback
( terminal-map)
( terminal-map)
( cone-prod A B)
( is-pullback-prod A B)
( is-acyclic-map-terminal-map-is-acyclic A ac-A)))
```

### Inhabited, locally acyclic types are acyclic

```agda
module _
{l : Level} (A : UU l)
where

is-acyclic-inhabited-is-acyclic-Id :
is-inhabited A
((a b : A) is-acyclic (a = b))
is-acyclic A
is-acyclic-inhabited-is-acyclic-Id h l-ac =
apply-universal-property-trunc-Prop h
( is-acyclic-Prop A)
( λ a
is-acyclic-is-acyclic-map-terminal-map A
( is-acyclic-map-left-factor
( terminal-map)
( point a)
( is-acyclic-map-terminal-map-is-acyclic unit is-acyclic-unit)
( λ b is-acyclic-equiv (fiber-const a b) (l-ac a b))))
```

## See also

- [Dependent epimorphisms](foundation.dependent-epimorphisms.md)
Expand Down
11 changes: 11 additions & 0 deletions src/synthetic-homotopy-theory/acyclic-types.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ open import foundation.contractible-types
open import foundation.equivalences
open import foundation.propositions
open import foundation.retracts-of-types
open import foundation.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.functoriality-suspensions
Expand Down Expand Up @@ -67,6 +68,16 @@ module _
is-contr-retract-of (suspension B) (retract-of-suspension-retract-of R) ac
```

### Contractible types are acyclic

```agda
is-acyclic-is-contr : {l : Level} (A : UU l) is-contr A is-acyclic A
is-acyclic-is-contr A = is-contr-suspension-is-contr

is-acyclic-unit : is-acyclic unit
is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit
```

## See also

- [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)
Expand Down
48 changes: 48 additions & 0 deletions src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -393,3 +393,51 @@ module _
pr1 (pr2 cocone-hom-arrow) = g
pr2 (pr2 cocone-hom-arrow) = coh-hom-arrow f g h
```

### The swapping function on cocones over spans

```agda
module _
{l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
(f : S A) (g : S B) (X : UU l4)
where

swap-cocone : cocone f g X cocone g f X
pr1 (swap-cocone c) = vertical-map-cocone f g c
pr1 (pr2 (swap-cocone c)) = horizontal-map-cocone f g c
pr2 (pr2 (swap-cocone c)) = inv-htpy (coherence-square-cocone f g c)

module _
{l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
(f : S A) (g : S B) (X : UU l4)
where

is-involution-swap-cocone : swap-cocone g f X ∘ swap-cocone f g X ~ id
is-involution-swap-cocone c =
eq-htpy-cocone f g
( swap-cocone g f X (swap-cocone f g X c))
( c)
( ( refl-htpy) ,
( refl-htpy) ,
( λ s
concat
( right-unit)
( coherence-square-cocone f g c s)
( inv-inv (coherence-square-cocone f g c s))))

module _
{l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
(f : S A) (g : S B) (X : UU l4)
where

is-equiv-swap-cocone : is-equiv (swap-cocone f g X)
is-equiv-swap-cocone =
is-equiv-is-invertible
( swap-cocone g f X)
( is-involution-swap-cocone g f X)
( is-involution-swap-cocone f g X)

equiv-swap-cocone : cocone f g X ≃ cocone g f X
pr1 equiv-swap-cocone = swap-cocone f g X
pr2 equiv-swap-cocone = is-equiv-swap-cocone
```
Loading

0 comments on commit f4e8b21

Please sign in to comment.