Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 8001ea5

Browse files
jjaassoonnjjaassoonn
committed
feat(category_theory/abelian): right derived functor (#12841)
This pr dualises derived.lean. Right derived functor and natural transformation between right derived functors and related lemmas are formalised. The docs string currently contains more than what is in this file, but everything else will come shortly after.
1 parent 25ec622 commit 8001ea5

5 files changed

Lines changed: 169 additions & 4 deletions

File tree

‎src/category_theory/abelian/ext.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Adam Topaz
55
-/
66
import algebra.category.Group.basic
77
import algebra.category.Module.abelian
8-
import category_theory.functor.derived
8+
import category_theory.functor.left_derived
99
import category_theory.linear.yoneda
1010
import category_theory.abelian.opposite
1111
import category_theory.abelian.projective
@@ -37,7 +37,7 @@ variables (R : Type*) [ring R] (C : Type*) [category C] [abelian C] [linear R C]
3737
[enough_projectives C]
3838

3939
/--
40-
`Ext R C n` is defined by deriving in the frst argument of `(X, Y) ↦ Module.of R (unop X ⟶ Y)`
40+
`Ext R C n` is defined by deriving in the first argument of `(X, Y) ↦ Module.of R (unop X ⟶ Y)`
4141
(which is the second argument of `linear_yoneda`).
4242
-/
4343
@[simps]

src/category_theory/abelian/derived.lean renamed to src/category_theory/abelian/left_derived.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Riccardo Brasca, Adam Topaz
55
-/
66

77
import category_theory.abelian.homology
8-
import category_theory.functor.derived
8+
import category_theory.functor.left_derived
99
import category_theory.abelian.projective
1010
import category_theory.limits.constructions.epi_mono
1111

‎src/category_theory/abelian/right_derived.lean‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
/-
2+
Copyright (c) 2022 Jujian Zhang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jujian Zhang, Scott Morrison
5+
-/
6+
import category_theory.abelian.injective_resolution
7+
import algebra.homology.additive
8+
import category_theory.limits.constructions.epi_mono
9+
import category_theory.abelian.homology
10+
import category_theory.abelian.exact
11+
12+
/-!
13+
# Right-derived functors
14+
15+
We define the right-derived functors `F.right_derived n : C ⥤ D` for any additive functor `F`
16+
out of a category with injective resolutions.
17+
18+
The definition is
19+
```
20+
injective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n
21+
```
22+
that is, we pick an injective resolution (thought of as an object of the homotopy category),
23+
we apply `F` objectwise, and compute `n`-th homology.
24+
25+
We show that these right-derived functors can be calculated
26+
on objects using any choice of injective resolution,
27+
and on morphisms by any choice of lift to a cochain map between chosen injective resolutions.
28+
29+
Similarly we define natural transformations between right-derived functors coming from
30+
natural transformations between the original additive functors,
31+
and show how to compute the components.
32+
33+
## Main results
34+
* `category_theory.functor.right_derived_obj_injective_zero`: the `0`-th derived functor of `F` on
35+
an injective object `X` is isomorphic to `F.obj X`.
36+
* `category_theory.functor.right_derived_obj_injective_succ`: injective objects have no higher
37+
right derived functor.
38+
* `category_theory.nat_trans.right_derived`: the natural isomorphism between right derived functors
39+
induced by natural transformation.
40+
41+
Now, we assume `preserves_finite_limits F`, then
42+
* `category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono`: if `f` is
43+
mono and `exact f g`, then `exact (F.map f) (F.map g)`.
44+
* `category_theory.abelian.functor.right_derived_zero_iso_self`: if there are enough injectives,
45+
then there is a natural isomorphism `(F.right_derived 0) ≅ F`.
46+
-/
47+
48+
noncomputable theory
49+
50+
open category_theory
51+
open category_theory.limits
52+
53+
54+
namespace category_theory
55+
universes v u
56+
variables {C : Type u} [category.{v} C] {D : Type*} [category D]
57+
variables [abelian C] [has_injective_resolutions C] [abelian D]
58+
59+
/-- The right derived functors of an additive functor. -/
60+
def functor.right_derived (F : C ⥤ D) [F.additive] (n : ℕ) : C ⥤ D :=
61+
injective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n
62+
63+
/-- We can compute a right derived functor using a chosen injective resolution. -/
64+
@[simps]
65+
def functor.right_derived_obj_iso (F : C ⥤ D) [F.additive] (n : ℕ)
66+
{X : C} (P : InjectiveResolution X) :
67+
(F.right_derived n).obj X ≅
68+
(homology_functor D _ n).obj ((F.map_homological_complex _).obj P.cocomplex) :=
69+
(homotopy_category.homology_functor D _ n).map_iso
70+
(homotopy_category.iso_of_homotopy_equiv
71+
(F.map_homotopy_equiv (InjectiveResolution.homotopy_equiv _ P)))
72+
≪≫ (homotopy_category.homology_factors D _ n).app _
73+
74+
/-- The 0-th derived functor of `F` on an injective object `X` is just `F.obj X`. -/
75+
@[simps]
76+
def functor.right_derived_obj_injective_zero (F : C ⥤ D) [F.additive]
77+
(X : C) [injective X] :
78+
(F.right_derived 0).obj X ≅ F.obj X :=
79+
F.right_derived_obj_iso 0 (InjectiveResolution.self X) ≪≫
80+
(homology_functor _ _ _).map_iso ((cochain_complex.single₀_map_homological_complex F).app X) ≪≫
81+
(cochain_complex.homology_functor_0_single₀ D).app (F.obj X)
82+
83+
open_locale zero_object
84+
85+
/-- The higher derived functors vanish on injective objects. -/
86+
@[simps]
87+
def functor.right_derived_obj_injective_succ (F : C ⥤ D) [F.additive] (n : ℕ)
88+
(X : C) [injective X] :
89+
(F.right_derived (n+1)).obj X ≅ 0 :=
90+
F.right_derived_obj_iso (n+1) (InjectiveResolution.self X) ≪≫
91+
(homology_functor _ _ _).map_iso ((cochain_complex.single₀_map_homological_complex F).app X) ≪≫
92+
(cochain_complex.homology_functor_succ_single₀ D n).app (F.obj X)
93+
/--
94+
We can compute a right derived functor on a morphism using a descent of that morphism
95+
to a cochain map between chosen injective resolutions.
96+
-/
97+
lemma functor.right_derived_map_eq (F : C ⥤ D) [F.additive] (n : ℕ) {X Y : C} (f : Y ⟶ X)
98+
{P : InjectiveResolution X} {Q : InjectiveResolution Y} (g : Q.cocomplex ⟶ P.cocomplex)
99+
(w : Q.ι ≫ g = (cochain_complex.single₀ C).map f ≫ P.ι) :
100+
(F.right_derived n).map f =
101+
(F.right_derived_obj_iso n Q).hom ≫
102+
(homology_functor D _ n).map ((F.map_homological_complex _).map g) ≫
103+
(F.right_derived_obj_iso n P).inv :=
104+
begin
105+
dsimp only [functor.right_derived, functor.right_derived_obj_iso],
106+
dsimp, simp only [category.comp_id, category.id_comp],
107+
rw [←homology_functor_map, homotopy_category.homology_functor_map_factors],
108+
simp only [←functor.map_comp],
109+
congr' 1,
110+
apply homotopy_category.eq_of_homotopy,
111+
apply functor.map_homotopy,
112+
apply homotopy.trans,
113+
exact homotopy_category.homotopy_out_map _,
114+
apply InjectiveResolution.desc_homotopy f,
115+
{ simp, },
116+
{ simp only [InjectiveResolution.homotopy_equiv_hom_ι_assoc],
117+
rw [←category.assoc, w, category.assoc],
118+
simp only [InjectiveResolution.homotopy_equiv_inv_ι], },
119+
end
120+
121+
/-- The natural transformation between right-derived functors induced by a natural transformation.-/
122+
@[simps]
123+
def nat_trans.right_derived {F G : C ⥤ D} [F.additive] [G.additive] (α : F ⟶ G) (n : ℕ) :
124+
F.right_derived n ⟶ G.right_derived n :=
125+
whisker_left (injective_resolutions C)
126+
(whisker_right (nat_trans.map_homotopy_category α _)
127+
(homotopy_category.homology_functor D _ n))
128+
129+
@[simp] lemma nat_trans.right_derived_id (F : C ⥤ D) [F.additive] (n : ℕ) :
130+
nat_trans.right_derived (𝟙 F) n = 𝟙 (F.right_derived n) :=
131+
by { simp [nat_trans.right_derived], refl, }
132+
133+
@[simp, nolint simp_nf] lemma nat_trans.right_derived_comp
134+
{F G H : C ⥤ D} [F.additive] [G.additive] [H.additive]
135+
(α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
136+
nat_trans.right_derived (α ≫ β) n = nat_trans.right_derived α n ≫ nat_trans.right_derived β n :=
137+
by simp [nat_trans.right_derived]
138+
139+
/--
140+
A component of the natural transformation between right-derived functors can be computed
141+
using a chosen injective resolution.
142+
-/
143+
lemma nat_trans.right_derived_eq {F G : C ⥤ D} [F.additive] [G.additive] (α : F ⟶ G) (n : ℕ)
144+
{X : C} (P : InjectiveResolution X) :
145+
(nat_trans.right_derived α n).app X =
146+
(F.right_derived_obj_iso n P).hom ≫
147+
(homology_functor D _ n).map ((nat_trans.map_homological_complex α _).app P.cocomplex) ≫
148+
(G.right_derived_obj_iso n P).inv :=
149+
begin
150+
symmetry,
151+
dsimp [nat_trans.right_derived, functor.right_derived_obj_iso],
152+
simp only [category.comp_id, category.id_comp],
153+
rw [←homology_functor_map, homotopy_category.homology_functor_map_factors],
154+
simp only [←functor.map_comp],
155+
congr' 1,
156+
apply homotopy_category.eq_of_homotopy,
157+
simp only [nat_trans.map_homological_complex_naturality_assoc,
158+
←functor.map_comp],
159+
apply homotopy.comp_left_id,
160+
rw [←functor.map_id],
161+
apply functor.map_homotopy,
162+
apply homotopy_equiv.homotopy_hom_inv_id,
163+
end
164+
165+
end category_theory

src/category_theory/functor/derived.lean renamed to src/category_theory/functor/left_derived.lean

File renamed without changes.

‎src/category_theory/monoidal/tor.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
6-
import category_theory.functor.derived
6+
import category_theory.functor.left_derived
77
import category_theory.monoidal.preadditive
88

99
/-!

0 commit comments

Comments
 (0)