-
Notifications
You must be signed in to change notification settings - Fork 251
/
HomologicalComplexAbelian.lean
70 lines (54 loc) · 2.34 KB
/
HomologicalComplexAbelian.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
/-
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.Additive
import Mathlib.Algebra.Homology.HomologicalComplexLimits
import Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-! # THe category of homological complexes is abelian
If `C` is an abelian category, then `HomologicalComplex C c` is an abelian
category for any complex shape `c : ComplexShape ι`.
We also obtain that a short complex in `HomologicalComplex C c`
is exact (resp. short exact) iff degreewise it is so.
-/
open CategoryTheory Category Limits
namespace HomologicalComplex
variable {C ι : Type*} {c : ComplexShape ι} [Category C] [Abelian C]
noncomputable instance : NormalEpiCategory (HomologicalComplex C c) := ⟨fun p _ =>
NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
(isColimitOfEval _ _ (fun _ =>
Abelian.isColimitMapCoconeOfCokernelCoforkOfπ _ _))⟩
noncomputable instance : NormalMonoCategory (HomologicalComplex C c) := ⟨fun p _ =>
NormalMono.mk _ (cokernel.π p) (cokernel.condition _)
(isLimitOfEval _ _ (fun _ =>
Abelian.isLimitMapConeOfKernelForkOfι _ _))⟩
noncomputable instance : Abelian (HomologicalComplex C c) where
variable (S : ShortComplex (HomologicalComplex C c))
lemma exact_of_degreewise_exact (hS : ∀ (i : ι), (S.map (eval C c i)).Exact) :
S.Exact := by
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
rw [IsZero.iff_id_eq_zero]
ext i
apply (IsZero.of_iso (hS i) (S.mapHomologyIso (eval C c i)).symm).eq_of_src
lemma shortExact_of_degreewise_shortExact
(hS : ∀ (i : ι), (S.map (eval C c i)).ShortExact) :
S.ShortExact where
mono_f := mono_of_mono_f _ (fun i => (hS i).mono_f)
epi_g := epi_of_epi_f _ (fun i => (hS i).epi_g)
exact := exact_of_degreewise_exact S (fun i => (hS i).exact)
lemma exact_iff_degreewise_exact :
S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact := by
constructor
· intro hS i
exact hS.map (eval C c i)
· exact exact_of_degreewise_exact S
lemma shortExact_iff_degreewise_shortExact :
S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact := by
constructor
· intro hS i
have := hS.mono_f
have := hS.epi_g
exact hS.map (eval C c i)
· exact shortExact_of_degreewise_shortExact S
end HomologicalComplex