instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp

English

A standard identity expresses that the kernel of d g composed with d f is zero under separator hypotheses.

Русский

Стандартное равенство: ядро композиции d g и d f равно нулю при условии разделителя.

LaTeX

$$$\\ker(ι_{d g})\\circ d f = 0$$$

Lean4

instance {X Y : C} (f : X ⟶ Y) : Mono (monoMapFactorizationDataRlp f).i :=
  (monoMapFactorizationDataRlp f).hi

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

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

Разделы

Аффилиация

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