[Merged by Bors] - feat(AlgebraicTopology): simplicial homology

Mathlib.lean

@@ -1523,6 +1523,8 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Finite
 public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
 public import Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
 public import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
 public import Mathlib.AlgebraicTopology.SimplicialSet.Horn
@@ -1553,7 +1555,6 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
 public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
-public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
 public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat
 public import Mathlib.AlgebraicTopology.SingularSet
 public import Mathlib.AlgebraicTopology.TopologicalSimplex

Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+public import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
+public import Mathlib.CategoryTheory.Linear.Basic
+
+/-!
+# Simplicial homology
+
+In this file, we define the homology of simplicial sets.
+For any preadditive category `C` with coproducts of size `w` and any
+object `R : C`, the simplicial chain complex of a simplicial
+set `X` is denoted `X.chainComplex R`, and its homology
+in degree `n : ℕ` is `X.homology R n`.
+
+-/
+
+@[expose] public section
+
+open Simplicial CategoryTheory Limits
+
+universe w v u
+
+namespace SSet
+
+variable (C : Type u) [Category.{v} C] [HasCoproducts.{w} C] [Preadditive C]
+
+/--
+The chain complex associated to a simplicial set, with coefficients in `R : C`.
+It computes the simplicial homology of a simplicial sets with coefficients
+in `R`. One can recover the ordinary simplicial chain complex when `C := Ab`
+and `X := ℤ`.
+-/
+noncomputable def chainComplexFunctor : C ⥤ SSet.{w} ⥤ ChainComplex C ℕ :=
+  (Functor.postcompose₂.obj (AlgebraicTopology.alternatingFaceMapComplex _)).obj
+    (sigmaConst ⋙ SimplicialObject.whiskering _ _)
+
+instance : (chainComplexFunctor C).Additive := by
+  dsimp [chainComplexFunctor, SimplicialObject.whiskering]
+  infer_instance
+
+@[deprecated (since := "2026-04-05")]
+alias _root_.AlgebraicTopology.SSet.singularChainComplexFunctor :=
+  chainComplexFunctor
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local simp] SSet.chainComplexFunctor in
+attribute [local simp←] _root_.SSet.yonedaEquiv_symm_comp in
+/-- The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `R : C` and `F : SSet ⥤ C`. -/
+noncomputable def chainComplexFunctorAdjunction (n : ℕ) :
+    (Functor.postcompose₂.obj (HomologicalComplex.eval _ _ n)).obj
+      (SSet.chainComplexFunctor C) ⊣ (evaluation _ _).obj Δ[n] where
+  unit.app R := Sigma.ι (fun _ : Δ[n] _⦋n⦌ ↦ R) (SSet.stdSimplex.objEquiv (n := ⦋n⦌).symm (𝟙 ⦋n⦌))
+  counit.app F := { app S := Sigma.desc fun α ↦ F.map (SSet.yonedaEquiv.symm α) }
+  right_triangle_components F := by dsimp; simp
+
+@[deprecated (since := "2026-04-05")]
+alias _root_.SSet.singularChainComplexFunctorAdjunction :=
+  SSet.chainComplexFunctorAdjunction
+
+variable {C} (X Y Z : SSet.{w}) (f : X ⟶ Y) (g : Y ⟶ Z) (R : C)
+
+/-- The (simplicial) chain complex of a simplicial set `X` with
+coefficients in `R : C`. Its homology is the simplicial homology
+of `X`. -/
+noncomputable abbrev chainComplex : ChainComplex C ℕ :=
+  ((SSet.chainComplexFunctor C).obj R).obj X
+
+variable {X Y} in
+/-- The morphism of simplicial chain complexes induces by a morphism
+of simplicial sets. -/
+noncomputable abbrev chainComplexMap : X.chainComplex R ⟶ Y.chainComplex R :=
+  ((SSet.chainComplexFunctor C).obj R).map f
+
+variable {R} in
+/-- The inclusion `R ⟶ (X.chainComplex R).X n` of the summand
+corresponding to a `n`-simplex `x : X _⦋n⦌`. -/
+noncomputable def ιChainComplex {n : ℕ} (x : X _⦋n⦌) : R ⟶ (X.chainComplex R).X n :=
+  Sigma.ι (fun (_ : X _⦋n⦌) ↦ R) x
+
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc (attr := simp)]
+lemma ιChainComplex_d {n : ℕ} (x : X _⦋n + 1⦌) :
+    X.ιChainComplex x ≫ (X.chainComplex R).d (n + 1) n =
+      ∑ (i : Fin (n + 2)), (-1) ^ i.val • X.ιChainComplex (X.δ i x) := by
+  simp [ιChainComplex, chainComplex, chainComplexFunctor, Preadditive.comp_sum]
+
+@[reassoc (attr := simp)]
+lemma ι_chainComplexMap_f {n : ℕ} (x : X _⦋n⦌) :
+    X.ιChainComplex x ≫ (chainComplexMap f R).f n =
+      Y.ιChainComplex (f.app _ x) := by
+  dsimp [chainComplexMap, chainComplexFunctor, ιChainComplex, Sigma.map',
+    chainComplex, chainComplexFunctor]
+  simp [Sigma.ι_desc]
+
+/-- The colimit cofan which defines the simplicial `n`-chains
+`(X.chainComplex R).X n`. -/
+noncomputable def chainComplexXCofan (n : ℕ) : Cofan (fun (_ : X _⦋n⦌) ↦ R) :=
+  Cofan.mk _ X.ιChainComplex
+
+/-- Simplicial `n`-chains `(X.chainComplex R).X n` of a simplicial set `X`
+with coefficients in `R` identify to a coproduct of copies of `R`
+indexed by `X _⦋n⦌`. -/
+noncomputable def isColimitChainComplexXCofan (n : ℕ) : IsColimit (X.chainComplexXCofan R n) :=
+  coproductIsCoproduct _
+
+variable {X R} in
+@[ext]
+lemma chainComplex_hom_ext {n : ℕ} {T : C} {f g : (X.chainComplex R).X n ⟶ T}
+    (h : ∀ (x : X _⦋n⦌), X.ιChainComplex x ≫ f = X.ιChainComplex x ≫ g) :
+    f = g :=
+  (X.isColimitChainComplexXCofan R n).hom_ext (fun _ ↦ h _)
+
+variable [CategoryWithHomology C]
+
+/-- The simplicial homology with coefficients in `R : C` in degree `n`
+of a simplicial set `X`. -/
+protected noncomputable abbrev homology (n : ℕ) : C := (X.chainComplex R).homology n
+
+variable {X Y} in
+/-- The morphism in simplicial homology that is induced by a morphism
+of simplicial sets. -/
+protected noncomputable abbrev homologyMap (n : ℕ) : X.homology R n ⟶ Y.homology R n :=
+  HomologicalComplex.homologyMap (chainComplexMap f R) n
+
+@[simp]
+lemma homologyMap_id (n : ℕ) : SSet.homologyMap (𝟙 X) R n = 𝟙 _ := by
+  simp [SSet.homologyMap]
+
+@[reassoc]
+lemma homologyMap_comp (n : ℕ) :
+    SSet.homologyMap (f ≫ g) R n = SSet.homologyMap f R n ≫ SSet.homologyMap g R n := by
+  simp [SSet.homologyMap, HomologicalComplex.homologyMap_comp]
+
+attribute [local simp] homologyMap_comp in
+/-- The simplicial homology functor in degree `n` with coefficients in `R : C`. -/
+@[simps]
+noncomputable def homologyFunctor (n : ℕ) : SSet.{w} ⥤ C where
+  obj X := X.homology R n
+  map f := SSet.homologyMap f R n
+
+end SSet

Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean → Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean

