instEssSurjUnderToUnder — Mathlib

English

If F is essentially surjective, then the projection functor from the structured-arrow category to the under-category is essentially surjective.

Русский

Если F существенно сюръективен, то переходник из структуры-стрелки к under-категории сюръективен по существу.

LaTeX

$$$\mathsf{EssSurj}\big(\mathrm{toUnder}(X,F)\big)$$$

Lean4

instance (X : T) (F : D ⥤ T) [F.EssSurj] : (toUnder X F).EssSurj :=
  show (StructuredArrow.pre _ _ _).EssSurj from inferInstance

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