Zulip Chat Archive

Stream: maths

Topic: product families of groups


Antoine Chambert-Loir (Sep 19 2022 at 14:15):

There is an instance to say that a product family groups is a group, but I couldn't find functions
that create group morphisms from that group to other groups, such as :

def prod.commprod_map {ι : Type*} [fintype ι] (G : ι  Type*) [Π (i : ι), group (G i)]
  {H : Type*} [comm_group H] (φ : Π (i : ι), (G i →* H)) :
  (Π (i : ι), G i) →* H := {
to_fun    := λ g, finset.prod (finset.univ) (λ (i : ι), (φ i) (g i)),
map_one'  := by simp only [pi.one_apply, map_one, finset.prod_const_one],
map_mul'  := λ g h, begin simp only [pi.mul_apply, map_mul, finset.prod_mul_distrib], end, }

def prod.noncomm_prod_map {ι : Type*} [fintype ι] {G : ι  Type*} [Π (i : ι), group (G i)]
  {H : Type*} [group H] (φ : Π (i : ι), (G i →* H))
  ( :  (g : Π i, G i) (i j : ι), commute ((φ i) (g i)) ((φ j) (g j)))
  (hφ' :  (g h : Π i, G i) (i j : ι) (hij : i  j), commute ((φ i) (h i)) ((φ j) (g j))):
  (Π (i : ι), G i) →* H := {
to_fun    := λ g, finset.noncomm_prod (finset.univ) (λ (i : ι), (φ i) (g i)) (λ i hi j hj,  g i j),
map_one'  := begin
  simp only [pi.one_apply, map_one],
  rw finset.noncomm_prod_eq_pow_card,
  exact one_pow _,
  { intros x _, refl, },
  end,
map_mul'  := λ g h,
begin
  rw  finset.noncomm_prod_mul_distrib (λ (i : ι), (φ i) (g i)) (λ (i : ι), (φ i) (h i)) _ _ _,
  simp only [pi.mul_apply, map_mul],
  intros i _ j _ hij,
  exact hφ' g h i j hij,
end, }

Should I have looked better? Should I make a PR (with some other similar functions) ?
(is the universal property already somewhere ?)

Jireh Loreaux (Sep 19 2022 at 14:23):

I think the name would involve pi, not prod if we had it. I looked in algebra/group/pi, which is where I would expect it to be, but it doesn't seem to be there. So, as far as I can tell, we don't have it, but perhaps someone who knows the algebra part of the library better will correct me.

Riccardo Brasca (Sep 19 2022 at 14:25):

Is docs#pi.eval_monoid_hom what you are looking for?

Jireh Loreaux (Sep 19 2022 at 14:26):

That's not into a different group, that's just projection onto one of the factors.

Riccardo Brasca (Sep 19 2022 at 14:27):

Ah, sure

Adam Topaz (Sep 19 2022 at 14:28):

I suppose one should use the direct sum in this case, and not the product. We probably have the isomorphism between the two in the finite case

Riccardo Brasca (Sep 19 2022 at 14:28):

OMG, it's in the wrong direction!

Adam Topaz (Sep 19 2022 at 14:28):

But of course that wouldn't take care of the noncommutative case

Riccardo Brasca (Sep 19 2022 at 14:33):

Ah, docs#monoid_hom.noncomm_pi_coprod

Riccardo Brasca (Sep 19 2022 at 14:33):

But it would be nice to have it directly for a comm_group codomain

Antoine Chambert-Loir (Sep 19 2022 at 14:52):

Cool ! I'll add that.

Junyan Xu (Sep 19 2022 at 15:07):

This was suggested by me and and added by Joachim Breitner in #11744 in March as part of his work on the characterization of finite nilpotent groups. Since you're working on finite groups, you might want to look into the tracking issue #11723 to see if you missed something else ...

I also suggested a generalization to the infinite case, but I only thought about a subgroup of pi or a quotient of free_product, not docs#dfinsupp or docs#direct_sum (which don't seem to be intended for multiplicative groups since the latter requires add_comm_monoid and the former only admits the instance docs#dfinsupp.add_group but not dfinsupp.group).


Last updated: Dec 20 2023 at 11:08 UTC