@@ -5,13 +5,12 @@ Authors: Fabian Odermatt, Joël Riou
 -/
 module
 
-public import Mathlib.AlgebraicTopology.SingularHomology.Basic
-public import Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
 public import Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
 
 /-!
-# Homotopy invariance of singular homology (simplicial step)
+# Homotopy invariance of simplicial homology
 
 This file proves that homotopic morphisms of simplicial sets induce
 the same maps on singular homology (with coefficients in an object `R`
@@ -39,6 +38,11 @@ using the definition `SSet.Homotopy.toSimplicialObjectHomotopy` from the file
 
 @[expose] public section
 
+/-! The invariance of singular homology (of topological spaces)
+is obtained in the file
+`Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvarianceTopCat.lean`. -/
+assert_not_exists TopologicalSpace
+
 universe v u w
 
 open CategoryTheory Limits AlgebraicTopology.SSet
@@ -52,37 +56,41 @@ namespace CategoryTheory.SimplicialObject.Homotopy
 If `f` and `g` are simplicially homotopic maps of simplicial sets,
 then they induce chain-homotopic maps on the singular chain complexes
 with coefficients in `R`. The assumption is in `SimplicialObject.Homotopy`,
-see also `SSet.Homotopy.singularChainComplexFunctorObjMap` for the
+see also `SSet.Homotopy.chainComplexMap` for the
 variant using `SSet.Homotopy` as an assumption.
 -/
-noncomputable def singularChainComplexFunctorObjMap
+noncomputable def sSetChainComplexMap
     (H : SimplicialObject.Homotopy f g) (R : C) :
-    _root_.Homotopy
-      (((singularChainComplexFunctor C).obj R).map f)
-      (((singularChainComplexFunctor C).obj R).map g) :=
+    _root_.Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R) :=
   toChainHomotopy (H.whiskerRight _)
 
