limitIsoPi_hom_comp_pi — Mathlib

English

The hom component of the limit iso composed with a projection equals the projection from the wide pullback.

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem limitIsoPi_hom_comp_pi [Finite ι] (X : C) (j : ι) :
    (wideCospan.limitIsoPi ι X).hom ≫ Pi.π _ j = WidePullback.π _ j := by
  rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]

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