mono

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Fork.IsLimit.mono

English

If s is a limit fork for f,g, then the leg s.ι is a monomorphism:

Русский

Если s является пределом-форк для f,g, то стрелка s.ι является моноэмо

LaTeX

$$$\operatorname{IsLimit}(s) \Rightarrow \operatorname{Mono}(s.\iota)$$$

Lean4

theorem mono {s : Fork f g} (hs : IsLimit s) : Mono s.ι where right_cancellation _ _ h := hom_ext hs h

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

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

Разделы

Аффилиация

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