Stream: math-comp users

Topic: Semidirect Product

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!

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?

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.

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)

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.

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

Raül (May 21 2023 at 10:13):

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

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.

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?

Raül (May 21 2023 at 19:00):

Open Scope group_scope.
Variable C D : FinGroup.type.

Variable φ : Mor D (Aut C).

Definition SemiDProd : Type := (C * D)%type.
HB.instance Definition _ := isFinite.Build SemiDProd (@prod_enumP C D).

Definition semiprod_mul (s t : SemiDProd) :=
  let: (x, y) := s in let: (u, v) := t in
  (x * (φ y u), y * v).
Definition semiprod_one : SemiDProd := (1 : C, 1 : D).
Definition semiprod_inv (s : SemiDProd) :=
  let: (x, y) := s in
  ((φ y^-1 x^-1), y^-1).

Lemma semiprod_oneP : left_id semiprod_one semiprod_mul.
Proof.
  by case => /= a b; rewrite !mul1g mor1 autE.
Qed.

Lemma semiprod_invP : left_inverse  semiprod_one semiprod_inv semiprod_mul.
Proof.
  case => /= a b.
  by rewrite -(aut_morph (φ b^-1)) !mulVg autg1.
Qed.

Lemma semiprod_mulP : associative semiprod_mul.
Proof.
  case => a b; case => c d; case => e f /=.
  by rewrite !mulgA !(morph_morph φ) autE /= (aut_morph (φ b)) mulgA !avalE.
Qed.

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.

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

Cyril Cohen (May 21 2023 at 20:18):

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

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?

Open Scope group_scope.
Variable C D : FinGroup.type.

Variable φ : Mor D (Aut C).

Definition SemiDProd : Type := (C * D)%type.
HB.instance Definition _ := isFinite.Build SemiDProd (@prod_enumP C D).

Definition semiprod_mul (s t : SemiDProd) :=
  let: (x, y) := s in let: (u, v) := t in
  (x * (φ y u), y * v).
Definition semiprod_one : SemiDProd := (1 : C, 1 : D).
Definition semiprod_inv (s : SemiDProd) :=
  let: (x, y) := s in
  ((φ y^-1 x^-1), y^-1).

Lemma semiprod_oneP : left_id semiprod_one semiprod_mul.
Proof.
  by case => /= a b; rewrite !mul1g mor1 autE.
Qed.

Lemma semiprod_invP : left_inverse  semiprod_one semiprod_inv semiprod_mul.
Proof.
  case => /= a b.
  by rewrite -(aut_morph (φ b^-1)) !mulVg autg1.
Qed.

Lemma semiprod_mulP : associative semiprod_mul.
Proof.
  case => a b; case => c d; case => e f /=.
  by rewrite !mulgA !(morph_morph φ) autE /= (aut_morph (φ b)) mulgA !avalE.
Qed.

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.

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!

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

Definition True_mul (x y : True) : True := y.
Definition True_one : True := I.
Definition True_inv (x : True) : True := x.

Lemma True_mulP : associative True_mul.
Proof. by[]. Qed.
Lemma True_oneP : left_id True_one True_mul.
Proof. by[]. Qed.
Lemma True_invP : left_inverse True_one True_inv True_mul.
Proof. by case. Qed.

HB.instance Definition _ :=  isMulGroup.Build True True_mulP True_oneP True_invP.

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: Oct 13 2024 at 01:02 UTC