commutator of products

Stream: maths

[Joachim Breitner]

I am struggling with a proof for

 ⁅H₁.prod H₂, K₁.prod K₂⁆ = ⁅H₁, K₁⁆.prod ⁅H₂, K₂⁆

(which I hope is true) that doesn’t end up with a horribly involved double induction on the closure that’s in the definitions of the general commutator. Is there no simple argument? ( ≤ is the easy direction.)

[Joachim Breitner]

Maybe a helpful step would be a nice lemma that shows H.prod K ≤ J from assumptions of he form H ≤ … and K ≤ … , but I have no good idea yet.

[Joachim Breitner]

Hmm, maybe it makes sense to start with

  (closure S1).prod (closure S2) = closure (S1 ×ˢ {1} \union {1} ×ˢ S2) :=

But that, too, needs ugly double induction.

[Reid Barton]

I think this is the right general idea

[Adam Topaz]

You can prove that the abelianization commutes with products, and use the fact that the commutator subgroup is the kernel of the abelianization.

[Adam Topaz]

Oh wait, I don't actually know what those symbols mean

[Adam Topaz]

Ignore me.

[Reid Barton]

I think this should boil down to the fact that H.prod K is the subgroup generated by elements of the form (h, 1) and (1, k)

[Reid Barton]

(whoops, pretend I wrote H₁.prod H₂ is ...)

[Joachim Breitner]

Ah, indeed, if I start with

H.prod K = closure (H ×ˢ {1} \union {1} ×ˢ K)

I avoid juggling with so many closures.

And then ⁅H₁, K₁⁆.prod ⁅H₂, K₂⁆ ≤ ⁅H₁.prod H₂, K₁.prod K₂⁆ suddenly has a closure on the left, and that’s easier.

Hmm, in the end that would be as useful as the following lemma, which would avoid talking about closure explicitly.

le_prod_iff : H.prod K ≤ J \iff (H.prod \bot ≤ J \and \bot.prod K  ≤ J)

Worth exploring, although I am not 100% sure yet that it will help in the end, and how easily this idea generalizes to Pi subgroups. Anyways, I’ll leave that for tomorrow .

[Reid Barton]

It seems to me that it doesn't, unless you use the "direct sum" (not product) of subgroups.

[Joachim Breitner]

It might actually, if I rephrase H.prod \bot as map (λ x, (x,1)) H. Then I’d be faced with

map … ⁅H₁, K₁⁆ ≤ ⁅H₁.prod H₂, K₁.prod K₂⁆

then I can apply subgroup.comap_map_eq_self_of_injective to have ⁅H₁, K₁⁆ ≤ … and then it’s just a simple calculation.
And this actually has a chance to generalize to Pi-types.
Hopefully I won’t find a flaw in this plan before I go to bed :-)