Skip to content

Commit 9a59085

Browse files
joelrioujoelriou
committed
feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence (leanprover-community#35378)
Given a spectral object `X` in an abelian category, we define the objects which shall appear on the various pages of the spectral sequence attached to `X`.
1 parent 2848a7a commit 9a59085

File tree

2 files changed

+320
-0
lines changed

2 files changed

+320
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -669,6 +669,7 @@ public import Mathlib.Algebra.Homology.SingleHomology
669669
public import Mathlib.Algebra.Homology.SpectralObject.Basic
670670
public import Mathlib.Algebra.Homology.SpectralObject.Cycles
671671
public import Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
672+
public import Mathlib.Algebra.Homology.SpectralObject.Page
672673
public import Mathlib.Algebra.Homology.SpectralSequence.Basic
673674
public import Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
674675
public import Mathlib.Algebra.Homology.Square

‎Mathlib/Algebra/Homology/SpectralObject/Page.lean‎

Lines changed: 319 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,319 @@
1+
/-
2+
Copyright (c) 2026 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+
module
7+
8+
public import Mathlib.Algebra.Homology.SpectralObject.Cycles
9+
public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
10+
public import Mathlib.CategoryTheory.Abelian.Refinements
11+
public import Mathlib.CategoryTheory.ComposableArrows.Three
12+
13+
/-!
14+
# Spectral objects in abelian categories
15+
16+
Let `X` be a spectral object index by the category `ι`
17+
in the abelian category `C`. The purpose of this file
18+
is to introduce the homology `X.E` of the short complex `X.shortComplex`
19+
`(X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₂).obj (mk₁ f₁)`
20+
when `f₁`, `f₂` and `f₃` are composable morphisms in `ι` and the
21+
equalities `n₀ + 1 = n₁` and `n₁ + 1 = n₂` hold (both maps in the
22+
short complex are given by `X.δ`). All the relevant objects in the
23+
spectral sequence attached to spectral objects can be defined
24+
in terms of this homology `X.E`: the objects in all pages, including
25+
the page at infinity.
26+
27+
## References
28+
* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, II.4][verdier1996]
29+
30+
-/
31+
32+
@[expose] public section
33+
34+
namespace CategoryTheory
35+
36+
open Limits ComposableArrows
37+
38+
namespace Abelian
39+
40+
variable {C ι : Type*} [Category* C] [Category* ι] [Abelian C]
41+
42+
namespace SpectralObject
43+
44+
variable (X : SpectralObject C ι)
45+
46+
section
47+
48+
variable {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
49+
(n₀ n₁ n₂ : ℤ)
50+
51+
/-- The short complex consisting of the composition of
52+
two morphisms `X.δ`, given three composable morphisms `f₁`, `f₂`
53+
and `f₃` in `ι`, and three consecutive integers. -/
54+
@[simps]
55+
def shortComplex (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
56+
ShortComplex C where
57+
X₁ := (X.H n₀).obj (mk₁ f₃)
58+
X₂ := (X.H n₁).obj (mk₁ f₂)
59+
X₃ := (X.H n₂).obj (mk₁ f₁)
60+
f := X.δ f₂ f₃ n₀ n₁
61+
g := X.δ f₁ f₂ n₁ n₂
62+
63+
/-- The homology of the short complex `shortComplex` consisting of
64+
two morphisms `X.δ`. In the documentation, we shorten it as `E^n₁(f₁, f₂, f₃)` -/
65+
noncomputable def E (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : C :=
66+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).homology
67+
68+
lemma isZero_E_of_isZero_H (h : IsZero ((X.H n₁).obj (mk₁ f₂)))
69+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
70+
IsZero (X.E f₁ f₂ f₃ n₀ n₁ n₂) :=
71+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).exact_iff_isZero_homology.1
72+
(ShortComplex.exact_of_isZero_X₂ _ h)
73+
74+
end
75+
76+
section
77+
78+
variable {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
79+
{i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
80+
{i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'') (f₃'' : k'' ⟶ l'')
81+
(α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃')
82+
(β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃'')
83+
(γ : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁'' f₂'' f₃'')
84+
(n₀ n₁ n₂ : ℤ)
85+
86+
/-- The functoriality of `shortComplex` with respect to morphisms
87+
in `ComposableArrows ι 3`. -/
88+
@[simps]
89+
def shortComplexMap (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
90+
X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⟶
91+
X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ where
92+
τ₁ := (X.H n₀).map (homMk₁ (α.app 2) (α.app 3) (naturality' α 2 3))
93+
τ₂ := (X.H n₁).map (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2))
94+
τ₃ := (X.H n₂).map (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
95+
comm₁₂ := δ_naturality ..
96+
comm₂₃ := δ_naturality ..
97+
98+
@[simp]
99+
lemma shortComplexMap_id (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
100+
X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 _) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 _ := by
101+
ext
102+
all_goals dsimp; convert (X.H _).map_id _; cat_disch
103+
104+
@[reassoc, simp]
105+
lemma shortComplexMap_comp (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
106+
X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
107+
X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
108+
X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂ := by
109+
ext
110+
all_goals dsimp; rw [← Functor.map_comp]; congr 1; cat_disch
111+
112+
/-- The functoriality of `E` with respect to morphisms
113+
in `ComposableArrows ι 3`. -/
114+
noncomputable def map (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
115+
X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂ :=
116+
ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂)
117+
118+
@[simp]
119+
lemma map_id (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
120+
X.map f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 _) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 _ := by
121+
dsimp only [map]
122+
simp [shortComplexMap_id, ShortComplex.homologyMap_id]
123+
rfl
124+
125+
set_option backward.isDefEq.respectTransparency false in
126+
@[reassoc, simp]
127+
lemma map_comp (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
128+
X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
129+
X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
130+
X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂ := by
131+
dsimp only [map]
132+
simp [shortComplexMap_comp, ShortComplex.homologyMap_comp]
133+
134+
set_option backward.isDefEq.respectTransparency false in
135+
lemma isIso_map
136+
(h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3).map α)))
137+
(h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3).map α)))
138+
(h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3).map α)))
139+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
140+
IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) := by
141+
have : IsIso (shortComplexMap X f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂) := by
142+
apply +allowSynthFailures ShortComplex.isIso_of_isIso <;> assumption
143+
dsimp [map]
144+
infer_instance
145+
146+
end
147+
148+
section
149+
150+
variable {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
151+
152+
lemma δ_eq_zero_of_isIso₁ (hf : IsIso f) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
153+
X.δ f g n₀ n₁ hn₁ = 0 := by
154+
simpa only [Preadditive.IsIso.comp_left_eq_zero] using X.zero₃ f g _ rfl n₀ n₁
155+
156+
lemma δ_eq_zero_of_isIso₂ (hg : IsIso g) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
157+
X.δ f g n₀ n₁ hn₁ = 0 := by
158+
simpa only [Preadditive.IsIso.comp_right_eq_zero] using X.zero₁ f g _ rfl n₀ n₁
159+
160+
end
161+
162+
set_option backward.isDefEq.respectTransparency false in
163+
lemma isZero_H_obj_of_isIso {i j : ι} (f : i ⟶ j) (hf : IsIso f) (n : ℤ) :
164+
IsZero ((X.H n).obj (mk₁ f)) := by
165+
let e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl _) (asIso f) (by simp)
166+
refine IsZero.of_iso ?_ ((X.H n).mapIso e.symm)
167+
have h := X.zero₂ (𝟙 i) (𝟙 i) (𝟙 i) (by simp) n
168+
rw [← Functor.map_comp] at h
169+
rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← h]
170+
congr 1
171+
cat_disch
172+
173+
section
174+
175+
variable {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
176+
(f₁₂ : i ⟶ k) (h₁₂ : f₁ ≫ f₂ = f₁₂) (f₂₃ : j ⟶ l) (h₂₃ : f₂ ≫ f₃ = f₂₃)
177+
(n₀ n₁ n₂ : ℤ)
178+
179+
set_option backward.isDefEq.respectTransparency false in
180+
/-- `E^n₁(f₁, f₂, f₃)` identifies to the cokernel
181+
of `δToCycles : H^{n₀}(f₃) ⟶ Z^{n₁}(f₁, f₂)`. -/
182+
@[simps]
183+
noncomputable def leftHomologyDataShortComplexE
184+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
185+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := by
186+
let hi := (X.kernelSequenceCycles_exact f₁ f₂ _ _ hn₂).fIsKernel
187+
have : hi.lift (KernelFork.ofι _ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).zero) =
188+
X.δToCycles f₁ f₂ f₃ n₀ n₁ :=
189+
Fork.IsLimit.hom_ext hi (by simpa using hi.fac _ .zero)
190+
exact {
191+
K := X.cycles f₁ f₂ n₁
192+
H := cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁)
193+
i := X.iCycles f₁ f₂ n₁
194+
π := cokernel.π _
195+
wi := by simp
196+
hi := hi
197+
wπ := by rw [this]; simp
198+
hπ := by
199+
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
200+
(cokernelIsCokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁))
201+
· exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
202+
· exact Cofork.ext (Iso.refl _) }
203+
204+
set_option backward.isDefEq.respectTransparency false in
205+
@[simp]
206+
lemma leftHomologyDataShortComplexE_f' (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
207+
(X.leftHomologyDataShortComplexE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f' =
208+
X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ := by
209+
let hi := (X.kernelSequenceCycles_exact f₁ f₂ _ _ hn₂).fIsKernel
210+
exact Fork.IsLimit.hom_ext hi (by simpa using hi.fac _ .zero)
211+
212+
/-- The cycles of the short complex `shortComplexE` at `E^{n₁}(f₁, f₂, f₃)`
213+
identifies to `Z^{n₁}(f₁, f₂)`. -/
214+
noncomputable def cyclesIso (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
215+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles ≅ X.cycles f₁ f₂ n₁ :=
216+
(X.leftHomologyDataShortComplexE f₁ f₂ f₃ n₀ n₁ n₂).cyclesIso
217+
218+
@[reassoc (attr := simp)]
219+
lemma cyclesIso_inv_i (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
220+
(X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ).inv ≫
221+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles = X.iCycles f₁ f₂ n₁ :=
222+
ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles _
223+
224+
@[reassoc (attr := simp)]
225+
lemma cyclesIso_hom_i (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
226+
(X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.iCycles f₁ f₂ n₁ =
227+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ).iCycles :=
228+
ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i _
229+
230+
set_option backward.isDefEq.respectTransparency false in
231+
/-- The epimorphism `Z^{n₁}(f₁, f₂) ⟶ E^{n₁}(f₁, f₂, f₃)`. -/
232+
noncomputable def πE (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
233+
X.cycles f₁ f₂ n₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ :=
234+
(X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂).inv ≫
235+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).homologyπ
236+
deriving Epi
237+
238+
set_option backward.isDefEq.respectTransparency false in
239+
@[reassoc (attr := simp)]
240+
lemma δToCycles_cyclesIso_inv (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
241+
X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv =
242+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ).toCycles := by
243+
simp [← cancel_mono (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).iCycles]
244+
245+
set_option backward.isDefEq.respectTransparency false in
246+
@[reassoc (attr := simp)]
247+
lemma δToCycles_πE (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
248+
X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = 0 := by
249+
simp [πE]
250+
251+
/-- The (exact) sequence `H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃) ⟶ 0`. -/
252+
@[simps]
253+
noncomputable def cokernelSequenceCyclesE
254+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
255+
ShortComplex C :=
256+
ShortComplex.mk _ _ (X.δToCycles_πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
257+
258+
set_option backward.isDefEq.respectTransparency false in
259+
/-- The short complex `H^{n-1}(f₃) ⟶ Z^n(f₁, f₂) ⟶ E^n(f₁, f₂, f₃)` identifies
260+
to the cokernel sequence of the definition of the homology of the short
261+
complex `shortComplexE` as a cokernel of `ShortComplex.toCycles`. -/
262+
@[simps!]
263+
noncomputable def cokernelSequenceCyclesEIso
264+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
265+
X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≅ ShortComplex.mk _ _
266+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles_comp_homologyπ :=
267+
ShortComplex.isoMk (Iso.refl _) (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂).symm
268+
(Iso.refl _) (by simp) (by simp [πE])
269+
270+
lemma cokernelSequenceCyclesE_exact (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
271+
(X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Exact :=
272+
ShortComplex.exact_of_iso (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ).symm
273+
(ShortComplex.exact_of_g_is_cokernel _ (ShortComplex.homologyIsCokernel _))
274+
275+
instance (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) :
276+
Epi (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g := by
277+
dsimp; infer_instance
278+
279+
set_option backward.isDefEq.respectTransparency false in
280+
/-- `E^n₁(f₁, f₂, f₃)` identifies to the kernel
281+
of `δFromOpcycles : opZ^{n₁}(f₂, f₃) ⟶ H^{n₂}(f₁)`. -/
282+
@[simps]
283+
noncomputable def rightHomologyDataShortComplexE
284+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
285+
(X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).RightHomologyData := by
286+
let hp := (X.cokernelSequenceOpcycles_exact f₂ f₃ _ _ hn₁).gIsCokernel
287+
have : hp.desc (CokernelCofork.ofπ _ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ).zero) =
288+
X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ :=
289+
Cofork.IsColimit.hom_ext hp (by simpa using hp.fac _ .one)
290+
exact {
291+
Q := X.opcycles f₂ f₃ n₁
292+
H := kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂)
293+
p := X.pOpcycles f₂ f₃ n₁
294+
ι := kernel.ι _
295+
wp := by simp
296+
hp := hp
297+
wι := by rw [this]; simp
298+
hι := by
299+
refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
300+
(kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))
301+
· exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
302+
· exact Fork.ext (Iso.refl _) }
303+
304+
set_option backward.isDefEq.respectTransparency false in
305+
@[simp]
306+
lemma rightHomologyDataShortComplexE_g'
307+
(hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
308+
(X.rightHomologyDataShortComplexE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' =
309+
X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂ := by
310+
let hp := (X.cokernelSequenceOpcycles_exact f₂ f₃ _ _ hn₁).gIsCokernel
311+
exact Cofork.IsColimit.hom_ext hp (by simpa using hp.fac _ .one)
312+
313+
end
314+
315+
end SpectralObject
316+
317+
end Abelian
318+
319+
end CategoryTheory

0 commit comments

Comments
 (0)