evaluation_aut_surjective_of_isGalois

English

Let A be Galois and a ∈ F.obj A. The map Aut A → F.obj A, sending f to F.map f.hom a, is surjective.

Русский

Пусть A галуа; для a ∈ F.obj A отображение Aut A → F.obj A, f ↦ F.map f.hom a, является сюръективным.

LaTeX

$$$\\mathrm{Surjective}\\bigl(\\mathrm{Aut}\,A \\to F.obj A,\\ f \\mapsto F.map f.hom a\\bigr).$$$

Lean4

theorem evaluation_aut_surjective_of_isGalois (A : C) [IsGalois A] (a : F.obj A) :
    Function.Surjective (fun f : Aut A ↦ F.map f.hom a) :=
  MulAction.IsPretransitive.exists_smul_eq a

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