+@[deprecated (since := "2026-04-05")]
+alias singularChainComplexFunctorObjMap :=
+  sSetChainComplexMap
+
 @[deprecated (since := "2026-03-24")]
 alias _root_.singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy :=
-  Homotopy.singularChainComplexFunctorObjMap
+  sSetChainComplexMap
 
 open HomologicalComplex in
 /--
 Simplicially homotopic maps of simplicial sets induce the same map on
 homology of the singular chain complex (with coefficients in `R`).
 The assumption is in `SimplicialObject.Homotopy`,
-see also `SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor` for the
+see also `SSet.Homotopy.congr_homologyMap` for the
 variant using `SSet.Homotopy` as an assumption.
 -/
-theorem congr_homologyMap_singularChainComplexFunctor [CategoryWithHomology C]
+theorem congr_sSetHomologyMap [CategoryWithHomology C]
     (H : SimplicialObject.Homotopy f g) (R : C) (n : ℕ) :
-    homologyMap (((singularChainComplexFunctor C).obj R).map f) n =
-    homologyMap (((singularChainComplexFunctor C).obj R).map g) n :=
-  (H.singularChainComplexFunctorObjMap R).homologyMap_eq n
+    SSet.homologyMap f R n = SSet.homologyMap g R n :=
+  (H.sSetChainComplexMap R).homologyMap_eq n
 
 @[deprecated (since := "2026-03-24")]
 alias singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy :=
-  congr_homologyMap_singularChainComplexFunctor
+  congr_sSetHomologyMap
+
+@[deprecated (since := "2026-04-05")] alias congr_homologyMap_singularChainComplexFunctor :=
+  congr_sSetHomologyMap
 
 end CategoryTheory.SimplicialObject.Homotopy
 
@@ -92,22 +100,25 @@ namespace SSet.Homotopy
 If `f` and `g` are homotopic maps of simplicial sets, then they induce chain-homotopic
 maps on the singular chain complexes with coefficients in `R`.
 -/
-noncomputable def singularChainComplexFunctorObjMap
+noncomputable def chainComplexMap
     (H : SSet.Homotopy f g) (R : C) :
