chore: fix SHA for Dold-Kan equivalence files (#6834)

leanprover-community · Aug 28, 2023 · cf01bda · cf01bda
1 parent 837c4ae
commit cf01bda
Show file tree

Hide file tree

Showing 17 changed files with 17 additions and 17 deletions.
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Equivalence
 
-#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"18ee599842a5d17f189fe572f0ed8cb1d064d772"
+#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! Tools for compatibilities between Dold-Kan equivalences
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 
-#align_import algebraic_topology.dold_kan.decomposition from "leanprover-community/mathlib"@"9af20344b24ef1801b599d296aaed8b9fffdc360"
+#align_import algebraic_topology.dold_kan.decomposition from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean b/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.Decomposition
 import Mathlib.Tactic.FinCases
 
-#align_import algebraic_topology.dold_kan.degeneracies from "leanprover-community/mathlib"@"ec1c7d810034d4202b0dd239112d1792be9f6fdc"
+#align_import algebraic_topology.dold_kan.degeneracies from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.NCompGamma
 
-#align_import algebraic_topology.dold_kan.equivalence_additive from "leanprover-community/mathlib"@"19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e"
+#align_import algebraic_topology.dold_kan.equivalence_additive from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The Dold-Kan equivalence for additive categories.
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility
 import Mathlib.CategoryTheory.Idempotents.SimplicialObject
 
-#align_import algebraic_topology.dold_kan.equivalence_pseudoabelian from "leanprover-community/mathlib"@"63721b2c3eba6c325ecf8ae8cca27155a4f6306f"
+#align_import algebraic_topology.dold_kan.equivalence_pseudoabelian from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.Homotopies
 
-#align_import algebraic_topology.dold_kan.faces from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
+#align_import algebraic_topology.dold_kan.faces from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
 
-#align_import algebraic_topology.dold_kan.functor_gamma from "leanprover-community/mathlib"@"5b8284148e8149728f4b90624888d98c36284454"
+#align_import algebraic_topology.dold_kan.functor_gamma from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 
-#align_import algebraic_topology.dold_kan.functor_n from "leanprover-community/mathlib"@"1995c7bbdbb0adb1b6d5acdc654f6cf46ed96cfa"
+#align_import algebraic_topology.dold_kan.functor_n from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
 import Mathlib.CategoryTheory.Idempotents.HomologicalComplex
 
-#align_import algebraic_topology.dold_kan.gamma_comp_n from "leanprover-community/mathlib"@"5f68029a863bdf76029fa0f7a519e6163c14152e"
+#align_import algebraic_topology.dold_kan.gamma_comp_n from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The counit isomorphism of the Dold-Kan equivalence
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.GammaCompN
 import Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
 
-#align_import algebraic_topology.dold_kan.n_comp_gamma from "leanprover-community/mathlib"@"19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e"
+#align_import algebraic_topology.dold_kan.n_comp_gamma from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The unit isomorphism of the Dold-Kan equivalence
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean b/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
@@ -8,7 +8,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Decomposition
 import Mathlib.CategoryTheory.Idempotents.HomologicalComplex
 import Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
 
-#align_import algebraic_topology.dold_kan.n_reflects_iso from "leanprover-community/mathlib"@"88bca0ce5d22ebfd9e73e682e51d60ea13b48347"
+#align_import algebraic_topology.dold_kan.n_reflects_iso from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 
-#align_import algebraic_topology.dold_kan.normalized from "leanprover-community/mathlib"@"d1d69e99ed34c95266668af4e288fc1c598b9a7f"
+#align_import algebraic_topology.dold_kan.normalized from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Notations.lean b/Mathlib/AlgebraicTopology/DoldKan/Notations.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 
-#align_import algebraic_topology.dold_kan.notations from "leanprover-community/mathlib"@"3d7987cda72abc473c7cdbbb075170e9ac620042"
+#align_import algebraic_topology.dold_kan.notations from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean b/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Projections
 import Mathlib.CategoryTheory.Idempotents.FunctorCategories
 import Mathlib.CategoryTheory.Idempotents.FunctorExtension
 
-#align_import algebraic_topology.dold_kan.p_infty from "leanprover-community/mathlib"@"31019c2504b17f85af7e0577585fad996935a317"
+#align_import algebraic_topology.dold_kan.p_infty from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Projections.lean b/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.Faces
 import Mathlib.CategoryTheory.Idempotents.Basic
 
-#align_import algebraic_topology.dold_kan.projections from "leanprover-community/mathlib"@"ed98c07faf6d9de3e52771d5b00394c4294ccb4d"
+#align_import algebraic_topology.dold_kan.projections from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.DoldKan.Degeneracies
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 
-#align_import algebraic_topology.dold_kan.split_simplicial_object from "leanprover-community/mathlib"@"31019c2504b17f85af7e0577585fad996935a317"
+#align_import algebraic_topology.dold_kan.split_simplicial_object from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 

diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean
@@ -6,7 +6,7 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Iso
 
-#align_import category_theory.functor.category from "leanprover-community/mathlib"@"8350c34a64b9bc3fc64335df8006bffcadc7baa6"
+#align_import category_theory.functor.category from "leanprover-community/mathlib"@"63721b2c3eba6c325ecf8ae8cca27155a4f6306f"
 
 /-!
 # The category of functors and natural transformations between two fixed categories.