Skip to content

Commit 795a5ff

Browse files
joelriouTwoFX
joelriou
and
TwoFX
committed
feat: the short complexes attached to homological complexes (#6039)
If `K` is an homological complex and `i` some degree, this PR defines the short complex `K.sc i` which is `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)``. - [x] depends on: #6008 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
1 parent cebb592 commit 795a5ff

File tree

3 files changed

+120
-0
lines changed

3 files changed

+120
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,7 @@ import Mathlib.Algebra.Homology.Opposite
222222
import Mathlib.Algebra.Homology.QuasiIso
223223
import Mathlib.Algebra.Homology.ShortComplex.Basic
224224
import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
225+
import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
225226
import Mathlib.Algebra.Homology.ShortComplex.Homology
226227
import Mathlib.Algebra.Homology.ShortComplex.LeftHomology
227228
import Mathlib.Algebra.Homology.ShortComplex.RightHomology

‎Mathlib/Algebra/Homology/HomologicalComplex.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,58 @@ theorem ext {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X)
9292
· rw [s₁ i j hij, s₂ i j hij]
9393
#align homological_complex.ext HomologicalComplex.ext
9494

95+
/-- The obvious isomorphism `K.X p ≅ K.X q` when `p = q`. -/
96+
def XIsoOfEq (K : HomologicalComplex V c) {p q : ι} (h : p = q) :
97+
K.X p ≅ K.X q := eqToIso (by rw [h])
98+
99+
@[simp]
100+
lemma XIsoOfEq_rfl (K : HomologicalComplex V c) (p : ι) :
101+
K.XIsoOfEq (rfl : p = p) = Iso.refl _ := rfl
102+
103+
@[reassoc (attr := simp)]
104+
lemma XIsoOfEq_hom_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
105+
(h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) :
106+
(K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₁₂.trans h₂₃)).hom := by
107+
dsimp [XIsoOfEq]
108+
simp only [eqToHom_trans]
109+
110+
@[reassoc (attr := simp)]
111+
lemma XIsoOfEq_hom_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
112+
(h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) :
113+
(K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₁₂.trans h₃₂.symm)).hom := by
114+
dsimp [XIsoOfEq]
115+
simp only [eqToHom_trans]
116+
117+
@[reassoc (attr := simp)]
118+
lemma XIsoOfEq_inv_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
119+
(h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) :
120+
(K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₂₁.symm.trans h₂₃)).hom := by
121+
dsimp [XIsoOfEq]
122+
simp only [eqToHom_trans]
123+
124+
@[reassoc (attr := simp)]
125+
lemma XIsoOfEq_inv_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
126+
(h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) :
127+
(K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₃₂.trans h₂₁).symm).hom := by
128+
dsimp [XIsoOfEq]
129+
simp only [eqToHom_trans]
130+
131+
@[reassoc (attr := simp)]
132+
lemma XIsoOfEq_hom_comp_d (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) :
133+
(K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃ := by subst h; simp
134+
135+
@[reassoc (attr := simp)]
136+
lemma XIsoOfEq_inv_comp_d (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) :
137+
(K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃ := by subst h; simp
138+
139+
@[reassoc (attr := simp)]
140+
lemma d_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) :
141+
K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃ := by subst h; simp
142+
143+
@[reassoc (attr := simp)]
144+
lemma d_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) :
145+
K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃ := by subst h; simp
146+
95147
end HomologicalComplex
96148

97149
/-- An `α`-indexed chain complex is a `HomologicalComplex`

‎Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/-
2+
Copyright (c) 2023 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
import Mathlib.Algebra.Homology.HomologicalComplex
7+
import Mathlib.Algebra.Homology.ShortComplex.Homology
8+
9+
/-!
10+
# The short complexes attached to homological complexes
11+
12+
In this file, we define a functor
13+
`shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C`.
14+
By definition, the image of a homological complex `K` by this functor
15+
is the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`.
16+
17+
When the homology refactor is completed (TODO @joelriou), the homology
18+
of a homological complex `K` in degree `i` shall be the homology
19+
of the short complex `(shortComplexFunctor C c i).obj K`, which can be
20+
abbreviated as `K.sc i`.
21+
22+
-/
23+
24+
open CategoryTheory Category Limits
25+
26+
namespace HomologicalComplex
27+
28+
variable (C : Type _) [Category C] [HasZeroMorphisms C] {ι : Type _} (c : ComplexShape ι)
29+
30+
/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
31+
complex `K` to the short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`. -/
32+
@[simps]
33+
def shortComplexFunctor' (i j k : ι) : HomologicalComplex C c ⥤ ShortComplex C where
34+
obj K := ShortComplex.mk (K.d i j) (K.d j k) (K.d_comp_d i j k)
35+
map f :=
36+
{ τ₁ := f.f i
37+
τ₂ := f.f j
38+
τ₃ := f.f k }
39+
40+
/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
41+
complex `K` to the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`. -/
42+
@[simps!]
43+
noncomputable def shortComplexFunctor (i : ι) :=
44+
shortComplexFunctor' C c (c.prev i) i (c.next i)
45+
46+
/-- The natural isomorphism `shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k`
47+
when `c.prev j = i` and `c.next j = k`. -/
48+
@[simps!]
49+
noncomputable def natIsoSc' (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
50+
shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k :=
51+
NatIso.ofComponents (fun K => ShortComplex.isoMk (K.XIsoOfEq hi) (Iso.refl _) (K.XIsoOfEq hk)
52+
(by aesop_cat) (by aesop_cat)) (by aesop_cat)
53+
54+
variable {C c}
55+
variable (K L M : HomologicalComplex C c) (φ : K ⟶ L) (ψ : L ⟶ M)
56+
57+
/-- The short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`. -/
58+
abbrev sc' (i j k : ι) := (shortComplexFunctor' C c i j k).obj K
59+
60+
/-- The short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`. -/
61+
noncomputable abbrev sc (i : ι) := (shortComplexFunctor C c i).obj K
62+
63+
/-- The canonical isomorphism `K.sc j ≅ K.sc' i j k` when `c.prev j = i` and `c.next j = k`. -/
64+
noncomputable abbrev isoSc' (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
65+
K.sc j ≅ K.sc' i j k := (natIsoSc' C c i j k hi hk).app K
66+
67+
end HomologicalComplex

0 commit comments

Comments
 (0)