補題
Grp を集合の圏とする。
I を小さいフィルター圏(>>97)とする。
F：I → Grp を関手とする。
S = ΣF(i) を直和集合とし、f_i：F(i) → S を標準写像とする。
≡ を>>109で定義した同値関係とする。
L を商集合 S/≡ とし、p：S → L を標準写像とする。
x ∈ S に対して p(x) を [x] と書くことにする。

x ∈ F(i)、y ∈ F(j) とする。
I はフィルター圏だから u：i → k、v：j → k となる射がある。
[x] と [y] の積 [x][y] を [F(u)(x)・F(v)(y)] により定義する。

このとき、この積は各同値類の代表の取り方によらず
L はこの乗法により群となる。

証明
積が各代表の取り方によらないことは I がフィルター圏であることから容易に分かる。
L がこの乗法により群となることは定義から明らかである。
証明終