reflectsMonomorphisms_of_faithful

Mathlib.CategoryTheory.Functor.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.reflectsMonomorphisms_of_faithful

← MathLib Explorer

English

If F is faithful, then F reflects monomorphisms.

Русский

Если F верен (faithful), тогда F отражает мономорфизмы.

LaTeX

$$ReflectsMonomorphisms F$$

Lean4

instance (priority := 100) reflectsMonomorphisms_of_faithful (F : C ⥤ D) [Faithful F] : ReflectsMonomorphisms F where
  reflects {X} {Y} f
    _ := ⟨fun {Z} g h hgh => F.map_injective ((cancel_mono (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩

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

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

Разделы

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

Аффилиация

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