1 For the construction of "Complete Group Ring"

1.1 Definition

For a Profinite group $G$ and a commutative ring $R$

$R[[G]] = \lim_{\leftarrow, N\ is\ open\ normal\ subgroup} R[G/N]$

In which inverse limit is realized as the subtype of the product space satisfying the transition map between coordinates. The transition map $R[G/N_1] \rightarrow R[G/N_2]$ for $N_1 \le N_2$ is induced by the canonical map $G/N_1 \rightarrow G/N_2$

1.2 Properties

1.2.0 Other basic constructions (copy MonoidAlgebra)

1.2.1 Verify the above construction satisfies the universal property of limit

1.2.2 For $G : ProfiniteGrp$, with $G = \lim_{\leftarrow, \lambda\in\Lambda} G_\lambda$ we have $R[[G]] \cong \lim_{\leftarrow, \lambda\in\Lambda} R[G_\lambda]$ especially for $\Lambda = \mathbb{N}$

2 For the isomorphism

In this section $R$ notes for a p-adic separably complete commutative ring (i.e. $R = \lim_\leftarrow R/p^nR$)

2.1 The small isomorphisms

2.1.1 if write $[1,mod,p^i]$ as $1 + T$ there is an isomorphism $R[\mathbb{Z}/p^i\mathbb{Z}] \cong R[T] / ((1 + T)^{p^i} - 1)$

generated by$[1,mod,p^i] \mapsto 1 + T.$

2.1.2 Take inverse limit on the two sides of the isomorphism above

2.2 $\lim_{\leftarrow, i} R[T] / ((1 + T)^{p^i} - 1) \cong R[[T]].$

2.3 other trivial transition maps

3 For the UFD

3.1 Finish "Weierstrass Preparation" for DVR (gnl's job)

3.2 PowerSeries on a DVR is UFD