isoMkFunctor — Mathlib

English

Any functor out of a join is naturally isomorphic to a mkFunctor of its projections.

Русский

Любой функтор из объединения категорий естественно изоморфен mkFunctor, построенному из его проекций.

LaTeX

$$$ \mathrm{F} \cong \mathrm{mkFunctor}(\mathrm{inclLeft} C D \circ F)(\mathrm{inclRight} C D \circ F)(\mathrm{whiskerRight}(\mathrm{edgeTransform} C D) F) $$$

Lean4

/-- Any functor out of a join is naturally isomorphic to a functor of the form `mkFunctor F G α`. -/
@[simps!]
def isoMkFunctor (F : C ⋆ D ⥤ E) :
    F ≅ mkFunctor (inclLeft C D ⋙ F) (inclRight C D ⋙ F) (whiskerRight (edgeTransform C D) F) :=
  mkNatIso (mkFunctorLeft _ _ _).symm (mkFunctorRight _ _ _).symm

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