prodComparisonNatTrans_comp — Mathlib

English

Naturality of the prodComparisonNatTrans with respect to composition of functors: prodComparisonNatTrans (F ⋙ G) A equals whisker compositions of prodComparisonNatTrans F and prodComparisonNatTrans G.

Русский

Естественность prodComparisonNatTrans по отношению к композиции функторов: prodComparisonNatTrans (F ⋙ G) A равняется композициям whisker.

LaTeX

$$prodComparisonNatTrans (F ⋙ G) A = Functor.whiskerRight (prodComparisonNatTrans F A) G ≫ Functor.whiskerLeft F (prodComparisonNatTrans G (F.obj A))$$

Lean4

theorem prodComparisonNatTrans_comp :
    prodComparisonNatTrans (F ⋙ G) A =
      Functor.whiskerRight (prodComparisonNatTrans F A) G ≫
        Functor.whiskerLeft F (prodComparisonNatTrans G (F.obj A)) :=
  by ext; simp [prodComparison_comp]

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