diff --git a/Mathlib.lean b/Mathlib.lean
index fb50e03194434..5df6e1d33a8be 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -300,6 +300,7 @@ import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 import Mathlib.AlgebraicTopology.CechNerve
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility
 import Mathlib.AlgebraicTopology.DoldKan.Decomposition
+import Mathlib.AlgebraicTopology.DoldKan.Degeneracies
 import Mathlib.AlgebraicTopology.DoldKan.Faces
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 import Mathlib.AlgebraicTopology.DoldKan.Homotopies
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean b/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
new file mode 100644
index 0000000000000..3f2c356ccf1ef
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+
+! This file was ported from Lean 3 source module algebraic_topology.dold_kan.degeneracies
+! leanprover-community/mathlib commit ec1c7d810034d4202b0dd239112d1792be9f6fdc
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.AlgebraicTopology.DoldKan.Decomposition
+import Mathlib.Tactic.FinCases
+
+/-!
+
+# Behaviour of P_infty with respect to degeneracies
+
+For any `X : SimplicialObject C` where `C` is an abelian category,
+the projector `PInfty : K[X] ⟶ K[X]` is supposed to be the projection
+on the normalized subcomplex, parallel to the degenerate subcomplex, i.e.
+the subcomplex generated by the images of all `X.σ i`.
+
+In this file, we obtain `degeneracy_comp_P_infty` which states that
+if `X : SimplicialObject C` with `C` a preadditive category,
+`θ : [n] ⟶ Δ'` is a non injective map in `SimplexCategory`, then
+`X.map θ.op ≫ P_infty.f n = 0`. It follows from the more precise
+statement vanishing statement `σ_comp_P_eq_zero` for the `P q`.
+
+-/
+
+
+open CategoryTheory CategoryTheory.Category CategoryTheory.Limits
+  CategoryTheory.Preadditive Simplicial
+
+namespace AlgebraicTopology
+
+namespace DoldKan
+
+variable {C : Type _} [Category C] [Preadditive C]
+
+theorem HigherFacesVanish.comp_σ {Y : C} {X : SimplicialObject C} {n b q : ℕ} {φ : Y ⟶ X _[n + 1]}
+    (v : HigherFacesVanish q φ) (hnbq : n + 1 = b + q) :
+    HigherFacesVanish q
+      (φ ≫
+        X.σ ⟨b, by
+          simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]⟩) :=
+  fun j hj => by
+  rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
+    zero_comp]
+  . dsimp
+    rw [Fin.lt_iff_val_lt_val, Fin.val_succ]
+    linarith
+  . intro hj'
+    simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right,
+      nonpos_iff_eq_zero, add_eq_zero, false_and] at hj
+#align algebraic_topology.dold_kan.higher_faces_vanish.comp_σ AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ
+
+theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1)) (hi : n + 1 ≤ i + q) :
+    X.σ i ≫ (P q).f (n + 1) = 0 := by
+  revert i hi
+  induction' q with q hq
+  . intro i (hi : n + 1 ≤ i)
+    exfalso
+    linarith [Fin.is_lt i]
+  · intro i (hi : n + 1 ≤ i + q + 1)
+    by_cases n + 1 ≤ (i : ℕ) + q
+    . rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
+    . replace hi : n = i + q := by
+        obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
+        rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right,
+          nonpos_iff_eq_zero] at h
+        rw [← add_left_inj 1, hj, self_eq_add_right, h]
+      rcases n with _|n
+      . fin_cases i
+        dsimp at h hi
+        rw [show q = 0 by linarith]
+        change X.σ 0 ≫ (P 1).f 1 = 0
+        simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
+          HomologicalComplex.id_f, AlternatingFaceMapComplex.obj_d_eq, Hσ,
+          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
+          comp_id]
+        erw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm, comp_id, Fin.sum_univ_two,
+          Fin.sum_univ_succ, Fin.sum_univ_two]
+        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.mk_one,
+          Fin.val_succ, Fin.val_one, Fin.succ_one_eq_two, P_zero, HomologicalComplex.id_f,
+          Fin.val_two, pow_two, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp,
+          comp_add, Fin.mk_zero, neg_comp, comp_neg, Fin.succ_zero_eq_one]
+        erw [SimplicialObject.δ_comp_σ_self, SimplicialObject.δ_comp_σ_self_assoc,
+          SimplicialObject.δ_comp_σ_succ, comp_id,
+          SimplicialObject.δ_comp_σ_of_le X
+            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
+          SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ_assoc]
+        simp only [add_right_neg, add_zero, zero_add]
+      · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
+          P_succ]
+        have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
+          (HigherFacesVanish.of_P q n).comp_σ hi
+        erw [← assoc, v.comp_P_eq_self, HomologicalComplex.add_f_apply, Preadditive.comp_add,
+          comp_id, v.comp_Hσ_eq hi, assoc, SimplicialObject.δ_comp_σ_succ_assoc, Fin.eta,
+          decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero, add_neg_eq_zero]
+        intro j hj
+        simp only [true_and_iff, Finset.mem_univ, Finset.mem_filter] at hj
+        simp only [Nat.succ_eq_add_one] at hi
+        obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
+        rw [add_comm] at hk
+        have hi' : i = Fin.castSucc ⟨i, by linarith⟩ := by
+          ext
+          simp only [Fin.castSucc_mk, Fin.eta]
+        have eq := hq j.rev.succ (by
+          simp only [← hk, Fin.rev_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
+          linarith)
+        rw [HomologicalComplex.comp_f, assoc, assoc, assoc, hi',
+          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
+          comp_zero]
+        simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val, Fin.val_mk]
+        linarith
+set_option linter.uppercaseLean3 false in
+#align algebraic_topology.dold_kan.σ_comp_P_eq_zero AlgebraicTopology.DoldKan.σ_comp_P_eq_zero
+
+@[reassoc (attr := simp)]
+theorem σ_comp_PInfty (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) :
+    X.σ i ≫ PInfty.f (n + 1) = 0 := by
+  rw [PInfty_f, σ_comp_P_eq_zero X i]
+  simp only [le_add_iff_nonneg_left, zero_le]
+set_option linter.uppercaseLean3 false in
+#align algebraic_topology.dold_kan.σ_comp_P_infty AlgebraicTopology.DoldKan.σ_comp_PInfty
+
+@[reassoc]
+theorem degeneracy_comp_PInfty (X : SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory}
+    (θ : ([n] : SimplexCategory) ⟶ Δ') (hθ : ¬Mono θ) : X.map θ.op ≫ PInfty.f n = 0 := by
+  rw [SimplexCategory.mono_iff_injective] at hθ
+  cases n
+  . exfalso
+    apply hθ
+    intro x y h
+    fin_cases x
+    fin_cases y
+    rfl
+  . obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
+    rw [h, op_comp, X.map_comp, assoc, show X.map (SimplexCategory.σ i).op = X.σ i by rfl,
+      σ_comp_PInfty, comp_zero]
+set_option linter.uppercaseLean3 false in
+#align algebraic_topology.dold_kan.degeneracy_comp_P_infty AlgebraicTopology.DoldKan.degeneracy_comp_PInfty
+
+end DoldKan
+
+end AlgebraicTopology