map_ofHom

Mathlib.CategoryTheory.Localization.CalculusOfFractions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.RightFraction.map_ofHom

← MathLib Explorer

English

Same content as above: the map of a Hom-constructed fraction equals the direct map.

Русский

То же самое: отображение дроби через Hom равно прямому отображению.

LaTeX

$$(\mathrm{ofHom} W f).map L hL = L.map f$$

Lean4

@[simp]
theorem map_ofHom (f : X ⟶ Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) [W.ContainsIdentities] :
    (ofHom W f).map L hL = L.map f := by simp [map]

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

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

Разделы

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

Аффилиация

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