prodComparisonIso_comp — Mathlib

English

For F: C → D and G: D → E with suitable preservation of limits, prodComparison Iso (F ⋙ G) A B equals the composite of G.mapIso (prodComparisonIso F A B) with prodComparisonIso G (F.obj A) (F.obj B).

Русский

Для F: C → D и G: D → E с подходящим сохранением пределов, prodComparisonIso (F ⋙ G) A B равен композиции G.mapIso (prodComparisonIso F A B) с prodComparisonIso G (F.obj A) (F.obj B).

LaTeX

$$$$ prodComparisonIso (F \cdot G) A B = G.mapIso (prodComparisonIso F A B) \; \succ \; prodComparisonIso G (F.obj A) (F.obj B). $$$$

Lean4

@[simp]
theorem prodComparisonIso_comp [PreservesLimit (pair A B) (F ⋙ G)] [PreservesLimit (pair (F.obj A) (F.obj B)) G] :
    prodComparisonIso (F ⋙ G) A B = G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B) := by
  ext <;> simp [CartesianMonoidalCategory.prodComparison, ← G.map_comp]

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