From b03b3c2bf48e78416d03e066e5598266b7e5cbe8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 11 Dec 2023 08:57:39 +0100 Subject: [PATCH 1/2] feat(Algebra/Homology): construction of the homotopy cofiber --- Mathlib.lean | 1 + Mathlib/Algebra/Homology/HomotopyCofiber.lean | 239 ++++++++++++++++++ 2 files changed, 240 insertions(+) create mode 100644 Mathlib/Algebra/Homology/HomotopyCofiber.lean diff --git a/Mathlib.lean b/Mathlib.lean index 327ff687a1bfb..e2b530f817c78 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -240,6 +240,7 @@ import Mathlib.Algebra.Homology.Homotopy import Mathlib.Algebra.Homology.HomotopyCategory import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex import Mathlib.Algebra.Homology.HomotopyCategory.Shift +import Mathlib.Algebra.Homology.HomotopyCofiber import Mathlib.Algebra.Homology.ImageToKernel import Mathlib.Algebra.Homology.LocalCohomology import Mathlib.Algebra.Homology.ModuleCat diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean new file mode 100644 index 0000000000000..a13cf8f054a0c --- /dev/null +++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean @@ -0,0 +1,239 @@ +/- +Copyright (c) 2023 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.Homotopy + +/-! The homotopy cofiber of a morphism of homological complexes + +In this file, we construct the homotopy cofibre of a morphism `φ : F ⟶ G` +between homological complexes in `HomologicalComplex C c`. In degree `i`, +it is isomorphic to `(F.X j) ⊞ (G.X i)` if there is a `j` such that `c.Rel i j`, +and `G.X i` otherwise. (This is also known as the mapping cone of `φ`. Under +the name `CochainComplex.mappingCone`, a specific API shall be developed +for the case of cochains complexes indexed by `ℤ` (TODO).) + +When we assume `hc : ∀ j, ∃ i, c.Rel i j` (which holds in the case of chain complexes, +or cochain complexes indexed by `ℤ`), then for any homological complex `K`, +there is a bijection `HomologicalComplex.homotopyCofiber.descEquiv φ K hc` +between `homotopyCofiber φ ⟶ K` and the tuples `(α, hα)` with +`α : G ⟶ K` and `hα : Homotopy (φ ≫ α) 0` (TODO). + +We shall also study the cylinder of an homological complex `K`: this is the +homotopy cofibre of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. +Then, a morphism `K.cylinder ⟶ M` is determined by the data of two +morphisms `φ₀ φ₁ : K ⟶ M` and a homotopy `h : Homotopy φ₀ φ₁`, +see `cylinder.desc`. There is also an homotopy equivalence +`cylinder.homotopyEquiv K : HomotopyEquiv K.cylinder K`. From the construction of +the cylinder, we deduce the lemma `Homotopy.map_eq_of_inverts_homotopyEquivalences` +which assert that if a functor inverts homotopy equivalences, then the image of +two homotopic maps are equal (TODO). + +-/ + + +open CategoryTheory Category Limits Preadditive + +variable {C : Type*} [Category C] [Preadditive C] + +namespace HomologicalComplex + +variable {ι : Type*} {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) + +lemma dNext_eq_zero (ho : ∀ i j, F.X i ⟶ G.X j) (i : ι) (hi : ¬ c.Rel i (c.next i)) : + dNext i ho = 0 := by + dsimp [dNext] + rw [shape _ _ _ hi, zero_comp] + +lemma prevD_eq_zero (ho : ∀ i j, F.X i ⟶ G.X j) (i : ι) (hi : ¬ c.Rel (c.prev i) i) : + prevD i ho = 0 := by + dsimp [prevD] + rw [shape _ _ _ hi, comp_zero] + +/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy cofiber if for all +indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X j ⊞ G.X i` exists. -/ +class HasHomotopyCofiber (φ : F ⟶ G) : Prop where + hasBinaryBiproduct (i j : ι) (hij : c.Rel i j) : HasBinaryBiproduct (F.X j) (G.X i) + +variable [HasHomotopyCofiber φ] [DecidableRel c.Rel] + +namespace homotopyCofiber + +/-- The `X` field of the homological complex `homotopyCofiber φ`. -/ +noncomputable def X (i : ι) : C := + if hi : c.Rel i (c.next i) + then + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi + (F.X (c.next i)) ⊞ (G.X i) + else G.X i + +/-- The canonical isomorphism `(homotopyCofibre φ).X i ≅ F.X j ⊞ G.X i` when `c.Rel i j`. -/ +noncomputable def XIsoBiprod (i j : ι) (hij : c.Rel i j) [HasBinaryBiproduct (F.X j) (G.X i)] : + X φ i ≅ F.X j ⊞ G.X i := + eqToIso (by + obtain rfl := c.next_eq' hij + apply dif_pos hij) + +/-- The canonical isomorphism `(homotopyCofibre φ).X i ≅ G.X i` when `¬ c.Rel i (c.next i)`. -/ +noncomputable def XIso (i : ι) (hi : ¬ c.Rel i (c.next i)) : + X φ i ≅ G.X i := + eqToIso (dif_neg hi) + +/-- The second projection `(homotopyCofibre φ).X i ⟶ G.X i`. -/ +noncomputable def sndX (i : ι) : X φ i ⟶ G.X i := + if hi : c.Rel i (c.next i) + then + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi + (XIsoBiprod φ _ _ hi).hom ≫ biprod.snd + else + (XIso φ i hi).hom + +/-- The right inclusion `G.X i ⟶ (homotopyCofibre φ).X i`. -/ +noncomputable def inrX (i : ι) : G.X i ⟶ X φ i := + if hi : c.Rel i (c.next i) + then + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi + biprod.inr ≫ (XIsoBiprod φ _ _ hi).inv + else + (XIso φ i hi).inv + +@[reassoc (attr := simp)] +lemma inrX_sndX (i : ι) : inrX φ i ≫ sndX φ i = 𝟙 _ := by + dsimp [sndX, inrX] + split_ifs with hi <;> simp + +@[reassoc] +lemma sndX_inrX (i : ι) (hi : ¬ c.Rel i (c.next i)) : + sndX φ i ≫ inrX φ i = 𝟙 _ := by + dsimp [sndX, inrX] + simp only [dif_neg hi, Iso.hom_inv_id] + +/-- The first projection `(homotopyCofibre φ).X i ⟶ F.X j` when `c.Rel i j`. -/ +noncomputable def fstX (i j : ι) (hij : c.Rel i j) : X φ i ⟶ F.X j := + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij + (XIsoBiprod φ i j hij).hom ≫ biprod.fst + +/-- The left inclusion `F.X i ⟶ (homotopyCofibre φ).X j` when `c.Rel j i`. -/ +noncomputable def inlX (i j : ι) (hij : c.Rel j i) : F.X i ⟶ X φ j := + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij + biprod.inl ≫ (XIsoBiprod φ j i hij).inv + +@[reassoc (attr := simp)] +lemma inlX_fstX (i j : ι ) (hij : c.Rel j i) : + inlX φ i j hij ≫ fstX φ j i hij = 𝟙 _ := by + simp [inlX, fstX] + +@[reassoc (attr := simp)] +lemma inlX_sndX (i j : ι) (hij : c.Rel j i) : + inlX φ i j hij ≫ sndX φ j = 0 := by + obtain rfl := c.next_eq' hij + simp [inlX, sndX, dif_pos hij] + +@[reassoc (attr := simp)] +lemma inrX_fstX (i j : ι) (hij : c.Rel i j) : + inrX φ i ≫ fstX φ i j hij = 0 := by + obtain rfl := c.next_eq' hij + simp [inrX, fstX, dif_pos hij] + +/-- The `d` field of the homological complex `homotopyCofiber φ`. -/ +noncomputable def d (i j : ι) : X φ i ⟶ X φ j := + if hij : c.Rel i j + then + (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d _ _ ≫ inlX φ _ _ hj else 0) + + fstX φ i j hij ≫ φ.f j ≫ inrX φ j + sndX φ i ≫ G.d i j ≫ inrX φ j + else + 0 + +lemma ext_to_X (i j : ι) (hij : c.Rel i j) {A : C} {f g : A ⟶ X φ i} + (h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij) (h₂ : f ≫ sndX φ i = g ≫ sndX φ i) : + f = g := by + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij + rw [← cancel_mono (XIsoBiprod φ i j hij).hom] + apply biprod.hom_ext + · simpa using h₁ + · obtain rfl := c.next_eq' hij + simpa [sndX, dif_pos hij] using h₂ + +lemma ext_to_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : A ⟶ X φ i} + (h : f ≫ sndX φ i = g ≫ sndX φ i) : f = g := by + rw [← cancel_mono (XIso φ i hi).hom] + simpa only [sndX, dif_neg hi] using h + +lemma ext_from_X (i j : ι) (hij : c.Rel j i) {A : C} {f g : X φ j ⟶ A} + (h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g) (h₂ : inrX φ j ≫ f = inrX φ j ≫ g) : + f = g := by + haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij + rw [← cancel_epi (XIsoBiprod φ j i hij).inv] + apply biprod.hom_ext' + · simpa [inlX] using h₁ + · obtain rfl := c.next_eq' hij + simpa [inrX, dif_pos hij] using h₂ + +lemma ext_from_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : X φ i ⟶ A} + (h : inrX φ i ≫ f = inrX φ i ≫ g) : f = g := by + rw [← cancel_epi (XIso φ i hi).inv] + simpa only [inrX, dif_neg hi] using h + +@[reassoc] +lemma d_fstX (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) : + d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k := by + obtain rfl := c.next_eq' hjk + simp [d, dif_pos hij, dif_pos hjk] + +@[reassoc] +lemma d_sndX (i j : ι) (hij : c.Rel i j) : + d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j := by + dsimp [d] + split_ifs with hij <;> simp + +@[reassoc] +lemma inlX_d (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) : + inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j := by + apply ext_to_X φ j k hjk + · dsimp + simp [d_fstX φ _ _ _ hij hjk] + · simp [d_sndX φ _ _ hij] + +@[reassoc] +lemma inlX_d' (i j : ι) (hij : c.Rel i j) (hj : ¬ c.Rel j (c.next j)): + inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j := by + apply ext_to_X' _ _ hj + simp [d_sndX φ i j hij] + +lemma shape (i j : ι) (hij : ¬ c.Rel i j) : + d φ i j = 0 := + dif_neg hij + +@[reassoc (attr := simp)] +lemma inrX_d (i j : ι) : + inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j := by + by_cases hij : c.Rel i j + · by_cases hj : c.Rel j (c.next j) + · apply ext_to_X _ _ _ hj + · simp [d_fstX φ _ _ _ hij] + · simp [d_sndX φ _ _ hij] + · apply ext_to_X' _ _ hj + simp [d_sndX φ _ _ hij] + · rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero] + +end homotopyCofiber + +/-- The homotopy cofiber of a morphism of homological complexes, +also known as the mapping cone. -/ +@[simps] +noncomputable def homotopyCofiber : HomologicalComplex C c where + X i := homotopyCofiber.X φ i + d i j := homotopyCofiber.d φ i j + shape i j hij := homotopyCofiber.shape φ i j hij + d_comp_d' i j k hij hjk := by + apply homotopyCofiber.ext_from_X φ j i hij + · dsimp + simp only [comp_zero, homotopyCofiber.inlX_d_assoc φ i j k hij hjk, + add_comp, assoc, homotopyCofiber.inrX_d, Hom.comm_assoc, neg_comp] + by_cases hk : c.Rel k (c.next k) + · simp [homotopyCofiber.inlX_d φ j k _ hjk hk] + · simp [homotopyCofiber.inlX_d' φ j k hjk hk] + · simp + +end HomologicalComplex From 4cb357f8915992539bf82d1626b416bdef4c217e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 15 Dec 2023 12:47:23 +0100 Subject: [PATCH 2/2] cleaning up --- Mathlib/Algebra/Homology/Homotopy.lean | 10 ++++++ Mathlib/Algebra/Homology/HomotopyCofiber.lean | 35 ++++++++----------- 2 files changed, 24 insertions(+), 21 deletions(-) diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index 7d9e0e0f5f8fc..dfacef324e6ab 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/Mathlib/Algebra/Homology/Homotopy.lean @@ -56,6 +56,11 @@ theorem dNext_eq (f : ∀ i j, C.X i ⟶ D.X j) {i i' : ι} (w : c.Rel i i') : rfl #align d_next_eq dNext_eq +lemma dNext_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel i (c.next i)) : + dNext i f = 0 := by + dsimp [dNext] + rw [shape _ _ _ hi, zero_comp] + @[simp 1100] theorem dNext_comp_left (f : C ⟶ D) (g : ∀ i j, D.X i ⟶ E.X j) (i : ι) : (dNext i fun i j => f.f i ≫ g i j) = f.f i ≫ dNext i g := @@ -74,6 +79,11 @@ def prevD (j : ι) : (∀ i j, C.X i ⟶ D.X j) →+ (C.X j ⟶ D.X j) := Preadditive.add_comp _ _ _ _ _ _ #align prev_d prevD +lemma prevD_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel (c.prev i) i) : + prevD i f = 0 := by + dsimp [prevD] + rw [shape _ _ _ hi, comp_zero] + /-- `f j (c.prev j)`. -/ def toPrev (j : ι) : (∀ i j, C.X i ⟶ D.X j) →+ (C.X j ⟶ D.xPrev j) := AddMonoidHom.mk' (fun f => f j (c.prev j)) fun _ _ => rfl diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean index a13cf8f054a0c..3c4e3799651b4 100644 --- a/Mathlib/Algebra/Homology/HomotopyCofiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean @@ -7,12 +7,12 @@ import Mathlib.Algebra.Homology.Homotopy /-! The homotopy cofiber of a morphism of homological complexes -In this file, we construct the homotopy cofibre of a morphism `φ : F ⟶ G` +In this file, we construct the homotopy cofiber of a morphism `φ : F ⟶ G` between homological complexes in `HomologicalComplex C c`. In degree `i`, it is isomorphic to `(F.X j) ⊞ (G.X i)` if there is a `j` such that `c.Rel i j`, and `G.X i` otherwise. (This is also known as the mapping cone of `φ`. Under the name `CochainComplex.mappingCone`, a specific API shall be developed -for the case of cochains complexes indexed by `ℤ` (TODO).) +for the case of cochain complexes indexed by `ℤ` (TODO).) When we assume `hc : ∀ j, ∃ i, c.Rel i j` (which holds in the case of chain complexes, or cochain complexes indexed by `ℤ`), then for any homological complex `K`, @@ -20,11 +20,11 @@ there is a bijection `HomologicalComplex.homotopyCofiber.descEquiv φ K hc` between `homotopyCofiber φ ⟶ K` and the tuples `(α, hα)` with `α : G ⟶ K` and `hα : Homotopy (φ ≫ α) 0` (TODO). -We shall also study the cylinder of an homological complex `K`: this is the -homotopy cofibre of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. +We shall also study the cylinder of a homological complex `K`: this is the +homotopy cofiber of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. Then, a morphism `K.cylinder ⟶ M` is determined by the data of two morphisms `φ₀ φ₁ : K ⟶ M` and a homotopy `h : Homotopy φ₀ φ₁`, -see `cylinder.desc`. There is also an homotopy equivalence +see `cylinder.desc`. There is also a homotopy equivalence `cylinder.homotopyEquiv K : HomotopyEquiv K.cylinder K`. From the construction of the cylinder, we deduce the lemma `Homotopy.map_eq_of_inverts_homotopyEquivalences` which assert that if a functor inverts homotopy equivalences, then the image of @@ -41,21 +41,14 @@ namespace HomologicalComplex variable {ι : Type*} {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) -lemma dNext_eq_zero (ho : ∀ i j, F.X i ⟶ G.X j) (i : ι) (hi : ¬ c.Rel i (c.next i)) : - dNext i ho = 0 := by - dsimp [dNext] - rw [shape _ _ _ hi, zero_comp] - -lemma prevD_eq_zero (ho : ∀ i j, F.X i ⟶ G.X j) (i : ι) (hi : ¬ c.Rel (c.prev i) i) : - prevD i ho = 0 := by - dsimp [prevD] - rw [shape _ _ _ hi, comp_zero] - /-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy cofiber if for all indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X j ⊞ G.X i` exists. -/ class HasHomotopyCofiber (φ : F ⟶ G) : Prop where hasBinaryBiproduct (i j : ι) (hij : c.Rel i j) : HasBinaryBiproduct (F.X j) (G.X i) +instance [HasBinaryBiproducts C] : HasHomotopyCofiber φ where + hasBinaryBiproduct _ _ _ := inferInstance + variable [HasHomotopyCofiber φ] [DecidableRel c.Rel] namespace homotopyCofiber @@ -68,19 +61,19 @@ noncomputable def X (i : ι) : C := (F.X (c.next i)) ⊞ (G.X i) else G.X i -/-- The canonical isomorphism `(homotopyCofibre φ).X i ≅ F.X j ⊞ G.X i` when `c.Rel i j`. -/ +/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i` when `c.Rel i j`. -/ noncomputable def XIsoBiprod (i j : ι) (hij : c.Rel i j) [HasBinaryBiproduct (F.X j) (G.X i)] : X φ i ≅ F.X j ⊞ G.X i := eqToIso (by obtain rfl := c.next_eq' hij apply dif_pos hij) -/-- The canonical isomorphism `(homotopyCofibre φ).X i ≅ G.X i` when `¬ c.Rel i (c.next i)`. -/ +/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ G.X i` when `¬ c.Rel i (c.next i)`. -/ noncomputable def XIso (i : ι) (hi : ¬ c.Rel i (c.next i)) : X φ i ≅ G.X i := eqToIso (dif_neg hi) -/-- The second projection `(homotopyCofibre φ).X i ⟶ G.X i`. -/ +/-- The second projection `(homotopyCofiber φ).X i ⟶ G.X i`. -/ noncomputable def sndX (i : ι) : X φ i ⟶ G.X i := if hi : c.Rel i (c.next i) then @@ -89,7 +82,7 @@ noncomputable def sndX (i : ι) : X φ i ⟶ G.X i := else (XIso φ i hi).hom -/-- The right inclusion `G.X i ⟶ (homotopyCofibre φ).X i`. -/ +/-- The right inclusion `G.X i ⟶ (homotopyCofiber φ).X i`. -/ noncomputable def inrX (i : ι) : G.X i ⟶ X φ i := if hi : c.Rel i (c.next i) then @@ -109,12 +102,12 @@ lemma sndX_inrX (i : ι) (hi : ¬ c.Rel i (c.next i)) : dsimp [sndX, inrX] simp only [dif_neg hi, Iso.hom_inv_id] -/-- The first projection `(homotopyCofibre φ).X i ⟶ F.X j` when `c.Rel i j`. -/ +/-- The first projection `(homotopyCofiber φ).X i ⟶ F.X j` when `c.Rel i j`. -/ noncomputable def fstX (i j : ι) (hij : c.Rel i j) : X φ i ⟶ F.X j := haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij (XIsoBiprod φ i j hij).hom ≫ biprod.fst -/-- The left inclusion `F.X i ⟶ (homotopyCofibre φ).X j` when `c.Rel j i`. -/ +/-- The left inclusion `F.X i ⟶ (homotopyCofiber φ).X j` when `c.Rel j i`. -/ noncomputable def inlX (i j : ι) (hij : c.Rel j i) : F.X i ⟶ X φ j := haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij biprod.inl ≫ (XIsoBiprod φ j i hij).inv