leftDerivedNatTrans_comp — Mathlib

English

A composition law for left-derived natural transformations: composing two such maps corresponds to composing their underlying morphisms.

Русский

Свойство композиции левогоDerivedNatTrans: композиция двух таких отображений соответствует композиции базовых морфизмов.

LaTeX

$$$$ leftDerivedNatTrans LF'' LF' α'' α' W τ' ≫ leftDerivedNatTrans LF' LF α' α W τ = leftDerivedNatTrans LF'' LF α'' α W (τ' ≫ τ). $$$$

Lean4

@[reassoc (attr := simp)]
theorem leftDerivedNatTrans_comp (τ' : F'' ⟶ F') (τ : F' ⟶ F) :
    leftDerivedNatTrans LF'' LF' α'' α' W τ' ≫ leftDerivedNatTrans LF' LF α' α W τ =
      leftDerivedNatTrans LF'' LF α'' α W (τ' ≫ τ) :=
  leftDerived_ext LF α W _ _ _ (by simp)

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