instGroup

Mathlib.CategoryTheory.Endomorphism

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Aut.instGroup

← MathLib Explorer

English

Units of the endomorphism monoid correspond to automorphisms of X.

Русский

Единицы моноида End X соответствуют автоморфизмам X.

LaTeX

$$$ (End(X))^{\times} \cong Aut(X) $$$

Lean4

instance : Group (Aut X) where
  one := Iso.refl X
  inv := Iso.symm
  mul x y := Iso.trans y x
  mul_assoc _ _ _ := (Iso.trans_assoc _ _ _).symm
  one_mul := Iso.trans_refl
  mul_one := Iso.refl_trans
  inv_mul_cancel := Iso.self_symm_id

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

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

Разделы

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

Аффилиация

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