instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois

Mathlib.CategoryTheory.Galois.Action

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

English

If X is an IsGalois object, the action of Aut X on the fiber is pretransitive.

Русский

Если X является объектом IsGalois, действие Aut X на волокне предперено.

LaTeX

$$$\\forall X\\,[IsGalois X] \\Rightarrow MulAction.IsPretransitive(Aut X, ((functorToAction F).obj X).V)$$$

Lean4

instance (X : C) [IsGalois X] : MulAction.IsPretransitive (Aut X) ((functorToAction F).obj X).V :=
  isPretransitive_of_isGalois F X

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

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

Разделы

Аффилиация

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