mapAut

Mathlib.CategoryTheory.Endomorphism

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

← MathLib Explorer

English

Map Aut X to Aut (f.obj X) as monoid hom.

Русский

Перевод Aut X в Aut (f.obj X) как моноид-гомоморфизм.

LaTeX

$$$\text{mapAut}: Aut(X) \to Aut(f.X)$$$

Lean4

/-- `f.mapIso` as a group hom between automorphism groups. -/
def mapAut : Aut X →* Aut (f.obj X) where
  toFun := f.mapIso
  map_mul' x y := f.mapIso_trans y x
  map_one' := f.mapIso_refl X

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

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

Разделы

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

Аффилиация

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