mapId'_hom_naturality — Mathlib

English

For a pseudofunctor F and f : b0 ⟶ b0 with hf: f = id, the naturality of the map on a with respect to the identity morphism holds: (F.map f).map a commutes with the identity component map on X and Y.

Русский

Пусть F — псевдофунктор, f : b0 ⟶ b0 с hf: f = id. Тогда естественность отображения на a по отношению к единичному морфизму выполняется: (F.map f).map a корректно компонуется с компонентой отображения id на X и Y.

LaTeX

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

Lean4

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

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