mapComp'_hom_naturality — Mathlib

English

For a pseudofunctor F and composable arrows f : b0 ⟶ b1, g : b1 ⟶ b2, fg : b0 ⟶ b2 with hfg : f ≫ g = fg, the naturality of the map on a holds with respect to the inverse of mapComp' and the map on a.

Русский

Пусть F — псевдофунктор, f : b0 ⟶ b1, g : b1 ⟶ b2, fg : b0 ⟶ b2 так, что hfg : f ≫ g = fg. Тогда естественность отображения на a относительно mapComp' соблюдается: (F.map fg).map a ≫ (F.mapComp' f g fg hfg).hom.app Y = (F.mapComp' f g fg hfg).hom.app X ≫ (F.map g).map ((F.map f).map a).

LaTeX

$$$ (F.map fg).map a ≫ (F.mapComp' f g fg hfg).hom.app Y = (F.mapComp' f g fg hfg).hom.app X ≫ (F.map g).map ((F.map f).map a) $$$

Lean4

@[reassoc]
theorem mapComp'_hom_naturality :
    (F.map fg).map a ≫ (F.mapComp' f g fg hfg).hom.app Y =
      (F.mapComp' f g fg hfg).hom.app X ≫ (F.map g).map ((F.map f).map a) :=
  (F.mapComp' f g fg hfg).hom.naturality a

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