pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac

English

An auxiliary fac-app lemma for the inverse facet in the preserved isomorphism.

Русский

Вспомогательная лемма о фаске и компоненте для сохраняемого изоморфизма.

LaTeX

$$$\text{PreservesIso_fac_app}$$$

Lean4

@[reassoc (attr := simp)]
theorem pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac :
    (L.pointwiseLeftKanExtensionUnit <| F ⋙ G) ≫ whiskerLeft L (pointwiseLeftKanExtensionCompIsoOfPreserves G F L).inv =
      whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom :=
  by simp [pointwiseLeftKanExtensionCompIsoOfPreserves]

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