English
For f ∈ End(F) and A with an element a in F(A), the π-map through endMulEquivAutGalois(F,f) sends a to the fiber action f.hom.app A a.
Русский
Для f ∈ End(F) и a ∈ F(A) отображение π через endMulEquivAutGalois(F,f) отправляет a в действие f.hom на A.
LaTeX
$$$ F.map (AutGalois.π F { obj := A, pt := a } (endMulEquivAutGalois F f).unop).hom a = f.hom.app A a $$$
Lean4
/-- The automorphism group of `F` is multiplicatively isomorphic to
(the multiplicative opposite of) the limit over the automorphism groups of
the Galois objects. -/
noncomputable def autMulEquivAutGalois : Aut F ≃* (AutGalois F)ᵐᵒᵖ
where
toFun := MonoidHom.comp (endMulEquivAutGalois F) (Aut.toEnd F)
invFun t := asIso ((endMulEquivAutGalois F).symm t)
left_inv
t := by
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, MulEquiv.symm_apply_apply]
exact Aut.ext rfl
right_inv
t := by
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, Aut.toEnd_apply]
exact (MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl
map_mul' := by simp [map_mul]