-    _root_.Homotopy
-      (((singularChainComplexFunctor C).obj R).map f)
-      (((singularChainComplexFunctor C).obj R).map g) :=
-  H.toSimplicialObjectHomotopy.singularChainComplexFunctorObjMap R
+    _root_.Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)  :=
+  H.toSimplicialObjectHomotopy.sSetChainComplexMap R
+
+@[deprecated (since := "2026-04-05")]
+alias singularChainComplexFunctorObjMap := chainComplexMap
 
 open HomologicalComplex in
 /--
 Homotopic maps of simplicial sets induce the same map on homology of the singular
 chain complex (with coefficients in `R`).
 -/
-theorem congr_homologyMap_singularChainComplexFunctor [CategoryWithHomology C]
+theorem congr_homologyMap [CategoryWithHomology C]
     (H : SSet.Homotopy f g) (R : C) (n : ℕ) :
-    homologyMap (((singularChainComplexFunctor C).obj R).map f) n =
-    homologyMap (((singularChainComplexFunctor C).obj R).map g) n :=
-  (H.singularChainComplexFunctorObjMap R).homologyMap_eq n
+    SSet.homologyMap f R n = SSet.homologyMap g R n :=
+  (H.chainComplexMap R).homologyMap_eq n
+
+@[deprecated (since := "2026-04-05")]
+alias congr_homologyMap_singularChainComplexFunctor := congr_homologyMap
 
 end SSet.Homotopy

Mathlib/AlgebraicTopology/SingularHomology/Basic.lean

@@ -6,6 +6,7 @@ Authors: Andrew Yang
 module
 
 public import Mathlib.Algebra.Homology.AlternatingConst
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
 public import Mathlib.AlgebraicTopology.SingularSet
 public import Mathlib.CategoryTheory.Adjunction.Whiskering
 public import Mathlib.CategoryTheory.Limits.MonoCoprod
@@ -31,23 +32,10 @@ universe w v u
 variable (C : Type u) [Category.{v} C] [HasCoproducts.{w} C]
 variable [Preadditive C] (n : ℕ)
 
-/--
-The singular chain complex associated to a simplicial set, with coefficients in `X : C`.
-One can recover the ordinary singular chain complex when `C := Ab` and `X := ℤ`.
--/
-def SSet.singularChainComplexFunctor :
-    C ⥤ SSet.{w} ⥤ ChainComplex C ℕ :=
-  (Functor.postcompose₂.obj (AlgebraicTopology.alternatingFaceMapComplex _)).obj
-    (sigmaConst ⋙ SimplicialObject.whiskering _ _)
-
-instance : (SSet.singularChainComplexFunctor C).Additive := by
-  dsimp [SSet.singularChainComplexFunctor, SimplicialObject.whiskering]
-  infer_instance
-
 /-- The singular chain complex functor with coefficients in `C`. -/
 def singularChainComplexFunctor :
     C ⥤ TopCat.{w} ⥤ ChainComplex C ℕ :=
-  SSet.singularChainComplexFunctor.{w} C ⋙ (Functor.whiskeringLeft _ _ _).obj TopCat.toSSet.{w}
+  SSet.chainComplexFunctor.{w} C ⋙ (Functor.whiskeringLeft _ _ _).obj TopCat.toSSet.{w}
 
 instance : (singularChainComplexFunctor C).Additive := by
   delta singularChainComplexFunctor
@@ -56,7 +44,7 @@ instance : (singularChainComplexFunctor C).Additive := by
 instance [Limits.HasPullbacks C] {X : C} :
     ((singularChainComplexFunctor C).obj X).PreservesMonomorphisms where
   preserves f _ := by
-    dsimp [singularChainComplexFunctor, SSet.singularChainComplexFunctor]
+    dsimp [singularChainComplexFunctor, SSet.chainComplexFunctor]
     apply +allowSynthFailures Functor.map_mono
     apply +allowSynthFailures Functor.map_mono
     dsimp [SSet, SimplicialObject.whiskering, SimplicialObject]
