子群群代数上的群代数模自由性证明问询
大家好，我之前在MathOverflow上问过这个问题，有人建议我来这里提问。下面是我的问题：
我觉得我要做的这件事应该不难，但就是没理清思路。
设$K$是有限群$H$的子群，$A$是含单位元的交换环。考虑群代数$A[K] \subset A[H]$，我想证明$A[H]$作为$A[K]$模是自由模。
我的现有思路
我觉得商$A[H]/A[K]$是有限的（如果这是对的，怎么证明呢？）。然后我们可以取陪集代表元$x_1, \dots, x_n \in A[H]$，其中$n$是商的基数。我觉得这些$x_i$构成$A[H]$作为$A[K]$模的基（同样，怎么验证这一点？）。
希望能得到大家的帮助！
社区解答思路
其实你已经找对方向啦，咱们一步步把逻辑理清楚：
先澄清“商的有限性”：你提到的“$A[H]/A[K]$”其实更准确的是群$H$关于子群$K$的左陪集集合$H/K$，它的大小（基数）是群指数$[H:K] = |H|/|K|$——因为$H$是有限群，这个指数必然是有限的。而$A[H]$作为$A$-模本身就是自由模，它的基就是$H$中的所有元素，我们可以把$A[H]$拆成陪集对应子模的直和：
$$A[H] = \bigoplus_{x \in H/K} xA[K]$$
这里每个$xA[K]$都是$A[K]$左模，而且和$A[K]$自身作为模是同构的（映射$xa \mapsto a$，$a \in A[K]$就能建立同构）。验证陪集代表元是自由基：取$H/K$的一组代表元$x_1, x_2, \dots, x_n$（$n=[H:K]$），我们可以从两个关键性质验证它们是$A[H]$作为$A[K]$模的基：
- 生成性：$H$里的每个元素都属于某个陪集$x_i K$，也就是能写成$x_i k$（$k \in K$）的形式。而$A[H]$中的元素都是$H$中元素的$A$-线性组合，自然就能表示成$x_1, \dots, x_n$分别乘以$A[K]$中元素的和。
- 线性无关性：假设$\sum_{i=1}^n x_i k_i = 0$，其中每个$k_i = \sum_{k \in K} a_{i,k} k$（$a_{i,k} \in A$）。把这个式子展开后得到$\sum_{i=1}^n \sum_{k \in K} a_{i,k} x_i k = 0$。注意${x_i k \mid 1 \leq i \leq n, k \in K}$刚好是$H$的全部元素，也就是$A[H]$作为$A$-模的基，所以所有系数$a_{i,k}$都必须是0，进而每个$k_i$也都是0。这就证明了这些$x_i$是线性无关的。
这样就完整证明了$A[H]$是秩为$[H:K]$的自由$A[K]$模哦。
备注：内容来源于stack exchange，提问作者EJB
