instGroupAutGalois

Mathlib.CategoryTheory.Galois.Prorepresentability

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

English

The Aut F object yields a fundamental group structure for the category Aut F in the Galois setting.

Русский

Объект Aut F дает структуру фундаментальной группы в контексте Galois.

LaTeX

$$$\text{IsFundamentalGroup}(F, Aut F)$$$

Lean4

noncomputable instance : Group (AutGalois F) :=
  inferInstanceAs <| Group (autGaloisSystem F ⋙ forget _).sections

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

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

Разделы

Аффилиация

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