prodComparison_natural_whiskerLeft

English

Naturality of prodComparisonNatTrans with respect to composition of functors: prodComparisonNatTrans (F ∘ G) A equals whisker compositions of prodComparisonNatTrans F and G with appropriate whiskers.

Русский

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

LaTeX

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

Lean4

/-- Naturality of the `prodComparison` morphism in the right argument. -/
@[reassoc]
theorem prodComparison_natural_whiskerLeft (g : B ⟶ B') :
    F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ (F.obj A ◁ F.map g) := by
  ext <;> simp [← Functor.map_comp]

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