autIsoFibers_inv_app — Mathlib

English

There is a canonical equivalence between the endomorphism monoid End(F) and the automorphism group AutGalois(F) that encodes how endomorphisms correspond to Galois automorphisms of the fiber functor.

Русский

Существует каноническое эквивалентность моноида End(F) и группы автоморфизмов AutGalois(F), описывающее соответствие эндоморфизмов автоморфизмам волокной функции F.

LaTeX

$$$\\operatorname{End}(F) \\simeq \\operatorname{AutGalois}(F)$$$

Lean4

theorem autIsoFibers_inv_app (A : PointedGaloisObject F) (b : F.obj A) :
    (autIsoFibers F).inv.app A b = (evaluationEquivOfIsGalois F A A.pt).symm b :=
  rfl

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