rightDerivedNatTrans_comp — Mathlib

English

Let e: X ≅ Y be an isomorphism in C and F: C ⥤ D ⥤ E a functor; then for any Z in D, (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙.

Русский

Пусть e: X ≅ Y — изоморфизм в C, и F: C ⥤ D ⥤ E — функтор; тогда для любого Z ∈ D выполняется (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙.

LaTeX

$$$ (F.map e.hom).app Z \circ (F.map e.inv).app Z = 𝟙_{(F.obj Y).obj Z} $$$

Lean4

@[reassoc (attr := simp)]
theorem rightDerivedNatTrans_comp (τ : F ⟶ F') (τ' : F' ⟶ F'') :
    rightDerivedNatTrans RF RF' α α' W τ ≫ rightDerivedNatTrans RF' RF'' α' α'' W τ' =
      rightDerivedNatTrans RF RF'' α α'' W (τ ≫ τ') :=
  rightDerived_ext RF α W _ _ _ (by simp)

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