endMulEquivAutGalois_pi — Mathlib

English

For any endomorphism f and any pointed object A, applying the automorphism π to endMulEquivAutGalois(F,f) recovers the action f on the fiber, i.e., F.map (AutGalois.π F { obj := A, pt := a } (endMulEquivAutGalois F f).unop).hom a = f.app A a.

Русский

Для любого эндоморфизма f и любого помеченного объекта A, применение π к endMulEquivAutGalois(F,f) восстанавливает действие f на фибрe: F.map (AutGalois.π F { obj := A, pt := a } (endMulEquivAutGalois F f).unop).hom a = f.app A a.

LaTeX

$$$ F.map (AutGalois.\\pi F { obj := A, pt := a } (endMulEquivAutGalois F f).unop).hom a = f.app A a $$$

Lean4

theorem endMulEquivAutGalois_pi (f : End F) (A : PointedGaloisObject F) :
    F.map (AutGalois.π F A (endMulEquivAutGalois F f).unop).hom A.2 = f.app A A.pt :=
  endEquivAutGalois_π F f A

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