of_iso_coprod_comparison — Mathlib

English

If the coproduct comparison map is an isomorphism, then G preserves the pair X, Y with respect to colimits.

Русский

Если отображение сопоставления копродукта является изоморфизмом, то G сохраняет пару X,Y относительно колимитов.

LaTeX

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

Lean4

/-- If the coproduct comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
theorem of_iso_coprod_comparison [i : IsIso (coprodComparison G X Y)] : PreservesColimit (pair X Y) G :=
  by
  apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)
  apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
  refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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