autMap_id

Mathlib.CategoryTheory.Galois.GaloisObjects

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.autMap_id

English

For any A with IsGalois, autMap(identity on A) equals the identity automorphism on A.

Русский

Для любого A с IsGalois, autMap(идентичное отображение на A) равно единице как автоморфизм A.

LaTeX

$$$autMap(\mathrm{id}_A) = \mathrm{id}$$$

Lean4

@[simp]
theorem autMap_id {A : C} [IsGalois A] : autMap (𝟙 A) = id :=
  funext fun σ ↦ autMap_unique (𝟙 A) σ _ (by simp)

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

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

Разделы

Аффилиация

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