instIsPretransitiveCarrierObjFintypeCatOfIsConnected

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

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

English

If every X with IsGalois has pretransitive G-action, then toAut F G is surjective.

Русский

Если для каждого X с IsGalois действие G над F(X) пред-транситивно, то toAut F G сюръективен.

LaTeX

$$$\text{Surjective}(toAut\,F\,G)$$$

Lean4

instance (X : C) [IsConnected X] : MulAction.IsPretransitive G (F.obj X) :=
  isPretransitive_of_surjective F G (toAut_bijective F G).surjective X

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

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

Разделы

Аффилиация

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