prodComparison_inv_natural_whiskerLeft

English

If prodComparison is iso, its inverse is natural in both arguments; i.e., inv(prodComparison F A B) commutes with tensor maps.

Русский

Если prodComparison — изоморфизм, то его обратная часть естественна по обеим аргументам; то есть inv(prodComparison F A B) commute с tensor maps.

LaTeX

$$prodComparison_inv_natural F A B f g [IsIso (prodComparison F A' B')]$$

Lean4

/-- If the product comparison morphism is an iso, its inverse is natural in the right argument. -/
@[reassoc]
theorem prodComparison_inv_natural_whiskerLeft (g : B ⟶ B') [IsIso (prodComparison F A B')] :
    inv (prodComparison F A B) ≫ F.map (A ◁ g) = (F.obj A ◁ F.map g) ≫ inv (prodComparison F A B') := by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]

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