instEssSurjOverToOver — Mathlib

English

If F: D ⥤ T is ess-surjective, then the induced functor toOver F X is ess-surjective.

Русский

Если F: D ⥤ T является эс-сюръективным, то индуцированный функтор toOver(F,X) эс-сюръективен.

LaTeX

$$$F:\\mathcal{D} \\to \\mathcal{T}$ ess-surjective \\Rightarrow \\operatorname{EssSurj}(\\mathrm{toOver}(F,X)).$$$

Lean4

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

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