mono

Mathlib.CategoryTheory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SplitMono.mono

← MathLib Explorer

English

Every split mono is a mono.

Русский

Каждый разложимый моно является моно.

LaTeX

$$$\\text{SplitMono}(f) \\Rightarrow \\text{Mono}(f)$$$

Lean4

theorem mono {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f :=
  { right_cancellation := fun g h w => by replace w := w =≫ sm.retraction; simpa using w }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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