ranObjObjIsoLimit_inv_π — Mathlib

English

The inverse of the previous isomorphism satisfies the corresponding equation with the limit's projection.

Русский

Обратная к предыдущей изоморфности удовлетворяет соответствующему равенству с проекцией предела.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem ranObjObjIsoLimit_inv_π (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
    (L.ranObjObjIsoLimit F X).inv ≫ (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right = limit.π _ f :=
  RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π (F := F) (isPointwiseRightKanExtensionRanCounit L F X) f

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