limitIsoPi_inv_comp_pi — Mathlib

English

In a finite index setting, the inverse of the limit iso composed with a projection equals the projection map from the wide pullback.

Русский

В конечной индексации отношение обратного изоморфизма предела и проекции равно проекции из широкого обратного предела.

LaTeX

$$$(\\text{wideCospan}.\\text{limitIsoPi} ι X)^{-1} \\circ \\mathrm{WidePullback}.π_{\\,j} = \\mathrm{Pi}.π_{\\,j}$$$

Lean4

@[reassoc (attr := simp)]
theorem limitIsoPi_inv_comp_pi [Finite ι] (X : C) (j : ι) :
    (wideCospan.limitIsoPi ι X).inv ≫ WidePullback.π _ j = Pi.π _ j :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

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