Is it there already a formalization of Outer Semidirect Product or at least Direct Product in math-comp?

Note that I want it to be a group of the cartesian product type.

Thx in advance!

As an update, I've put myself to it but I'm blocked already when trying to take a morphism from a group into the automorphism groups of some other (H -> Aut N), as Aut_group [set: N] gives me a (group_of {perm N}) instead of a FinGroup.type.

```
Variable C D : FinGroup.type.
Variable φ : morphism (Aut_group [set: C]) [set: D].
```

Is there any way of switching between them?

Do I have to do a separate type on perms with a proof of morphic and then give group structure?

I have close to no experience with fingroup so I'm unable to help. However, I think you should consider giving a working example, that will make it easier for eveyone to help you.

The previous code doesn't work , with error:

```
Error:
In environment
C, D : finGroupType
The term "[Aut [set: C]]%G" has type "{group perm_perm_type__canonical__fingroup_FinGroup C}"
while it is expected to have type "finGroupType".
```

All I'm trying to do is to write a morphism D -> Aut(C)

The problem si that all ways I find the group Aut C is as a predArgType and I don't understand why Coq doesn't let me use it as a Type:

For example, in the same context as before this doesn't work (similarly when using Aut_group):

```
Variable φ : D -> Aut [set: C].
```

Which fails with

```
Error: In environment
C, D : finGroupType
The term "Aut [set: C]" has type "{set perm_perm_type__canonical__fintype_Finite C}"
which should be Set, Prop or Type.
```

Is there any way of converting a group like these (usually noted A B C D in the code) into a group in finGroupType (usually noted aT rT in the code)?

https://math-comp.github.io/htmldoc//mathcomp.fingroup.morphism.html#8a399d885a5b51d8b3b3ad681df3eb79

If not it would be useful still to have a FinGroup.type of morphisms.

I don't see how I can't put a working example, as I can't even express the group type of morphisms between two groups.

So you can consider the question as this.

If it's somehow useful i can paste how did I formalise the group direct product, but it is not very interesting.

I'm doing a {perm T}-like type for automorphisms, following more or less the {perm T} in mathcomp (basically using allpairs instead to define a dmorphb).

Would it be interesting as an addition to the library?

Why is it that the following HB.instance for the isMulGroup.Build produces an error?

```
HB.instance Definition _ :=
isMulGroup.Build SemiDProd semiprod_mulP semiprod_oneP semiprod_invP.
```

I won't post the full code giving the precise lemmas and the other groups not to flood anymore the Zulip, but if its helpful I can send you my github repository.

Raül said:

As an update, I've put myself to it but I'm blocked already when trying to take a morphism from a group into the automorphism groups of some other (H -> Aut N), as Aut_group [set: N] gives me a (group_of {perm N}) instead of a FinGroup.type.

`From mathcomp Require Import all_fingroup Variable C D : finGroupType. Variable φ : morphism (Aut_group [set: C]) [set: D].`

Is there any way of switching between them?

Do I have to do a separate type on perms with a proof of morphic and then give group structure?

Here is a possible fix:

```
From mathcomp Require Import all_ssreflect all_fingroup.
Variable C D : finGroupType.
Variable φ : {morphism Aut [set: C] >-> D}.
```

I think `sdprod_by`

might be what you are looking for, isn't it?

Raül said:

Why is it that the following HB.instance for the isMulGroup.Build produces an error?

`HB.instance Definition _ := isMulGroup.Build SemiDProd semiprod_mulP semiprod_oneP semiprod_invP.`

I won't post the full code giving the precise lemmas and the other groups not to flood anymore the Zulip, but if its helpful I can send you my github repository.

To make this code work, you should replace

```
HB.instance Definition _ := isFinite.Build SemiDProd (@prod_enumP C D).
```

by

```
HB.instance Definition _ := Finite.on SemiDProd.
```

Indeed the former attempts to redeclare only the finiteness, while the latter copies the eqType, choiceType and countType structures from the type product `(C * D)%type`

to the alias `SemiDProd`

.

`sdprod_by`

was certainly what I was looking for, as it was expressed with action I didn't process it was it.

Thx!

Preceding code:

Is it there some type with only one element as a fingroup?

If not, why does the following:

produce this error?

```
Toplevel input, characters 14-95:
> .............
> HB.instance Definition _ := isMulGroup.Build True True_mulP True_oneP True_invP
Error:
Definition illtyped: The term "id_phant" has type "phantom Type True -> phantom Type True"
while it is expected to have type
"unify Type Type True ?t (is_not_canonically_a finType)".
```

I have manually added `isFinite`

, `hasChoice`

and `isCountable`

to it, as I don't understand `Finite.on`

and it doesn't work neither (if don't remember wrong Finite.on also failed in my previous question).

Last updated: Jul 23 2024 at 20:01 UTC