isPretransitive_of_isGalois — Mathlib

English

If X is a Galois object of the category, then the action of Aut F on the fiber F(X) is pretransitive: for any x,y in F(X) there exists an automorphism of F sending x to y.

Русский

Если X — Галоc-объект, то действие Aut F на волокне F(X) является прeтранситивным: для любых x,y ∈ F(X) существует автоморфизм F, переводящий x в y.

LaTeX

$$MulAction.IsPretransitive (Aut F) (F.obj X)$$

Lean4

/-- The `Aut F` action on the fiber of a Galois object is transitive. See
`pretransitive_of_isConnected` for the same result for connected objects. -/
theorem isPretransitive_of_isGalois (X : C) [IsGalois X] : MulAction.IsPretransitive (Aut F) (F.obj X) :=
  by
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y
  obtain ⟨a, ha⟩ := AutGalois.π_surjective F ⟨X, x, inferInstance⟩ φ
  use (autMulEquivAutGalois F).symm ⟨a⟩
  simpa [mulAction_def, ha]

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