autMap_surjective_of_isGalois — Mathlib

English

If A and B are Galois, autMap f is surjective for f: A ⟶ B.

Русский

Если A и B галуа, то autMap f сюръективен для f: A ⟶ B.

LaTeX

$$$\mathrm{Surjective}(\operatorname{autMap} f)$$$

Lean4

/-- `autMap` is surjective, if the source is also Galois. -/
theorem autMap_surjective_of_isGalois {A B : C} [IsGalois A] [IsGalois B] (f : A ⟶ B) :
    Function.Surjective (autMap f) := by
  intro σ
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f a))
  obtain ⟨τ, (hτ : F.map τ.hom a = a')⟩ := MulAction.exists_smul_eq (Aut A) a a'
  use τ
  apply evaluation_aut_injective_of_isConnected F B (F.map f a)
  simp [hτ, ha']

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