evaluation_aut_bijective_of_isGalois

English

Let A be Galois and a ∈ F.obj A. The evaluation map Aut A → F.obj A is bijective.

Русский

Пусть A галуа; отображение оценки Aut A → F.obj A является биекцией.

LaTeX

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

Lean4

theorem evaluation_aut_bijective_of_isGalois (A : C) [IsGalois A] (a : F.obj A) :
    Function.Bijective (fun f : Aut A ↦ F.map f.hom a) :=
  ⟨evaluation_aut_injective_of_isConnected F A a, evaluation_aut_surjective_of_isGalois F A a⟩

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