preservesLimitIso_hom_π — Mathlib

English

The hom component of the preservesLimitIso is given by mapping projections: (preservesLimitIso G F).hom ≫ limit.π (F⋅G) j = G.map (limit.π F j).

Русский

Гом-часть preservesLimitIso задается отображением проекции: hom ≫ π = G.map(π).

LaTeX

$$$(\\text{preservesLimitIso } G F).hom \\; \\circ \\lim\\!\\pi\\!_{F G} j = G.map(\\lim\\pi_F j)$$$

Lean4

@[reassoc (attr := simp)]
theorem preservesLimitIso_hom_π (j) : (preservesLimitIso G F).hom ≫ limit.π _ j = G.map (limit.π F j) :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ j

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