English
For any endomorphism f of F and any pointed Galois object A, the A-component of the corresponding section (endEquivSectionsFibers F f) equals the action of f on the fiber at A, i.e., (endEquivSectionsFibers F f).val A = f.app A A.pt.
Русский
Для любого концевого отображения f: F → F и любого помеченного Galois-объекта A компонент End-SectionsEquivalence равна действию f на ответвлении над A: (endEquivSectionsFibers F f).val A = f.app A A.pt.
LaTeX
$$$(endEquivSectionsFibers\,F\,f).val(A)=f.{\\rm app}(A,A.{\\rm pt}).$$$
Lean4
@[simp]
theorem endEquivSectionsFibers_π (f : End F) (A : PointedGaloisObject F) :
(endEquivSectionsFibers F f).val A = f.app A A.pt :=
by
dsimp [endEquivSectionsFibers, Types.sectionsEquiv]
erw [Types.limitEquivSections_apply]
simp only [colimitCoyonedaHomIsoLimit'_π_apply, incl_obj, comp_obj, FintypeCat.incl_obj, op_obj, FunctorToTypes.comp]
change
(((FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful FintypeCat.incl) C).homEquiv) f).app A
(((colimit.ι _ _) ≫ (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).hom).app A _) =
f.app A A.pt
simp
rfl
