autMulEquivAutGalois_π — Mathlib

English

For x ∈ Aut F, A any object, and a ∈ F(A), the symmetric inverse of autMulEquivAutGalois maps to the fiber via F.map and π, yielding equality with the action x.hom.app A a.

Русский

Для x ∈ Aut F, произвольного A и a ∈ F(A) симметрическая обратная операция autMulEquivAutGalois возвращает через F.map и π соответствие с действием x.hom.app A a.

LaTeX

$$$ ((autMulEquivAutGalois F).symm \\langle x \\rangle).hom.app A a = F.map (AutGalois.\\pi F \\langle A, a, \\text{...} \\rangle x).hom a $$$

Lean4

theorem autMulEquivAutGalois_π (f : Aut F) (A : C) [IsGalois A] (a : F.obj A) :
    F.map (AutGalois.π F { obj := A, pt := a } (autMulEquivAutGalois F f).unop).hom a = f.hom.app A a :=
  by
  dsimp [autMulEquivAutGalois, endMulEquivAutGalois]
  rw [endEquivAutGalois_π]
  rfl

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