Acyclic maps are closed under retracts (#1113)

Easy corollary as @fredrik-bakke added retracts of maps to the library
UniMath · Apr 14, 2024 · ac75d87 · ac75d87
1 parent aab86e6
commit ac75d87
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 1 deletion.
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -34,6 +34,7 @@ open import foundation.precomposition-functions
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.pullbacks
+open import foundation.retracts-of-maps
 open import foundation.torsorial-type-families
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-arithmetic-unit-type
@@ -528,6 +529,22 @@ module _
             ( λ b → is-acyclic-equiv (compute-fiber-point a b) (l-ac a b))))
 ```
 
+### Acyclic maps are closed under retracts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-acyclic-map-retract-of :
+    f retract-of-map g → is-acyclic-map g → is-acyclic-map f
+  is-acyclic-map-retract-of R ac b =
+    is-acyclic-retract-of
+      ( retract-fiber-retract-map f g R b)
+      ( ac (map-codomain-inclusion-retract-map f g R b))
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)

diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
@@ -35,6 +35,7 @@ open import foundation.precomposition-functions
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.pullbacks
+open import foundation.retracts-of-maps
 open import foundation.torsorial-type-families
 open import foundation.truncated-types
 open import foundation.truncation-equivalences
@@ -513,7 +514,25 @@ module _
                 ( l-ac a b))))
 ```
 
-### Acyclic maps are closed under pushouts
+### `k`-acyclic maps are closed under retracts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-truncated-acyclic-map-retract-of :
+    f retract-of-map g →
+    is-truncated-acyclic-map k g →
+    is-truncated-acyclic-map k f
+  is-truncated-acyclic-map-retract-of R ac b =
+    is-truncated-acyclic-retract-of
+      ( retract-fiber-retract-map f g R b)
+      ( ac (map-codomain-inclusion-retract-map f g R b))
+```
+
+### `k`-acyclic maps are closed under pushouts
 
 **Proof:** We consider the pushout squares