π_surjective — Mathlib

English

For connected X, the action of G on F(X) is pretransitive.

Русский

Для связаного X действие G на F(X) всегда предтранситивно.

LaTeX

$$$\forall X\ [IsConnected X]:\ MulAction.IsPretransitive G (F.obj X).carrier$$$

Lean4

/-- `autGalois.π` is surjective for every pointed Galois object. -/
theorem π_surjective (A : PointedGaloisObject F) : Function.Surjective (AutGalois.π F A) := fun (σ : Aut A.obj) ↦
  by
  have (i : PointedGaloisObject F) : Finite ((autGaloisSystem F ⋙ forget _).obj i) :=
    inferInstanceAs <| Finite (Aut (i.obj))
  exact eval_section_surjective_of_surjective (autGaloisSystem F ⋙ forget _) (autGaloisSystem_map_surjective F) A σ

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