instIsCocontinuousOverForgetOver — Mathlib

English

For every X, the forgetful functor Over forget X is cocontinuous with respect to J.over X and J, i.e., it preserves colimits along the forgetful direction.

Русский

Для каждого X забывающая функция Over forget X является ко-континьюутной/коконтинуальной относительно J.over X и J, т. е. сохраняет колимиты вдоль забывания.

LaTeX

$$$\\forall X:\\ C,\\; (Over.forget X).IsCocontinuous (J.over X) J$$$

Lean4

instance (X : C) : (Over.forget X).IsCocontinuous (J.over X) J where cover_lift hS := J.overEquiv_symm_mem_over _ _ hS

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