isoOfEquivalence_inv_π — Mathlib

English

The inverse component interacts with projections by: (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j.

Русский

Обратная компонента изоморфизма взаимодействует с проекциями так: (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j.

LaTeX

$$$(\\mathrm{HasLimit.isoOfEquivalence}\,e\,w).inv \\gg \\operatorname{limit.}\\pi F j = \\operatorname{limit.}\\pi G (e.functor.obj j) \\gg w.hom.app j$$$

Lean4

@[simp]
theorem isoOfEquivalence_inv_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F)
    (j : J) : (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j :=
  by
  simp only [HasLimit.isoOfEquivalence]
  simp

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