preservesBinaryCoproducts_of_isIso_coprodComparison

English

Under a preserved limit structure, the product comparison morphism is an isomorphism.

Русский

При сохранённой структуре предела отображение произведения является изоморфизмом.

LaTeX

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

Lean4

/-- If the coproduct comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary coproducts. -/
theorem preservesBinaryCoproducts_of_isIso_coprodComparison [HasBinaryCoproducts C] [HasBinaryCoproducts D]
    [i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)] : PreservesColimitsOfShape (Discrete WalkingPair) G where
  preservesColimit := by
    intro K
    have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
    apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

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