/
InjectiveResolution.lean
155 lines (124 loc) · 5.73 KB
/
InjectiveResolution.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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
/-
Copyright (c) 2022 Jujian Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jujian Zhang, Scott Morrison, Joël Riou
-/
import Mathlib.CategoryTheory.Preadditive.Injective
import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
import Mathlib.Algebra.Homology.QuasiIso
#align_import category_theory.preadditive.injective_resolution from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7"
/-!
# Injective resolutions
An injective resolution `I : InjectiveResolution Z` of an object `Z : C` consists of
an `ℕ`-indexed cochain complex `I.cocomplex` of injective objects,
along with a quasi-isomorphism `I.ι` from the cochain complex consisting just of `Z`
in degree zero to `I.cocomplex`.
```
Z ----> 0 ----> ... ----> 0 ----> ...
| | |
| | |
v v v
I⁰ ---> I¹ ---> ... ----> Iⁿ ---> ...
```
-/
noncomputable section
universe v u
namespace CategoryTheory
open Limits HomologicalComplex CochainComplex
variable {C : Type u} [Category.{v} C] [HasZeroObject C] [HasZeroMorphisms C]
/--
An `InjectiveResolution Z` consists of a bundled `ℕ`-indexed cochain complex of injective objects,
along with a quasi-isomorphism from the complex consisting of just `Z` supported in degree `0`.
-/
-- @[nolint has_nonempty_instance]
structure InjectiveResolution (Z : C) where
/-- the cochain complex involved in the resolution -/
cocomplex : CochainComplex C ℕ
/-- the cochain complex must be degreewise injective -/
injective : ∀ n, Injective (cocomplex.X n) := by infer_instance
/-- the cochain complex must have homology -/
[hasHomology : ∀ i, cocomplex.HasHomology i]
/-- the morphism from the single cochain complex with `Z` in degree `0` -/
ι : (single₀ C).obj Z ⟶ cocomplex
/-- the morphism from the single cochain complex with `Z` in degree `0` is a quasi-isomorphism -/
quasiIso : QuasiIso ι := by infer_instance
set_option linter.uppercaseLean3 false in
#align category_theory.InjectiveResolution CategoryTheory.InjectiveResolution
open InjectiveResolution in
attribute [instance] injective hasHomology InjectiveResolution.quasiIso
/-- An object admits an injective resolution. -/
class HasInjectiveResolution (Z : C) : Prop where
out : Nonempty (InjectiveResolution Z)
#align category_theory.has_injective_resolution CategoryTheory.HasInjectiveResolution
attribute [inherit_doc HasInjectiveResolution] HasInjectiveResolution.out
section
variable (C)
/-- You will rarely use this typeclass directly: it is implied by the combination
`[EnoughInjectives C]` and `[Abelian C]`. -/
class HasInjectiveResolutions : Prop where
out : ∀ Z : C, HasInjectiveResolution Z
#align category_theory.has_injective_resolutions CategoryTheory.HasInjectiveResolutions
attribute [instance 100] HasInjectiveResolutions.out
end
namespace InjectiveResolution
variable {Z : C} (I : InjectiveResolution Z)
lemma cocomplex_exactAt_succ (n : ℕ) :
I.cocomplex.ExactAt (n + 1) := by
rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]
· infer_instance
lemma exact_succ (n : ℕ):
(ShortComplex.mk _ _ (I.cocomplex.d_comp_d n (n + 1) (n + 2))).Exact :=
(HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 2) (by simp)
(by simp only [CochainComplex.next]; rfl)).1 (I.cocomplex_exactAt_succ n)
@[simp]
theorem ι_f_succ (n : ℕ) : I.ι.f (n + 1) = 0 :=
(isZero_single_obj_X _ _ _ _ (by simp)).eq_of_src _ _
set_option linter.uppercaseLean3 false in
#align category_theory.InjectiveResolution.ι_f_succ CategoryTheory.InjectiveResolution.ι_f_succ
-- Porting note (#10618): removed @[simp] simp can prove this
@[reassoc]
theorem ι_f_zero_comp_complex_d :
I.ι.f 0 ≫ I.cocomplex.d 0 1 = 0 := by
simp
set_option linter.uppercaseLean3 false in
#align category_theory.InjectiveResolution.ι_f_zero_comp_complex_d CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d
-- Porting note (#10618): removed @[simp] simp can prove this
theorem complex_d_comp (n : ℕ) :
I.cocomplex.d n (n + 1) ≫ I.cocomplex.d (n + 1) (n + 2) = 0 := by
simp
set_option linter.uppercaseLean3 false in
#align category_theory.InjectiveResolution.complex_d_comp CategoryTheory.InjectiveResolution.complex_d_comp
/-- The (limit) kernel fork given by the composition
`Z ⟶ I.cocomplex.X 0 ⟶ I.cocomplex.X 1` when `I : InjectiveResolution Z`. -/
@[simp]
def kernelFork : KernelFork (I.cocomplex.d 0 1) :=
KernelFork.ofι _ I.ι_f_zero_comp_complex_d
/-- `Z` is the kernel of `I.cocomplex.X 0 ⟶ I.cocomplex.X 1` when `I : InjectiveResolution Z`. -/
def isLimitKernelFork : IsLimit (I.kernelFork) := by
refine IsLimit.ofIsoLimit (I.cocomplex.cyclesIsKernel 0 1 (by simp)) (Iso.symm ?_)
refine Fork.ext ((singleObjHomologySelfIso _ _ _).symm ≪≫
isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm) ?_
rw [← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom,
← cancel_epi (isoHomologyπ₀ _).hom,
← cancel_epi (singleObjCyclesSelfIso (ComplexShape.up ℕ) _ _).inv]
simp
instance (n : ℕ) : Mono (I.ι.f n) := by
cases n
· exact mono_of_isLimit_fork I.isLimitKernelFork
· rw [ι_f_succ]; infer_instance
variable (Z)
/-- An injective object admits a trivial injective resolution: itself in degree 0. -/
@[simps]
def self [Injective Z] : InjectiveResolution Z where
cocomplex := (CochainComplex.single₀ C).obj Z
ι := 𝟙 ((CochainComplex.single₀ C).obj Z)
injective n := by
cases n
· simpa
· apply IsZero.injective
apply HomologicalComplex.isZero_single_obj_X
simp
set_option linter.uppercaseLean3 false in
#align category_theory.InjectiveResolution.self CategoryTheory.InjectiveResolution.self
end InjectiveResolution
end CategoryTheory