ranObjObjIsoLimit_hom_π — Mathlib

English

There is a canonical equality relating the hom component of the ranObjObjIsoLimit and the projections from a limit, matching the counit with the map f.hom.

Русский

Существует каноническое равенство между компонентами гом и проекциями предела, сопряжающее единицу и отображение f.hom через counit.

LaTeX

$$$ (L.ranObjObjIsoLimit F X).hom \\; \\pi_f = (L.ran.obj F).map f.hom \\; \\circ \\; (L.ranCounit.app F).app f.right, $$$

Lean4

@[reassoc (attr := simp)]
theorem ranObjObjIsoLimit_hom_π (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
    (L.ranObjObjIsoLimit F X).hom ≫ limit.π _ f = (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right := by
  simp [ranObjObjIsoLimit, ran, ranCounit]

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