limMap_mono'

Mathlib.CategoryTheory.Limits.HasLimits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.limMap_mono'

English

If α: F ⟶ G is mono, then the induced map limMap α is mono.

Русский

Если α: F ⟶ G моно, то индуцированное отображение limMap α моно.

LaTeX

$$$\\mathrm{Mono}(\\mathrm{limMap}(\\alpha))$$$

Lean4

instance limMap_mono' {F G : J ⥤ C} [HasLimitsOfShape J C] (α : F ⟶ G) [Mono α] : Mono (limMap α) :=
  (lim : (J ⥤ C) ⥤ C).map_mono α

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru