liftNatTrans_add — Mathlib

English

The lift of a sum of natural transformations equals the sum of the lifts.

Русский

Подъем суммы натрансформаций равен сумме подъемов.

LaTeX

$$$liftNatTrans\\ L\\ W\\ F_1\\ F_2\\ F_1'\\ F_2'\\ (\\tau + \\tau') = liftNatTrans\\ L\\ W\\ F_1\\ F_2\\ F_1'\\ F_2'\\ \\tau + liftNatTrans\\ L\\ W\\ F_1\\ F_2\\ F_1'\\ F_2'\\ \\tau'$$$

Lean4

theorem liftNatTrans_add (F₁ F₂ : C ⥤ E) (F₁' F₂' : D ⥤ E) [Lifting L W F₁ F₁'] [Lifting L W 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 (by simp)

Похожие утверждения