mapEnd

Mathlib.CategoryTheory.Endomorphism

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

← MathLib Explorer

English

Map from End X to End (f.obj X) induced by a functor f.

Русский

Гомоморфизм End X к End (f.obj X) индукцируется через функтор f.

LaTeX

$$$\text{mapEnd}: End(X) \to End(f(X))$ as monoid hom$$

Lean4

/-- `f.map` as a monoid hom between endomorphism monoids. -/
@[simps]
def mapEnd : End X →* End (f.obj X) where
  toFun := f.map
  map_mul' x y := f.map_comp y x
  map_one' := f.map_id X

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

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

Разделы

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

Аффилиация

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