prodComparison_natural_whiskerRight

English

Naturality of prodComparisonNatTrans with respect to left whiskering: the left whisker with f commutes with prodComparison via the natural transformation.

Русский

Естественность prodComparisonNatTrans по отношению к левому взвешиванию: левое взвешивание f коммутирует с prodComparison через естественную трансформацию.

LaTeX

$$prodComparisonNatTrans_natural_left F A f g$$

Lean4

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

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