η_comp_isoPointwiseLeftKanExtension_hom

English

A natural isomorphism exists between DayFunctor tensor Obj and the left Kan extension unit

Русский

Существует естественный изоморфизм между DayFunctor tensorObj и единицей левого канлевского расслоения.

LaTeX

$$$\\bigl(\\mathrm{DayFunctor}.inst\\tensorObj F G\\bigr).functor \\cong (tensor C).pointwiseLeftKanExtension (F.functor ⊠ G.functor)$$$

Lean4

@[simp]
theorem η_comp_isoPointwiseLeftKanExtension_hom (F G : C ⊛⥤ V) (x y : C) :
    (η F G).app (x, y) ≫ (isoPointwiseLeftKanExtension F G).hom.app (x ⊗ y) =
      Limits.colimit.ι (CostructuredArrow.proj (tensor C) (x ⊗ y) ⋙ F.functor ⊠ G.functor)
        (.mk (Y := (x, y)) <| 𝟙 (x ⊗ y)) :=
  by
  simpa [η, isoPointwiseLeftKanExtension] using
    Functor.descOfIsLeftKanExtension_fac_app (F ⊗ G).functor (η F G) _
      ((tensor C).pointwiseLeftKanExtensionUnit (F.functor ⊠ G.functor)) (x, y)

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