feat(CategoryTheory): categories of homological complexes have a sepa…

…rator (#20229)

(This also requires the introduction of a typeclass `ComplexShape.HasNoLoop`, which holds for the most common shapes.)



Co-authored-by: Joël Riou <[email protected]>

Mathlib.lean

@@ -475,6 +475,7 @@ import Mathlib.Algebra.Homology.Embedding.TruncLEHomology
 import Mathlib.Algebra.Homology.ExactSequence
 import Mathlib.Algebra.Homology.Factorizations.Basic
 import Mathlib.Algebra.Homology.Functor
+import Mathlib.Algebra.Homology.HasNoLoop
 import Mathlib.Algebra.Homology.HomologicalBicomplex
 import Mathlib.Algebra.Homology.HomologicalComplex
 import Mathlib.Algebra.Homology.HomologicalComplexAbelian
@@ -1919,6 +1920,7 @@ import Mathlib.CategoryTheory.Galois.Prorepresentability
 import Mathlib.CategoryTheory.Galois.Topology
 import Mathlib.CategoryTheory.Generator.Abelian
 import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Generator.HomologicalComplex
 import Mathlib.CategoryTheory.Generator.Indization
 import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Generator.Presheaf

Mathlib/Algebra/Homology/ComplexShape.lean

@@ -167,7 +167,7 @@ lemma prev_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬ c.Rel (c.prev j) j) :
 (For example when `a = 1`, a cohomology theory indexed by `ℕ` or `ℤ`)
 -/
 @[simps]
-def up' {α : Type*} [AddRightCancelSemigroup α] (a : α) : ComplexShape α where
+def up' {α : Type*} [Add α] [IsRightCancelAdd α] (a : α) : ComplexShape α where
   Rel i j := i + a = j
   next_eq hi hj := hi.symm.trans hj
   prev_eq hi hj := add_right_cancel (hi.trans hj.symm)
@@ -176,27 +176,27 @@ def up' {α : Type*} [AddRightCancelSemigroup α] (a : α) : ComplexShape α whe
 (For example when `a = 1`, a homology theory indexed by `ℕ` or `ℤ`)
 -/
 @[simps]
-def down' {α : Type*} [AddRightCancelSemigroup α] (a : α) : ComplexShape α where
+def down' {α : Type*} [Add α] [IsRightCancelAdd α] (a : α) : ComplexShape α where
   Rel i j := j + a = i
   next_eq hi hj := add_right_cancel (hi.trans hj.symm)
   prev_eq hi hj := hi.symm.trans hj
 
