-
Notifications
You must be signed in to change notification settings - Fork 384
/
Copy pathShortExact.lean
143 lines (119 loc) · 6.07 KB
/
ShortExact.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
/-
Copyright (c) 2024 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.HomotopyCategory.HomologicalFunctor
import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
import Mathlib.Algebra.Homology.HomologySequenceLemmas
import Mathlib.Algebra.Homology.Refinements
/-!
# The mapping cone of a monomorphism, up to a quasi-isomophism
If `S` is a short exact short complex of cochain complexes in an abelian category,
we construct a quasi-isomorphism `descShortComplex S : mappingCone S.f ⟶ S.X₃`.
We obtain this by comparing the homology sequence of `S` and the homology
sequence of the homology functor on the homotopy category, applied to the triangle
attached to the mapping cone of `S.f`.
-/
open CategoryTheory Category ComplexShape HomotopyCategory Limits
HomologicalComplex.HomologySequence Pretriangulated Preadditive
variable {C : Type*} [Category C] [Abelian C]
namespace CochainComplex
section
variable (T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
@[reassoc]
lemma homologySequenceδ_quotient_mapTriangle_obj :
(homologyFunctor C (up ℤ) 0).homologySequenceδ
((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
(homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
(HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ (by omega) ≫
(homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
sorry
end
namespace mappingCone
variable (S : ShortComplex (CochainComplex C ℤ)) (hS : S.ShortExact)
/-- The canonical morphism `mappingCone S.f ⟶ S.X₃` when `S` is a short complex
of cochain complexes. -/
noncomputable def descShortComplex : mappingCone S.f ⟶ S.X₃ := desc S.f 0 S.g (by simp)
@[reassoc (attr := simp)]
lemma inr_descShortComplex : inr S.f ≫ descShortComplex S = S.g := by
simp [descShortComplex]
@[reassoc (attr := simp)]
lemma inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n := by
simp [descShortComplex]
@[reassoc (attr := simp)]
lemma inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) :
(inl S.f).v i j h ≫ (descShortComplex S).f j = 0 := by
simp [descShortComplex]
variable {S}
lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
(homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
(homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫
(homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
dsimp
rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
assoc, assoc, assoc, Iso.inv_hom_id_app,
← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]
dsimp
rw [comp_id]
apply yoneda.map_injective
ext ⟨A⟩ (x : A ⟶ _)
dsimp
obtain ⟨A', π, _, x', w, hx'⟩ :=
(mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)
erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]
dsimp
rw [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
erw [comp_id]
rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
HomologicalComplex.homologyπ_naturality_assoc,
HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
inl_v_descShortComplex_f, comp_zero, zero_add]
rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
(by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
dsimp [Functor.shiftMap, homologyFunctor_shift]
rw [HomologicalComplex.homologyπ_naturality_assoc,
HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
sorry
open ComposableArrows
set_option simprocs false
lemma quasiIso_descShortComplex : QuasiIso (descShortComplex S) where
quasiIsoAt n := by
rw [quasiIsoAt_iff_isIso_homologyMap]
let φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅
(triangleh S.f) n _ rfl).δlast ⟶ (composableArrows₅ hS n _ rfl).δlast :=
homMk₄ ((homologyFunctorFactors C (up ℤ) _).hom.app _)
((homologyFunctorFactors C (up ℤ) _).hom.app _)
((homologyFunctorFactors C (up ℤ) _).hom.app _ ≫
HomologicalComplex.homologyMap (descShortComplex S) n)
((homologyFunctorFactors C (up ℤ) _).hom.app _)
((homologyFunctorFactors C (up ℤ) _).hom.app _)
((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
(by
erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]
dsimp
rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex])
(by
dsimp
erw [homologySequenceδ_triangleh hS]
simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc,
Iso.inv_hom_id_app, comp_id])
((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
HomologicalComplex.homologyMap (descShortComplex S) n) := by
apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
(mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
(composableArrows₅_exact hS n _ rfl).δlast φ
all_goals dsimp [φ]; infer_instance
apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))
end mappingCone
end CochainComplex