mul_aut and mul_hom

Stream: new members

[Antoine Chambert-Loir]

From what I understand, in a group G, one has a homomorphism mul_aut.conj : G →* mul_aut G.
But, when g : G, I apparently can't use mul_aut.conj g as an automorphism of the group G,
because mul_aut does not contain the property that the morphism respects 1.
Since docs#sylow manages to use mul_aut.conj, I presumably have something wrong, but what?

[Kevin Buzzard]

It's an automorphism of a group which preserves * so it automatically preserves 1

[Kevin Buzzard]

import data.equiv.mul_add_aut

example (G : Type) [group G] (g : G) : mul_aut.conj g 1 = 1 := by simp

I'm not entirely sure what your question is.

[Antoine Chambert-Loir]

Well, the following

example (α : Type*) (g : perm α) (s : set α) : Prop :=
begin
  let this := monoid_hom.map_closure (mul_aut.conj g) s,

  sorry,
end

generates the following error, which I don't understand :

type mismatch at application
  monoid_hom.map_closure (⇑mul_aut.conj g)
term
  ⇑mul_aut.conj g
has type
  mul_aut (perm α) : Type u_1
but is expected to have type
  ?m_1 →* ?m_2 : Type (max ? ?)

[Kevin Buzzard]

Can you post fully working code? I don't know what to import/open

[Kevin Buzzard]

Maybe you just need to coerce it?

[Kevin Buzzard]

An automorphism is not equal to a homomorphism

[Thomas Browning]

You can try (mul_aut.conj g).to_monoid_hom. The main issue though, is that mul_aut.conj g is an automorphism of equiv.perm α, so monoid_hom.map_closure will want a subset of equiv.perm α, as opposed to a subset of α.

[Antoine Chambert-Loir]

Sorry for providing a minimal non-working example… The to_monoid_hom did the job,
that was that, thank you. As a matter of fact, I couldn't find again how to do the coercion, although I had already used it once…