conjAut

Mathlib.CategoryTheory.Conj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.conjAut

← MathLib Explorer

English

Conjugation by α induces a group isomorphism Aut X ≃* Aut Y.

Русский

Конъюгация α порождает изоморфизм групп Aut X и Aut Y.

LaTeX

$$$\\mathrm{conjAut}: \\mathrm{Aut}(X) \\simeq^* \\mathrm{Aut}(Y)$$$

Lean4

/-- `conj` defines a group isomorphisms between groups of automorphisms -/
def conjAut : Aut X ≃* Aut Y :=
  (Aut.unitsEndEquivAut X).symm.trans <| (Units.mapEquiv α.conj).trans <| Aut.unitsEndEquivAut Y

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

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

Разделы

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

Аффилиация

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