comp_autMap

Mathlib.CategoryTheory.Galois.GaloisObjects

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

← MathLib Explorer

English

If X is Galois, then the quotient X/Aut X is terminal.

Русский

Если X галуа, то фактор X/Aut X является терминальным.

LaTeX

$$$\text{IsTerminal}\Bigl(\operatorname{colimit}(\mathrm{SingleObj.functor}(\mathrm{Aut.toEnd} X))\Bigr)$$$

Lean4

@[simp]
theorem comp_autMap {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) : f ≫ (autMap f σ).hom = σ.hom ≫ f :=
  (exists_autMap f σ).choose_spec.left

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

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

Разделы

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

Аффилиация

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