toAut_surjective_isGalois — Mathlib

English

For any t in Aut F and a Galois object X, there exists g in G such that g acts on every fiber as t does.

Русский

Для любого t ∈ Aut(F) и Galois-объекта X существует g ∈ G, так что g действует на каждой волокне так же, как t.

LaTeX

$$$\exists g\in G\;\forall X\,\forall x\in F(X),\; g\cdot x = t_X(x)$$$

Lean4

theorem toAut_surjective_isGalois (t : Aut F) (X : C) [IsGalois X] [MulAction.IsPretransitive G (F.obj X)] :
    ∃ (g : G), ∀ (x : F.obj X), g • x = t.hom.app X x :=
  by
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F X
  obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G a (t.hom.app X a)
  exact ⟨g, action_ext_of_isGalois F _ hg⟩

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