of_iso_prod_comparison — Mathlib

English

If the product comparison map at (X,Y) is an isomorphism, then G preserves the limit of the pair (X,Y).

Русский

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

LaTeX

$$$\text{IsIso}(\,\mathrm{prodComparison}\ G\ X\ Y\,) \;\Rightarrow\; \text{PreservesLimit}(\text{pair } X Y)\ G$$$

Lean4

/-- If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
theorem of_iso_prod_comparison [i : IsIso (prodComparison G X Y)] : PreservesLimit (pair X Y) G :=
  by
  apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)
  apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
  refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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