singleObjApplyIso_inv_single_map — Mathlib

English

The inverse of the single-object application is compatible with map translations under index equality, establishing a commuting square with the inverse isomorphisms.

Русский

Обратный к каноническому отображению для единичного индекса совместим с отображениями при равенстве индексов, образуя диагональ-подобный квадрат.

LaTeX

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

Lean4

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

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