English
If liftNatTrans is taken for all segments, then the composition of lifted natural transformations equals the lift of the composed transformations: lift τ ∘ lift τ' = lift(τ ≫ τ').
Русский
Если для всех частей взять liftNatTrans, то композиция поднятых натуралных преобразований равна lift от композиции преобразований: lift(τ) ∘ lift(τ′) = lift(τ ≫ τ′).
LaTeX
$$$\\text{liftNatTrans } L W F_1 F_2 F_1' F_2' \\tau \\;\\gg\\; \\text{liftNatTrans } L W F_2 F_3 F_2' F_3' \\tau' = \\text{liftNatTrans } L W F_1 F_3 F_1' F_3' (\\tau \\gg \\tau').$$$
Lean4
@[reassoc (attr := simp)]
theorem comp_liftNatTrans (F₁ F₂ F₃ : C ⥤ E) (F₁' F₂' F₃' : D ⥤ E) [h₁ : Lifting L W F₁ F₁'] [h₂ : Lifting L W F₂ F₂']
[h₃ : Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) :
liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ' = liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ') :=
natTrans_ext L W fun X => by simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]
