English
The same endomorphism–automorphismGalois equivalence is compatible with composition, i.e., the map respects multiplication of endomorphisms via AutGalois components.
Русский
Та же эквивалентность эндоморфизмов и автоморфизмов Гало совместима с композициями, то есть сохраняет умножение.
LaTeX
$$$ (endEquivAutGalois F)(g\\circ f) = (endEquivAutGalois F)(g) \\circ (endEquivAutGalois F)(f) $$$
Lean4
@[simp]
theorem endEquivAutGalois_mul (f g : End F) :
(endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F g) * (endEquivAutGalois F f) :=
by
refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)
simp only [map_mul, endEquivAutGalois_π, Aut.Aut_mul_def, NatTrans.comp_app, Iso.trans_hom]
simp only [map_comp, FintypeCat.comp_apply, endEquivAutGalois_π]
change f.app A (g.app A A.pt) = (f.app A ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt
rw [← f.naturality, FintypeCat.comp_apply, endEquivAutGalois_π]
