pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac

English

A similar isomorphism-facility holds for the pointwise left Kan extension when preserving is assumed.

Русский

При сохранении сохраняется аналогичная изоморфность для точечного левого кан-расширения.

LaTeX

$$$\text{pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac}$$$

Lean4

@[reassoc (attr := simp)]
theorem pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac :
    whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
        (Functor.associator _ _ _).hom ≫ whiskerLeft L (pointwiseLeftKanExtensionCompIsoOfPreserves G F L).hom =
      (L.pointwiseLeftKanExtensionUnit <| F ⋙ G) :=
  by
  simpa [pointwiseLeftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac (α :=
      whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom) (β :=
      L.pointwiseLeftKanExtensionUnit <| F ⋙ G)

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