Stream: math-comp users

Topic: Semidirect Product


view this post on Zulip Raül (May 19 2023 at 17:54):

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!

view this post on Zulip Raül (May 20 2023 at 22:33):

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?

view this post on Zulip Pierre Roux (May 21 2023 at 06:40):

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.

view this post on Zulip Raül (May 21 2023 at 09:45):

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)

view this post on Zulip Raül (May 21 2023 at 10:00):

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.

view this post on Zulip Raül (May 21 2023 at 10:03):

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

view this post on Zulip Raül (May 21 2023 at 10:13):

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

view this post on Zulip Raül (May 21 2023 at 10:20):

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.

view this post on Zulip Raül (May 21 2023 at 11:32):

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?

view this post on Zulip Raül (May 21 2023 at 19:00):

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.

view this post on Zulip Cyril Cohen (May 21 2023 at 20:05):

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}.

view this post on Zulip Cyril Cohen (May 21 2023 at 20:18):

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

view this post on Zulip Cyril Cohen (May 21 2023 at 20:32):

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.

view this post on Zulip Raül (May 22 2023 at 18:19):

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