ι_comp_isoPointwiseLeftKanExtension_inv

English

Alternate expression for the colimit-ι composition with the isoPointwiseLeftKanExtension inverse

Русский

Альтернативное выражение композиции colimit-ι с обратным isoPointwiseLeftKanExtension.

LaTeX

$$$\\iota_{(x,y)} \\circ (\\mathrm{isoPointwiseLeftKanExtension})_{(x \\otimes y)}^{-1} = \\eta_{(F,G)}(x,y)$$$

Lean4

@[simp]
theorem ι_comp_isoPointwiseLeftKanExtension_inv (F G : C ⊛⥤ V) (x y : C) :
    Limits.colimit.ι (CostructuredArrow.proj (tensor C) (x ⊗ y) ⋙ F.functor ⊠ G.functor)
          (.mk (Y := (x, y)) <| 𝟙 (x ⊗ y)) ≫
        (isoPointwiseLeftKanExtension F G).inv.app (x ⊗ y) =
      (η F G).app (x, y) :=
  by simp [η, isoPointwiseLeftKanExtension]

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