instEssSurjSkeletonMapSkeleton — Mathlib

English

If a functor F: C ⥤ D is essentially surjective, then the induced functor on skeletons mapSkeleton is essentially surjective as well.

Русский

Если однозначный функтор F: C ⥤ D является эссенциально сюръективным, то порождающий его переход на skeletons mapSkeleton также эссенциально сюръективен.

LaTeX

$$$F\\text{.EssSurj} \\rightarrow F\\text{.mapSkeleton}.EssSurj$$$

Lean4

instance [F.EssSurj] : F.mapSkeleton.EssSurj := by unfold mapSkeleton; infer_instance

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