English
Let f: X → Y be a morphism in C, with P ⟶ Q a morphism of cocomplexes representing maps between injective resolutions. For any additive F, a naturality condition holds relating F.map f, Q.toRightDerivedZero' F, and P.toRightDerivedZero' F via the cycles map of φ.
Русский
Пусть f: X → Y — морфизм в C, и φ: P.cocomplex ⟶ Q.cocomplex — отображение между разрешениями. Для любого аддитивного F выполняется естественность: F.map f слагается с Q.toRightDerivedZero' F и равно P.toRightDerivedZero' F через cyclesMap φ.
LaTeX
$$$F.map f ≫ Q.toRightDerivedZero' F = P.toRightDerivedZero' F ≫ \operatorname{HomologicalComplex.cyclesMap} \big( (F.mapHomologicalComplex (ComplexShape.up \Nat)).map \varphi \big) 0$$$
Lean4
@[reassoc]
theorem toRightDerivedZero'_naturality {C} [Category C] [Abelian C] {X Y : C} (f : X ⟶ Y) (P : InjectiveResolution X)
(Q : InjectiveResolution Y) (φ : P.cocomplex ⟶ Q.cocomplex) (comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0) (F : C ⥤ D)
[F.Additive] :
F.map f ≫ Q.toRightDerivedZero' F =
P.toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex _).map φ) 0 :=
by
simp only [← cancel_mono (HomologicalComplex.iCycles _ _), Functor.mapHomologicalComplex_obj_X, assoc,
toRightDerivedZero'_comp_iCycles, CochainComplex.single₀_obj_zero, HomologicalComplex.cyclesMap_i,
Functor.mapHomologicalComplex_map_f, toRightDerivedZero'_comp_iCycles_assoc, ← F.map_comp, comm]
