preservesBinaryProducts_of_isIso_prodComparison

English

Similarly, for the colimit side, the coproduct comparison is an iso when limits are preserved.

Русский

Аналогично на стороне колимитаCoprod, сопоставление копроедного произведения является изоморфизмом при сохранении пределов.

LaTeX

$$$\text{IsIso}(\mathrm{coprodComparison} G X Y)$$$

Lean4

/-- If the product comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary products. -/
theorem preservesBinaryProducts_of_isIso_prodComparison [HasBinaryProducts C] [HasBinaryProducts D]
    [i : ∀ {X Y : C}, IsIso (prodComparison G X Y)] : PreservesLimitsOfShape (Discrete WalkingPair) G where
  preservesLimit := by
    intro K
    have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesLimitPair.of_iso_prod_comparison ..
    apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm

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