diagramNatTrans_comp — Mathlib

English

The plus-map respects composition: plusMap(η ≫ γ) = plusMap(η) ≫ plusMap(γ).

Русский

Сохранение композиции: плюс-карта от композиции равна композиции плюс-карт.

LaTeX

$$$J.plusMap(\\eta \\;\\hspace{-1pt} \\gamma) = J.plusMap(\\eta) \\circ J.plusMap(\\gamma)$$$

Lean4

@[simp]
theorem diagramNatTrans_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) :
    J.diagramNatTrans (η ≫ γ) X = J.diagramNatTrans η X ≫ J.diagramNatTrans γ X :=
  by
  ext : 2
  refine Multiequalizer.hom_ext _ _ _ (fun i => ?_)
  simp

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