endEquivAutGalois — Mathlib

English

The End-to-AutGalois equivalence is a monoid isomorphism when viewed as a map between End(F) and AutGalois(F) with the opposite multiplication.

Русский

Эквиваленция End(F) и AutGalois(F) является моидным гомоморфизмом, если рассматривать AutGalois(F) с противоположным умножением.

LaTeX

$$$ End(F) \\cong_{\\text{Mul}} (AutGalois(F))^{\\mathrm{op}} $$$

Lean4

/-- The equivalence between endomorphisms of `F` and the limit over the automorphism groups
of all Galois objects. -/
noncomputable def endEquivAutGalois : End F ≃ AutGalois F :=
  let e1 := endEquivSectionsFibers F
  let e2 := ((Functor.sectionsFunctor _).mapIso (autIsoFibers F).symm).toEquiv
  e1.trans e2

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