mono_homMk

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StructuredArrow.mono_homMk

English

For f : S ⟶ T.obj Y, g : Y ⟶ Y', g' : Y' ⟶ Y'',

Русский

Для f : S ⟶ T.obj Y, g : Y ⟶ Y', g' : Y' ⟶ Y''

LaTeX

$$$homMk' (mk f) (g \circ g') = homMk' (mk f) g \circ homMk' (mk (f \circ T.map g)) g' \circ eqToHom (by simp)$$$

Lean4

instance mono_homMk {A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h : Mono f] : Mono (homMk f w) :=
  (proj S T).mono_of_mono_map h

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

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

Разделы

Аффилиация

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