prodComparison_inv_natural — Mathlib

English

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

Русский

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

LaTeX

$$prodComparisonNatTrans_natural_right F G A$$

Lean4

/-- If the product comparison morphism is an iso, its inverse is natural in both argument. -/
@[reassoc]
theorem prodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] :
    inv (prodComparison F A B) ≫ F.map (f ⊗ₘ g) = (F.map f ⊗ₘ F.map g) ≫ inv (prodComparison F A' B') := by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

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