-theorem down'_mk {α : Type*} [AddRightCancelSemigroup α] (a : α) (i j : α) (h : j + a = i) :
+theorem down'_mk {α : Type*} [Add α] [IsRightCancelAdd α] (a : α) (i j : α) (h : j + a = i) :
     (down' a).Rel i j := h
 
 /-- The `ComplexShape` appropriate for cohomology, so `d : X i ⟶ X j` only when `j = i + 1`.
 -/
 @[simps!]
-def up (α : Type*) [AddRightCancelSemigroup α] [One α] : ComplexShape α :=
+def up (α : Type*) [Add α] [IsRightCancelAdd α] [One α] : ComplexShape α :=
   up' 1
 
 /-- The `ComplexShape` appropriate for homology, so `d : X i ⟶ X j` only when `i = j + 1`.
 -/
 @[simps!]
-def down (α : Type*) [AddRightCancelSemigroup α] [One α] : ComplexShape α :=
+def down (α : Type*) [Add α] [IsRightCancelAdd α] [One α] : ComplexShape α :=
   down' 1
 
-theorem down_mk {α : Type*} [AddRightCancelSemigroup α] [One α] (i j : α) (h : j + 1 = i) :
+theorem down_mk {α : Type*} [Add α] [IsRightCancelAdd α] [One α] (i j : α) (h : j + 1 = i) :
     (down α).Rel i j :=
   down'_mk (1 : α) i j h
 

Mathlib/Algebra/Homology/Double.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import Mathlib.Algebra.Homology.HasNoLoop
 import Mathlib.Algebra.Homology.Single
 import Mathlib.CategoryTheory.Yoneda
 
@@ -182,4 +183,34 @@ noncomputable def evalCompCoyonedaCorepresentableBySingle (i : ι) [DecidableEq
       right_inv f := by simp }
   homEquiv_comp := by simp
 
+variable [c.HasNoLoop] [DecidableEq ι]
+
+open Classical in
+/-- Given a complex shape `c : ComplexShape ι` (with no loop), `X : C` and `j : ι`,
+this is a quite explicit choice of corepresentative of the functor which sends
+`K : HomologicalComplex C c` to `X ⟶ K.X j`. -/
+noncomputable def evalCompCoyonedaCorepresentative (X : C) (j : ι) :
+    HomologicalComplex C c :=
+  if hj : ∃ (k : ι), c.Rel j k then
+    double (𝟙 X) hj.choose_spec
+  else (single C c j).obj X
+
+/-- If a complex shape `c : ComplexShape ι` has no loop,
+then for any `X : C` and `j : ι`, the functor which sends `K : HomologicalComplex C c`
+to `X ⟶ K.X j` is corepresentable. -/
+noncomputable def evalCompCoyonedaCorepresentable (X : C) (j : ι) :
+    (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy
+      (evalCompCoyonedaCorepresentative c X j) := by
+  dsimp [evalCompCoyonedaCorepresentative]
+  by_cases h : ∃ (k : ι), c.Rel j k
+  · rw [dif_pos h]
+    exact evalCompCoyonedaCorepresentableByDoubleId _
+      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
+  · rw [dif_neg h]
+    apply evalCompCoyonedaCorepresentableBySingle
+    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto
+
+instance (X : C) (j : ι) : (eval C c j ⋙ coyoneda.obj (op X)).IsCorepresentable where
+  has_corepresentation := ⟨_, ⟨evalCompCoyonedaCorepresentable c X j⟩⟩
+
 end HomologicalComplex

Mathlib/Algebra/Homology/HasNoLoop.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.ComplexShape
+import Mathlib.Algebra.Group.Int.Defs
+import Mathlib.Algebra.Group.Nat.Defs
+
+/-!
+# Complex shapes with no loop
+
+Let `c : ComplexShape ι`. We define a type class `c.HasNoLoop`
+which expresses that `¬ c.Rel i i` for all `i : ι`.
+
+-/
+
+namespace ComplexShape
+
+variable {ι : Type*}
+
+/-- The condition that `c.Rel i i` does not hold for any `i`. -/
+class HasNoLoop (c : ComplexShape ι) : Prop where
+  not_rel_self (i : ι) : ¬ c.Rel i i
+
+section
+
+variable (c : ComplexShape ι) [c.HasNoLoop] (j : ι)
+
+lemma not_rel_self : ¬ c.Rel j j :=
+  HasNoLoop.not_rel_self j
+
+variable {j} in
+lemma not_rel_of_eq {j' : ι } (h : j = j') : ¬ c.Rel j j' := by
+  subst h
+  exact c.not_rel_self j
+
+instance : c.symm.HasNoLoop where
+  not_rel_self j := c.not_rel_self j
+
+lemma exists_distinct_prev_or :
+    (∃ (k : ι), c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬ c.Rel j k := by
+  by_cases h : ∃ (k : ι), c.Rel j k
+  · obtain ⟨k, hk⟩ := h
+    exact Or.inl ⟨k, hk, fun hjk ↦ c.not_rel_of_eq hjk hk⟩
+  · exact Or.inr (by simpa using h)
+
+lemma exists_distinct_next_or :
+    (∃ (i : ι), c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬ c.Rel i j := by
+  by_cases h : ∃ (i : ι), c.Rel i j
+  · obtain ⟨i, hi⟩ := h
+    exact Or.inl ⟨i, hi, fun hij ↦ c.not_rel_of_eq hij hi⟩
+  · exact Or.inr (by simpa using h)
+
+lemma hasNoLoop_up' {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
+    (a : α) (ha : a ≠ 0) :
+    (up' a).HasNoLoop where
+  not_rel_self i (hi : _ = _) :=
+    ha (add_left_cancel (by rw [add_zero, hi]))
+
+lemma hasNoLoop_down' {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
+    (a : α) (ha : a ≠ 0) :
+    (down' a).HasNoLoop := by
+  have := hasNoLoop_up' a ha
+  exact inferInstanceAs (up' a).symm.HasNoLoop
+
+lemma hasNoLoop_up {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
+    [One α] (ha : (1 : α) ≠ 0) :
+    (up α).HasNoLoop :=
+  hasNoLoop_up' _ ha
+
+lemma hasNoLoop_down {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
+    [One α] (ha : (1 : α) ≠ 0) :
+    (down α).HasNoLoop :=
+  hasNoLoop_down' _ ha
+
+end
+
+instance : (up ℤ).HasNoLoop := hasNoLoop_up (by simp)
+instance : (up ℕ).HasNoLoop := hasNoLoop_up (by simp)
+instance : (down ℤ).HasNoLoop := hasNoLoop_down (by simp)
+instance : (down ℕ).HasNoLoop := hasNoLoop_down (by simp)
+
+end ComplexShape

Mathlib/Algebra/Homology/Homotopy.lean

@@ -495,14 +495,14 @@ def mkInductiveAux₂ :
 
 @[simp] theorem mkInductiveAux₂_zero :
     mkInductiveAux₂ e zero comm_zero one comm_one succ 0 =
-      ⟨0, zero ≫ (Q.xPrevIso rfl).inv, mkInductiveAux₂.proof_2 e zero comm_zero⟩ :=
+      ⟨0, zero ≫ (Q.xPrevIso rfl).inv, mkInductiveAux₂.proof_3 e zero comm_zero⟩ :=
   rfl
 
 @[simp] theorem mkInductiveAux₂_add_one (n) :
     mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
       let I := mkInductiveAux₁ e zero one comm_one succ n
       ⟨(P.xNextIso rfl).hom ≫ I.1, I.2.1 ≫ (Q.xPrevIso rfl).inv,
-        mkInductiveAux₂.proof_5 e zero one comm_one succ n⟩ :=
+        mkInductiveAux₂.proof_6 e zero one comm_one succ n⟩ :=
   rfl
 
 theorem mkInductiveAux₃ (i j : ℕ) (h : i + 1 = j) :
@@ -624,14 +624,14 @@ def mkCoinductiveAux₂ :
 
 @[simp] theorem mkCoinductiveAux₂_zero :
     mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 =
-      ⟨0, (P.xNextIso rfl).hom ≫ zero, mkCoinductiveAux₂.proof_2 e zero comm_zero⟩ :=
+      ⟨0, (P.xNextIso rfl).hom ≫ zero, mkCoinductiveAux₂.proof_3 e zero comm_zero⟩ :=
   rfl
 
 @[simp] theorem mkCoinductiveAux₂_add_one (n) :
     mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
       let I := mkCoinductiveAux₁ e zero one comm_one succ n
       ⟨I.1 ≫ (Q.xPrevIso rfl).inv, (P.xNextIso rfl).hom ≫ I.2.1,
-        mkCoinductiveAux₂.proof_5 e zero one comm_one succ n⟩ :=
+        mkCoinductiveAux₂.proof_6 e zero one comm_one succ n⟩ :=
   rfl
 
 theorem mkCoinductiveAux₃ (i j : ℕ) (h : i + 1 = j) :

Mathlib/CategoryTheory/Generator/HomologicalComplex.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.Double
+import Mathlib.Algebra.Homology.HomologicalComplexLimits
+import Mathlib.CategoryTheory.Generator.Basic
+
+/-!
+# Generators of the category of homological complexes
+
+Let `c : ComplexShape ι` be a complex shape with no loop.
+If a category `C` has a separator, then `HomologicalComplex C c`
+has a separating family, and a separator when suitable coproducts exist.
+
+-/
+
+universe t w v u
+
+open CategoryTheory Limits
+
+namespace HomologicalComplex
+
+variable {C : Type u} [Category.{v} C] {ι : Type w} [DecidableEq ι]
+  (c : ComplexShape ι) [c.HasNoLoop]
+
+section
+
+variable [HasZeroMorphisms C] [HasZeroObject C]
+
+variable {α : Type t} {X : α → C} (hX : IsSeparating (Set.range X))
+
+variable (X) in
+/-- If `X : α → C` is a separating family, and `c : ComplexShape ι` has no loop,
+then this is a separating family indexed by `α × ι` in `HomologicalComplex C c`,
+which consists of homological complexes that are nonzero in at most
+two (consecutive) degrees. -/
+noncomputable def separatingFamily (j : α × ι) : HomologicalComplex C c :=
+  evalCompCoyonedaCorepresentative c (X j.1) j.2
+
+include hX in
+lemma isSeparating_separatingFamily :
+    IsSeparating (Set.range (separatingFamily c X)) := by
+  intro K L f g h
+  ext j
+  apply hX
+  rintro _ ⟨a, rfl⟩ p
+  have H := evalCompCoyonedaCorepresentable c (X a) j
+  apply H.homEquiv.symm.injective
+  simpa only [H.homEquiv_symm_comp] using h _ ⟨⟨a, j⟩, rfl⟩ (H.homEquiv.symm p)
+
+end
+
+variable [HasCoproductsOfShape ι C] [Preadditive C] [HasZeroObject C]
+
+lemma isSeparator_coproduct_separatingFamily {X : C} (hX : IsSeparator X) :
+    IsSeparator (∐ (fun i ↦ separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩)) := by
+  let φ (i : ι) := separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩
+  refine isSeparator_of_isColimit_cofan
+    (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using hX))
+      (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_
+  exact IsColimit.ofWhiskerEquivalence
+    (Discrete.equivalence (Equiv.punitProd.{0} ι).symm) (coproductIsCoproduct φ)
+
+instance [HasSeparator C] : HasSeparator (HomologicalComplex C c) :=
+  ⟨_, isSeparator_coproduct_separatingFamily c (isSeparator_separator C)⟩
+
+end HomologicalComplex