English
A natural transformation α: F ⇒ G induces a morphism between leftDerived functors: F.leftDerived n ⟶ G.leftDerived n.
Русский
Естественное преобразование α: F ⇒ G индуцирует отображение между левыми производными: F.leftDerived n ⟶ G.leftDerived n.
LaTeX
$$$\alpha: F \Rightarrow G \Rightarrow \text{leftDerived }(\alpha,n): F.leftDerived n \Rightarrow G.leftDerived n$$$
Lean4
@[reassoc]
theorem fromLeftDerivedZero'_naturality {C} [Category C] [Abelian C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X)
(Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) (F : C ⥤ D)
[F.Additive] :
HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex _).map φ) 0 ≫ Q.fromLeftDerivedZero' F =
P.fromLeftDerivedZero' F ≫ F.map f :=
by
simp only [← cancel_epi (HomologicalComplex.pOpcycles _ _), ← F.map_comp, comm,
HomologicalComplex.p_opcyclesMap_assoc, Functor.mapHomologicalComplex_map_f, pOpcycles_comp_fromLeftDerivedZero',
pOpcycles_comp_fromLeftDerivedZero'_assoc]
