isGalois_iff_pretransitive — Mathlib

English

Let X be a connected object. Then X is Galois if and only if the natural action of Aut X on F.obj X is pretransitive.

Русский

Пусть X связный. Тогда X есть галуа-объект тогда и только тогда, когда естественное действие Aut X на F.obj X является предтранситивным.

LaTeX

$$$\\mathrm{IsGalois}(X) \\iff \\mathrm{MulAction.IsPretransitive}(\\mathrm{Aut}\,X, F.obj X).$$$

Lean4

/-- Given a fiber functor `F` and a connected object `X` of `C`. Then `X` is Galois if and only if
the natural action of `Aut X` on `F.obj X` is transitive. -/
theorem isGalois_iff_pretransitive (X : C) [IsConnected X] : IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X) :=
  by
  rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]
  exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

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