English
The composition of two left-derived natural transformations is again a left-derived natural transformation, corresponding to the composition of the underlying morphisms.
Русский
Сложение двух лев Derived натрансформаций снова даёт лев Derived натрансформацию и соответствует композиции базовых морфизмов.
LaTeX
$$$$ \\big(\\mathrm{leftDerivedNatTrans}\\; LF'' LF' α'' α' W τ' \\big) \\;\\ggg \\big(\\mathrm{leftDerivedNatTrans}\\; LF' LF α' α W τ \\big) \;=\; \\mathrm{leftDerivedNatTrans}\\; LF'' LF α'' α W (τ' \\circ τ). $$$$
Lean4
@[reassoc (attr := simp)]
theorem derivedη_fac_app (X₁ : C₁) :
(adj.derivedη W₁ α β).app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁) := by
simpa using
((G' ⋙ F').leftDerived_fac_app ((Functor.associator _ _ _).inv ≫ whiskerRight α F') W₁ _
(L₁.rightUnitor.hom ≫
L₁.leftUnitor.inv ≫
whiskerRight adj.unit L₁ ≫
(Functor.associator _ _ _).hom ≫ whiskerLeft G β ≫ (Functor.associator _ _ _).inv))
X₁
