single_map_singleObjApplyIso_hom — Mathlib

English

The horizontal (tensor) compatibility for the single-object isomorphism and map morphisms asserts a commutation between the isomorphism hom and the map component.

Русский

Гомоморфизм гомоморфизмов единичного индекса и отображение образуют коммутирующую диаграмму.

LaTeX

$$$(single j).map f j \;\circ\; (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom \circ f$$$

Lean4

@[reassoc (attr := simp)]
theorem single_map_singleObjApplyIso_hom (j : J) {X Y : C} (f : X ⟶ Y) :
    (single j).map f j ≫ (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom ≫ f := by
  apply single_map_singleObjApplyIsoOfEq_hom

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