direct product of sylow groups

Stream: maths

[Joachim Breitner]

The next step in my quest to provide the equivalent definitions for finite nilpotent groups I have to show that if every sylow group is normal, then the group is the direct product of its sylow groups.
I am unsure what would be the best way to phrase the latter statement. Do we have “group is the direct product of $n$ of its subgroups” somewhere? Should I go via $G$ isomorphic to the external product of the sylow subgroups, or rather some notion of internal n-ary product?

[Johan Commelin]

Probably something like

def foobar : G ≃* Π (p : nat.primes) (H : sylow p G), H := sorry

[Joachim Breitner]

Oh, is this using the fact that those primes that don't divide the group order have trivial Sylow group? Clever, thanks!

[Joachim Breitner]

Hmm, but it does seem to assume that there is exactly one Sylow group for each prime (else that product contains conjugate copies). Which I know in the one implication, but not the other. So maybe I should fix a function P : Pi (p : nat.primes) , Sylow p G and use that selection of Sylow groups.

OTOH, if that equivalency holds, it follows thst each Sylow group exists only once in it, based on a group order argument.

I'll play around with what works best.

[Reid Barton]

Don't we have some kind of internal direct products?

[Joachim Breitner]

There is the subgroup lattice’s ⊔, e.g. as used in Frattini’s argument. That’s a product? But not necessarily a direct product.

[Johan Commelin]

Right, you would need a separate lemma saying that the product is direct.

[Joachim Breitner]

For the binary product, that’s “just” that the ⊓ is trivial. But for the n-ary internal direct product, that’s a bit more hairy to express, isn't it?

[Johan Commelin]

Yep, I think so.

[Joachim Breitner]

So the best course of action is to create a new definition for the internal product (in its own file?), with various helper lemmas as desired, maybe even the equivalence with the external product definition, and then use that in the Sylow development.

[Johan Commelin]

That might very well be the smoothest way forward.

[Eric Wieser]

Is the direct product distinct from the docs#free_product?

[Damiano Testa]

I think so: the direct product of $\mathbb{Z}$ with itself is commutative, while the free product is not.

[Damiano Testa]

In the direct product, the operation happens componentwise, while the free product is essentially only concatenation of symbols from each factor.

[Joachim Breitner]

I am starting with this definition:

structure direct_factors (S : set (subgroup G)) : Prop :=
  (elements_commute : ∀ H₁ ∈ S, ∀ H₂ ∈ S, H₁ ≠ H₂ → ∀ x ∈ H₁, ∀ y ∈ H₂, x * y = y * x)
  (triv_intersection: ∀ H₁ ∈ S, H₁ ⊓ Sup (S \ {H₁}) = ⊥)

I am _not_ requiring that Sup S is the whole group here, so this is “these groups are the direct factors of their product”. Not sure if this is helpful or not.

The main theorem would be something like

theorem external_of_internal_direct_product (S : finset (subgroup G))
  (hi : direct_factors (S : set (subgroup G))) :
  (∏ H in S, H) ≃ (Sup S : subgroup G) :=

but these n-ary products are only defined for comm_monoid, it seems.

Am I missing something or do we not have the n-ary product of groups somewhere?

[Reid Barton]

It would probably be better to use an indexed family (indexed by some other type) rather than a set. Then the product is just a Pi type. I'm not even sure what ∏ H in S, H is.

[Reid Barton]

compare https://leanprover-community.github.io/mathlib_docs/linear_algebra/linear_independent.html

[Joachim Breitner]

It’s defined in https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html: There products are defined over types and over sets.
But in either case it’s comm_monoids, which is where I think I am stuck here.
Or is there another definitions elsewhere for n-ary products of groups?

[Joachim Breitner]

Ah, I think I get what you are saying: Lean’s fundamental Pi type has group instance somewhere?

[Joachim Breitner]

Indeed,

theorem external_of_internal_direct_product (S : finset (subgroup G))
  (hi : direct_factors (S : set (subgroup G))) :
  (Π (x : S), x) ≃ (Sup S : subgroup G) :=

typechecks. Thanks :-)

[Reid Barton]

Right

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/algebra/group/pi.html

[Joachim Breitner]

Heh, I looked at that fine, but didn’t get it. Thanks for the nudge.

[Reid Barton]

Before I think you were using the fact that subgroup G has a * operation, and then implicitly coercing to a type at the end