This article describes a natural isomorphism between two structures or between a family of structures
Statement
Set-theoretic version
Suppose  are subgroups. Then, there is a natural bijection between the left coset spaces:
 are subgroups. Then, there is a natural bijection between the left coset spaces:
 .
.
Numerical version
Let  and
 and  be two subgroups of a finite group
 be two subgroups of a finite group  . Then:
. Then:
 
Here  is the product of subgroups.
 is the product of subgroups.
Related facts
- Second isomorphism theorem: This is a stronger formulation of the set-theoretic version, which holds when both the groups in the denominator are normal in the respective numerators. In this case, the natural bijection turns out to be an isomorphism.
- Index satisfies transfer inequality: This states that if  , then , then![{\displaystyle [K:H\cap K]\leq [G:H]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8e21a45694b763e0ad9015f829a499360c7ff133) . .
- Index satisfies intersection inequality: This states that if  are subgroups, then are subgroups, then![{\displaystyle [G:H\cap K]\leq [G:H][G:K]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3a7d1aeb117b5c80da4e7fa9a2320c9a65834ba7) . .
Facts used
- Subgroup containment implies coset containment: If  are subgroups, then every left coset of are subgroups, then every left coset of is contained in a left coset of is contained in a left coset of . .
- Lagrange's theorem
Proof
Proof of the set-theoretic version
Given: A group  , and subgroups
, and subgroups  .
.
To prove: There is a natural bijection between the coset spaces  and
 and  .
.
Proof: We first define the map:
 
as follows:
 .
.
In other words, it sends each coset of  to the coset of
 to the coset of  containing it.
 containing it.
- The map sends cosets to cosets: Note first that if two elements are in the same coset of  , they are in the same coset of , they are in the same coset of . Thus, the map sends cosets of . Thus, the map sends cosets of to cosets of to cosets of . (This is fact (1)). . (This is fact (1)).
- The map is well-defined with the specified domain and co-domain: Further, if  , then , then . In other words, if the original coset is in . In other words, if the original coset is in , the new coset is in , the new coset is in . Thus, the map . Thus, the map is well-defined from is well-defined from to to . .
- The map is injective: Finally,  . That means that . That means that , forcing , forcing . But we anyway have . But we anyway have , so , so , forcing that , forcing that and and are in the same coset of are in the same coset of . Thus, . Thus, . .
- The map is surjective: Any left coset of  in in can be written as can be written as where where . Thus, we can write . Thus, we can write where where . Then, . Then, , with , with . Thus, . Thus, . .
Proof of the numerical version using the set-theoretic version
The numerical version follows by combining the set-theoretic version with Lagrange's theorem:
 .
.
By Lagrange's theorem, the left side is  and the right side is
 and the right side is  . This yields:
. This yields:
 
which, upon rearrangement, gives the product formula.