π — Mathlib · SciLib

English

For each pointed Galois object A, the projection π F A is surjective.

Русский

Для каждого точечного Galois-объекта A проекция π F A сюръективна.

LaTeX

$$$\forall A:\; AutGalois F \to Aut(A) \text{ is surjective}$$$

Lean4

/-- The canonical projection from `AutGalois F` to the `C`-automorphism group of each
pointed Galois object. -/
noncomputable def π (A : PointedGaloisObject F) : AutGalois F →* Aut (A : C) :=
  GrpCat.sectionsπMonoidHom (autGaloisSystem F) A

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