leftDerivedNatTrans_fac — Mathlib

English

LeftDerivedNatTrans_fac describes how leftDerivedNatTrans interacts with composing natural transformations τ: F′ ⟶ F.

Русский

LeftDerivedNatTrans_fac описывает взаимодействие leftDerivedNatTrans с композицией натрансформаций τ: F′ ⟶ F.

LaTeX

$$$$ \\mathrm{leftDerivedNatTrans}_{LF',LF,α',α,W}(τ) \\circ α' = α \\circ τ. $$$$

Lean4

@[reassoc (attr := simp)]
theorem leftDerivedNatTrans_fac (τ : F' ⟶ F) : whiskerLeft L (leftDerivedNatTrans LF' LF α' α W τ) ≫ α = α' ≫ τ :=
  by
  dsimp only [leftDerivedNatTrans]
  simp

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