Holomorph of a group

Stream: maths

[Seewoo Lee]

For a group $G$, the holomorph $\mathrm{Hol}(G)$ is simply defined as the semidirect product $G \rtimes \mathrm{Aut}(G)$. I recently saw the definition from Dummit--Foote and realized that it does not exist in mathlib yet. It is fairly easy to formalize the definition (since we already have semidirect product) but not sure if it worths to add assuming I don't have any nice theorems / applications using it. (Dummit--Foote include some computations for small $G$.) What's usual practice in such case?

[Kenny Lau]

@Seewoo Lee I don't speak for mathlib, but I think usually mathlib wouldn't include it in this case.

[Ruben Van de Velde]

I guess it depends - I don't think you need Big Results:trademark:, but you'd be expected to have at least some basic lemmas about the definition so you can actually use it

[Seewoo Lee]

I see, probably I will think of some basic facts (things on wikipedia or textbooks). There are some big(?) theorems using it but haven’t looked in details.

[Yury G. Kudryashov]

At least, we can introduce it as an abbrev so that loogle can find it.

[Kenny Lau]

is that how loogle works?

[Scott Carnahan]

A basic fact you could try formalizing is that, as a subgroup of Perm(G), the holomorph is equal to the normalizer of the left regular subgroup.

[Kenny Lau]

how do you embed it into Perm(G)?

[Scott Carnahan]

G acts by left multiplication, and Aut(G) acts by automorphisms.

[Kenny Lau]

I think this map already should be in mathlib (cc @Seewoo Lee)