product families of groups

Stream: maths

[Antoine Chambert-Loir]

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))
  (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, hφ 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]

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]

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

[Jireh Loreaux]

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

[Riccardo Brasca]

Ah, sure

[Adam Topaz]

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]

OMG, it's in the wrong direction!

[Adam Topaz]

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

[Riccardo Brasca]

Ah, docs#monoid_hom.noncomm_pi_coprod

[Riccardo Brasca]

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

[Antoine Chambert-Loir]

Cool ! I'll add that.

[Junyan Xu]

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