mapComp'_naturality_2 — Mathlib

English

For a lax functor F and arrows f,g,fg with hfg, the naturality of mapComp' in the first slot holds: the left side with inv.app X and map a equals the right side with (F.map g).map ((F.map f).map a).

Русский

Для слабого функторa F и стрел f,g,fg с hfg естественность mapComp' в первом компоненте: левый член с inv.app X и a равен правому члену с (F.map g).map ((F.map f).map a).

LaTeX

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

Lean4

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

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