plusMap_comp — Mathlib

English

Composition compatibility: plusMap (η ≫ γ) equals plusMap η then plusMap γ.

Русский

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

LaTeX

$$$J.plusMap(\\eta \\circ \\gamma) = J.plusMap(\\eta) \\circ J.plusMap(\\gamma)$$$

Lean4

@[simp, reassoc]
theorem plusMap_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) : J.plusMap (η ≫ γ) = J.plusMap η ≫ J.plusMap γ :=
  by
  ext : 2
  refine colimit.hom_ext (fun S => ?_)
  simp [plusMap, J.diagramNatTrans_comp]

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