autGaloisSystem_map_surjective — Mathlib

English

Equality of AutGalois automorphisms is determined by their π-projections on all pointed Galois objects.

Русский

Равенство автоморфизмов AutGalois определяется их π-проекциями на всех точечных Galois-объектах.

LaTeX

$$$\forall f,g:\ AutGalois F, (\forall A, AutGalois.\pi F A f = AutGalois.\pi F A g) \Rightarrow f=g$$$

Lean4

theorem autGaloisSystem_map_surjective ⦃A B : PointedGaloisObject F⦄ (f : A ⟶ B) :
    Function.Surjective ((autGaloisSystem F).map f) :=
  by
  intro (φ : Aut B.obj)
  obtain ⟨ψ, hψ⟩ := autMap_surjective_of_isGalois f.val φ
  use ψ
  simp only [autGaloisSystem_map]
  exact hψ

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