@@ -73,20 +61,10 @@ open Limits _root_.SSet
 open scoped Simplicial
 open HomologicalComplex (eval)
 
-set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] SSet.singularChainComplexFunctor in
-attribute [local simp←] _root_.SSet.yonedaEquiv_symm_comp in
-/-- The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `X : C` and `F : SSet ⥤ C`. -/
-def SSet.singularChainComplexFunctorAdjunction : (Functor.postcompose₂.obj (eval _ _ n)).obj
-    (SSet.singularChainComplexFunctor C) ⊣ (evaluation _ _).obj Δ[n] where
-  unit.app R := Sigma.ι (fun _ : Δ[n] _⦋n⦌ ↦ R) (SSet.stdSimplex.objEquiv (n := ⦋n⦌).symm (𝟙 ⦋n⦌))
-  counit.app F := { app S := Sigma.desc fun α ↦ F.map (SSet.yonedaEquiv.symm α) }
-  right_triangle_components F := by dsimp; simp
-
 /-- The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `X : C` and `F : Top ⥤ C`. -/
 def singularChainComplexFunctorAdjunction : (Functor.postcompose₂.obj (eval _ _ n)).obj
     (singularChainComplexFunctor C) ⊣ (evaluation _ _).obj (SimplexCategory.toTop.obj ⦋n⦌) :=
-  ((SSet.singularChainComplexFunctorAdjunction C n).comp (sSetTopAdj.whiskerLeft _)).ofNatIsoRight
+  ((SSet.chainComplexFunctorAdjunction C n).comp (sSetTopAdj.whiskerLeft _)).ofNatIsoRight
     ((evaluation TopCat C).mapIso (SSet.toTopSimplex.app _))
 
 lemma singularChainComplexFunctorAdjunction_unit_app (R : C) :
@@ -96,7 +74,7 @@ lemma singularChainComplexFunctorAdjunction_unit_app (R : C) :
   dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
     Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
     Adjunction.comp, singularChainComplexFunctor,
-    SSet.singularChainComplexFunctorAdjunction, SSet.singularChainComplexFunctor]
+    SSet.chainComplexFunctorAdjunction, SSet.chainComplexFunctor]
   simp [stdSimplexToTop]
 
 set_option backward.isDefEq.respectTransparency false in
@@ -107,8 +85,8 @@ lemma ι_singularChainComplexFunctorAdjunction_counit_app_app (F : TopCat ⥤ C)
       sSetTopAdj.counit.app X)
   · dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
       Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
-      Adjunction.comp, singularChainComplexFunctor, SSet.singularChainComplexFunctor,
-      SSet.singularChainComplexFunctorAdjunction]
+      Adjunction.comp, singularChainComplexFunctor, SSet.chainComplexFunctor,
+      SSet.chainComplexFunctorAdjunction]
     simp
   · congr 1
     rw [← reassoc_of% sSetTopAdj_unit_app_app_down]

Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvarianceTopCat.lean

@@ -5,7 +5,8 @@ Authors: Joël Riou, Fabian Odermatt
 -/
 module
 
-public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
+public import Mathlib.AlgebraicTopology.SingularHomology.Basic
 public import Mathlib.Topology.Homotopy.TopCat.ToSSet
 
 /-!
@@ -48,7 +49,7 @@ an object of the category of abelian groups). -/
 noncomputable def singularChainComplexFunctorObjMap (H : TopCat.Homotopy f g) (R : C) :
     _root_.Homotopy (((singularChainComplexFunctor C).obj R).map f)
       (((singularChainComplexFunctor C).obj R).map g) :=
-  H.toSSet.singularChainComplexFunctorObjMap R
+  H.toSSet.chainComplexMap R
 
 open HomologicalComplex in
 /-- Two homotopic morphisms in `TopCat` induce equal morphisms on the