cosets / Second isomorphism theorem

Stream: Is there code for X?

[Kevin Buzzard]

To develop the theory of Hecke operators for FLT I need what I was taught was the second isomorphism theorem, but to my surprise I've discovered that mathlib's statement of the theorem docs#QuotientGroup.quotientInfEquivProdNormalQuotient was strictly weaker than what I was taught as an undergraduate.

Let $G$ be a group and let $H$ and $K$ be subgroups, with no normality assumption on either (this is why my claim below is different to mathlib's). By $H/(H\cap K)$ I mean the set of left cosets $h(H\cap K)$ and by $HK$ I mean the set of products $\{hk:h\in H,k\in K\}$ (note that this is not a group in general, if neither $H$ nor $K$ are normal). This set is easily checked to be a union of left cosets $hK$ of $K$; by $HK/K$ I mean the set of these left cosets. I was taught that the second isomorphism theorem was the canonical bijection $H/(H\cap K)\cong HK/K$ sending $h(H\cap K)$ to $hK$. And then the rider is that if $K$ happens to be normal then $HK$ is a subgroup and both the things I'm quotienting out by are normal subgroups and the canonical map unsurprisingly preserves multiplication (which is the statement we have in mathlib).

I realised that I didn't even know how to state the version I need. We have $HK$ of type Set G as (H : Set G) * (K : Set G) after open scoped Pointwise, but do we even have $HK/K$ in any form? The \/ symbol only works for groups and in my application $HK$ will definitely not be closed under multiplication.

---

The application is this. Again let $H$ and $K$ be subgroups of a (infinite, in my case) group $G$ (neither of them normal in the application). If $G$ acts on an additive abelian group $A$ and if $g\in G$ then under the hypothesis that $g^{-1}Hg\cap K$ has finite index in $g^{-1}Hg$ (and in particular the $H$ in the previous para is $g^{-1}Hg$ here) I claim that there is a map $T_g$ from $A^K$ (the $K$-invariant elements of $A$) to $A^H$ defined by first decomposing $HgK$ as a finite (by an argument which uses my version of the second isomorphism theorem and the fact that $g^{-1}HgK/K$ bijects with $HgK/K$) disjoint union $g_iK$ and then sending $a$ to $\sum_i g_i.a$ (which is well-defined and in $A^H$ if I got all this right; note that it's not yet been formalized). So the #xy of my question is that I want to say "write a subset of $G$ which is closed under right multiplication by $K$ as a disjoint union of cosets of $K$ and choose arbitrary coset representatives" but I would like an idiomatic way to say this if we have such a way (and if not I'll have to make one).

[Kevin Buzzard]

Hmm, I guess I could look at subsets of $G/K$ and $G/(H\cap K)$, we have these, hopefully we have the $G$-action on them

[Edison Xie]

Kevin Buzzard said:

To develop the theory of Hecke operators for FLT I need what I was taught was the second isomorphism theorem, but to my surprise I've discovered that mathlib's statement of the theorem docs#QuotientGroup.quotientInfEquivProdNormalQuotient was strictly weaker than what I was taught as an undergraduate.

Let $G$ be a group and let $H$ and $K$ be subgroups, with no normality assumption on either (this is why my claim below is different to mathlib's). By $H/(H\cap K)$ I mean the set of left cosets $h(H\cap K)$ and by $HK$ I mean the set of products $\{hk:h\in H,k\in K\}$ (note that this is not a group in general, if neither $H$ nor $K$ are normal). This set is easily checked to be a union of left cosets $hK$ of $K$; by $HK/K$ I mean the set of these left cosets. I was taught that the second isomorphism theorem was the canonical bijection $H/(H\cap K)\cong HK/K$ sending $h(H\cap K)$ to $hK$. And then the rider is that if $K$ happens to be normal then $HK$ is a subgroup and both the things I'm quotienting out by are normal subgroups and the canonical map unsurprisingly preserves multiplication (which is the statement we have in mathlib).

I realised that I didn't even know how to state the version I need. We have $HK$ of type Set G as (H : Set G) * (K : Set G) after open scoped Pointwise, but do we even have $HK/K$ in any form? The \/ symbol only works for groups and in my application $HK$ will definitely not be closed under multiplication.

---

The application is this. Again let $H$ and $K$ be subgroups of a (infinite, in my case) group $G$ (neither of them normal in the application). If $G$ acts on an additive abelian group $A$ and if $g\in G$ then under the hypothesis that $g^{-1}Hg\cap K$ has finite index in $g^{-1}Hg$ (and in particular the $H$ in the previous para is $g^{-1}Hg$ here) I claim that there is a map $T_g$ from $A^K$ (the $K$-invariant elements of $A$) to $A^H$ defined by first decomposing $HgK$ as a finite (by an argument which uses my version of the second isomorphism theorem and the fact that $g^{-1}HgK/K$ bijects with $HgK/K$) disjoint union $g_iK$ and then sending $a$ to $\sum_i g_i.a$ (which is well-defined and in $A^H$ if I got all this right; note that it's not yet been formalized). So the #xy of my question is that I want to say "write a subset of $G$ which is closed under right multiplication by $K$ as a disjoint union of cosets of $K$ and choose arbitrary coset representatives" but I would like an idiomatic way to say this if we have such a way (and if not I'll have to make one).

would be a great project for the undergrads :joy: