InnerAutomorphisms.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Inner automorphisms of nonabelian simple groups.

def OAI.SimpleInnerAutomorphisms.inner line 12
Source documentation
The subgroup of inner automorphisms.
```
def inner : Subgroup (MulAut T) := (MulAut.conj : T →* MulAut T).range
```
theorem OAI.SimpleInnerAutomorphisms.conjugate_conj line 15
Source documentation
Conjugation is natural under every automorphism.
```
theorem conjugate_conj (b : MulAut T) (t : T) :
    b * MulAut.conj t * b⁻¹ = MulAut.conj (b t) := by
…
```
theorem OAI.SimpleInnerAutomorphisms.inner_normal line 23
Source documentation
Inner automorphisms form a normal subgroup, for any group.
```
theorem inner_normal : (inner T).Normal := by
…
```
Mentions: OAI.SimpleInnerAutomorphisms.inner
theorem OAI.SimpleInnerAutomorphisms.conj_injective line 33
Source documentation
Noncommutativity rules out a total kernel of conjugation; simplicity forces its kernel to be trivial.
```
theorem conj_injective (hna : ∃ x y : T, x * y ≠ y * x) :
    Function.Injective (MulAut.conj : T →* MulAut T) := by
…
```
theorem OAI.SimpleInnerAutomorphisms.perfect_of_simple line 53
Source documentation
The derived subgroup is normal; simplicity and noncommutativity force it to be the whole group.
```
theorem perfect_of_simple (hna : ∃ x y : T, x * y ≠ y * x) :
    Group.IsPerfect T := by
…
```
def OAI.SimpleInnerAutomorphisms.innerEquiv line 63
Source documentation
A nonabelian simple group is canonically isomorphic to its inner automorphism group.
```
noncomputable def innerEquiv (hna : ∃ x y : T, x * y ≠ y * x) :
    T ≃* inner T := MonoidHom.ofInjective (conj_injective hna)
```
Mentions: OAI.SimpleInnerAutomorphisms.inner, OAI.SimpleInnerAutomorphisms.conj_injective
theorem OAI.SimpleInnerAutomorphisms.innerEquiv_apply line 67
Source documentation
The canonical isomorphism sends an element to conjugation by that element.
```
theorem innerEquiv_apply (hna : ∃ x y : T, x * y ≠ y * x) (t : T) :
    ((innerEquiv hna t : inner T) : MulAut T) = MulAut.conj t :=
…
```
Mentions: OAI.SimpleInnerAutomorphisms.innerEquiv, OAI.SimpleInnerAutomorphisms.inner
theorem OAI.SimpleInnerAutomorphisms.inner_perfect line 72
Source documentation
The inner automorphism group of a nonabelian simple group is perfect.
```
theorem inner_perfect (hna : ∃ x y : T, x * y ≠ y * x) :
    Group.IsPerfect (inner T) := by
…
```
Mentions: OAI.SimpleInnerAutomorphisms.inner