English
For f ∈ End(F) and a pointed Galois object A, the map π applied to the end-equivalence yields compatibility with f on the fiber: F.map (AutGalois.π F A (endEquivAutGalois F f).unop).hom maps A.pt to f.app A A.pt.
Русский
Для f ∈ End(F) и помеченного Galois-объекта A отображение π, применяемое к соответствию эндоморфизмов, обеспечивает совместимость с f на фибре: F.map (AutGalois.π F A (endEquivAutGalois F f).unop).hom переходят A.pt к f.app A A.pt.
LaTeX
$$$F.map(AutGalois.\\pi F A (endEquivAutGalois F f).unop).hom(A.{\\rm pt}) = f.\\mathrm{app}(A,A.{\\rm pt})$$$
Lean4
theorem endEquivAutGalois_π (f : End F) (A : PointedGaloisObject F) :
F.map (AutGalois.π F A (endEquivAutGalois F f)).hom A.pt = f.app A A.pt :=
by
dsimp [endEquivAutGalois, AutGalois.π_apply]
change F.map ((((sectionsFunctor _).map (autIsoFibers F).inv) _).val A).hom A.pt = _
dsimp [autIsoFibers]
simp only [endEquivSectionsFibers_π]
erw [evaluationEquivOfIsGalois_symm_fiber]
