English
The automorphism group of a root pairing is the same as the group of automorphisms of the underlying RootPairing structure.
Русский
Группа автоморфизмов корневого парирования совпадает с группой автоморфизмов самой структуры RootPairing.
LaTeX
$$$\\\\mathrm{Aut}(P) = \\\\mathrm{RootPairing.Equiv}(P,P).$$$
Lean4
theorem coweightHom_injective (P : RootPairing ι R M N) : Injective (Equiv.coweightHom P) :=
by
refine Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_
have h : (MulOpposite.unop (coweightHom P g)).toLinearMap = (MulOpposite.unop (coweightHom P g')).toLinearMap := by
simp_all
rw [coweightHom_toLinearMap, coweightHom_toLinearMap] at h
suffices h' : g.toHom = g'.toHom by exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')
apply Hom.coweightHom_injective P
exact MulOpposite.unop_inj.mp h
