mapId'_inv_naturality — Mathlib

English

For a pseudofunctor F and f : b0 ⟶ b0 with hf: f = id, the inverse map interacts with the naturality of map on a: (F.mapId' f hf).inv.app X ≫ (F.map f).map a = a ≫ (F.mapId' f hf).inv.app Y.

Русский

Пусть F — псевдофунктор, f : b0 ⟶ b0 с hf: f = id. Тогда обратная компонента отображения совместима с естественностью отображения на a: (F.mapId' f hf).inv.app X ≫ (F.map f).map a = a ≫ (F.mapId' f hf).inv.app Y.

LaTeX

$$$ (F.mapId' f hf).inv.app X \; \circ \; (F.map f).map a = a \; \circ \; (F.mapId' f hf).inv.app Y $$$

Lean4

@[reassoc]
theorem mapId'_inv_naturality : (F.mapId' f hf).inv.app X ≫ (F.map f).map a = a ≫ (F.mapId' f hf).inv.app Y :=
  ((F.mapId' f hf).inv.naturality a).symm

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