Inner and Outer Automorphism Groups

Stream: new members

[Alex Griffin]

I am currently trying to define the inner and outer automorphism groups of a given group G and have run into some issues. I have included the relevant code below (in a dropdown for length reasons):

Code for Inner and Outer Automorphisms

import data.equiv.mul_add_aut
import group_theory.subgroup
import group_theory.quotient_group

/-
The definition of the inner and outer automorphism groups of a group G
-/

universe u

namespace inner_aut

/-- The inner automorphism group of a group G -/
def inner_aut {G : Type u} [group G] : subgroup (mul_aut G) :=
{
carrier := {φ | ∃ (c : G), ∀ (g : G), φ g = c * g * c⁻¹},
one_mem' := sorry,
mul_mem' := sorry,
inv_mem' := sorry,
}

/-- A proof that the inner automorphism group is normal in Aut(G) -/
lemma inner_normal {G : Type u} [group G] : (inner_aut G).normal :=
begin
sorry,
end,

/-- The outer automorphism group of a group G -/
def outer_aut {G : Type u} [group G] : quotient (inner_aut G) :=
begin
sorry,
end,

end inner_aut

The first, more immediate issue is that, even filling in the gaps with sorry I still get errors related to some of the definitions, specifically related to the statement that inner_aut G is normal in mul_aut G and the definition of outer_aut as a quotient. For the inner automorphism group, the Infoview claims that Lean expects a function, which baffles me. The specific error it gives is

function expected at
  inner_aut
term has type
  subgroup (mul_aut ?m_1)

I assume that, if this error is fixed, then at least some of what else is giving errors will go away, but I wouldn't be surprised if, in fact, there are still issues with what I have.

The second issue is that, even with these errors fixed, I am not quite sure how to proceed with providing the necessary proofs for the definition of the inner automorphism group. Perhaps someone would be willing to provide some pointers on how to proceed? This would be much appreciated.

[Patrick Massot]

Your inner_aut doesn't take any explicit argument.

[Patrick Massot]

This is clearly not what you want.

[Patrick Massot]

So switch to def inner_aut (G : Type u) [group G] :

[Patrick Massot]

Note also there is no reason to handle universe variables by hand here. You should use (G : Type*)

[Patrick Massot]

You also have trailing commas after end which will confuse Lean. And quotient is not what you think until you open the quotient_group namespace (or use the full name quotient_group.quotient.

[Patrick Massot]

And the last declaration is declaring you will define outer_aut as an element of the quotient of the automorphism group of an implicitly specified G by its inner automorphism group. This is not what you want.

[Patrick Massot]

Also, defining the inner automorphisms like this will give you a lot of extra work compared to defining it as the image of the group morphism sending an element to the corresponding automorphism. In particular you'll need to prove it is a subgroup instead of getting it for free.

[Patrick Massot]

def inner_aut (G : Type u) [group G] : subgroup (mul_aut G) := subgroup.map mul_aut.conj ⊤

[Patrick Massot]

Note I haven't checked if this definition is already in mathlib.

[Eric Wieser]

I think that's just mul_aut.conj.range