toAut_bijective — Mathlib

English

Equality of two automorphisms in AutGalois F is determined by their projections to Aut(A) for each pointed Galois object A.

Русский

Сравнение двух автоморфизмов в AutGalois F определяется по их проекциям в Aut(A) для каждого точечного Galois-объекта A.

LaTeX

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

Lean4

theorem toAut_bijective : Function.Bijective (toAut F G)
    where
  left := toAut_injective_of_non_trivial F G IsFundamentalGroup.non_trivial'
  right := toAut_surjective_of_isPretransitive F G IsFundamentalGroup.transitive_of_isGalois

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