8.2. The conjugation action🔗

To write different actions, we use type synonyms. The type ConjAct G is a type synonym for G; a term of type ConjAct G contains exactly the same data as a term of type G, and can be converted to G using the function ConjAct.ofConjAct.

This allows us to have elements of ConjAct G act on G by conjugation.

open ConjAct in
example {G} [Group G] (g : ConjAct G) (s : G) :
    g • s = ofConjAct g * s * (ofConjAct g)⁻¹ :=
  smul_def g s

Often it is more convenient to work directly with the conjugation automorphism of G instead of using a type synonym.

For this we have the homomorphism MulAut.conj from G to its automorphism group MulAut G.

example {G} [Group G] (g : G) (s : G) :
    MulAut.conj g s = g * s * g⁻¹ :=
  MulAut.conj_apply g s