Editing Profinite group (section)

===First definition (constructive)===

A profinite group is a topological group that is [[isomorphism|isomorphic]] to the [[inverse limit]] of an [[inverse system]] of [[discrete space|discrete]] finite groups.<ref>{{Cite web|url=http://websites.math.leidenuniv.nl/algebra/Lenstra-Profinite.pdf|title=Profinite Groups|last=Lenstra|first=Hendrik|website=Leiden University}}</ref> In this context, an inverse system consists of a [[directed set]]  <math>(I, \leq),</math> an [[indexed family]] of finite groups <math>\{G_i: i \in I\},</math> each having the [[discrete topology]], and a family of [[Group homomorphism|homomorphisms]] <math>\{f^j_i : G_j \to G_i \mid i, j \in I, i \leq j\}</math> such that <math>f_i^i</math> is the [[identity map]] on <math>G_i</math> and the collection satisfies the composition property <math>f^j_i \circ f^k_j = f^k_i</math> whenever <math>i\leq j\leq k.</math> The inverse limit is the set:
<math display=block>\varprojlim G_i = \left\{(g_i)_{i \in I} \in {\textstyle\prod\limits_{i \in I}} G_i : f^j_i (g_j) = g_i \text{ for all } i\leq j\right\}</math>
equipped with the [[Subspace topology|relative]] [[product topology]].

One can also define the inverse limit in terms of a [[universal property]]. In [[category theory|categorical]] terms, this is a special case of a [[filtered category|cofiltered limit]] construction.