這裡我們開始介紹群論

Definition. 群 Group [Group.Def]

module Group.Def where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

一個群（group）是由一個非空集合 G 跟一個二元運算子（binary operation）

• : G × G → G

構成，且滿足以下條件

G 有一個特別的元素叫單位元素（identity 或是 neutral element），用 e 表示，任何元素 g 跟它運算都是 g，也就是 g = g • e = e • g
這個運算子是 associative 的，也就是說 (a • b) • c = a • (b • c)，所以我們可以安全的寫成 a • b • c
每個元素 g ∈ G 都有一個反元素 g⁻¹ ∈ G，滿足以下等式 g • g⁻¹ = g⁻¹ • g = e

我們把這些條件匯總，就寫成了下面的定義

record Group (G : 𝓤 ̇) : 𝓤 ̇ where
  field
    size : is-set G
    _∙_ : G → G → G
    ∙-assoc : associative _∙_
    e : G
    neu-l : left-neutral e _∙_
    neu-r : right-neutral e _∙_
    _⁻¹ : G → G
    cancel : {x : G} → ((x ⁻¹) ∙ x ＝ e) × (x ∙ (x ⁻¹) ＝ e)

  infix 40 _⁻¹
  infixl 20 _∙_

Agda 小知識 [agda-0000]

在我們開始之前需要知道怎麼閱讀 agda 的證明，這裡使用的是由 Martin Escardo 維護的 TypeTopology 程式庫，下面經常會用到的是等式證明，寫成形式

A ＝⟨ B ⟩ C ∎

這段程式的意思是「因為 $B$ ，所以 $A$ 等於 $C$ 」。每個寫好的證明，都可由其他程式引用，比如

proposition-4 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → φ e ＝ e

就可以引用

φ e ＝⟨ proposition-4 φ is-hom ⟩
e ∎

這就是說 $\varphi(e_G) = e_H$ ，因為前面證明過的事實 proposition-4 φ is-hom。

Basic facts about groups [Group.Basic]

module Group.Basic where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

open import Group.Def
open Group {{...}}

現在來看一些命題

Proposition 1

假設元素 h ∈ G 是另一個滿足單位元素條件的元素，那 h = e。

事實上，很酷的事情是甚至不用完全滿足單位元素條件，就如下面的證明所演示的

proposition-1 : {G : 𝓤 ̇} {{_ : Group G}} {h : G} → left-neutral h _∙_ → h ＝ e
proposition-1 {G}{_} {h} h-is-identity =
  h     ＝⟨ sym (neu-r h) ⟩
  h ∙ e ＝⟨ h-is-identity e ⟩
  e ∎

這個命題的重點是單位元素是唯一的，所以英文的話你可以用「the」修飾。

sym 把等式翻面：A ＝ B 變成 B ＝ A

Proposition 2

如果 h₁ and h₂ 的反元素都是 g，那 h₁ = h₂。或者我們會說反元素是唯一的，跟上面的命題的意義類似。

proposition-2 : {G : 𝓤 ̇} {{_ : Group G}} {g h1 h2 : G} → (g ∙ h1 ＝ e) → (g ∙ h2 ＝ e) → h1 ＝ h2
proposition-2 {G}{_} {g}{h1}{h2} fact1 fact2 =
  h1              ＝⟨ sym (neu-l h1) ⟩
  e ∙ h1          ＝⟨ ap (_∙ h1) (sym (cancel .pr₁)) ⟩
  g ⁻¹ ∙ g ∙ h1   ＝⟨ ∙-assoc (g ⁻¹) g h1 ⟩
  g ⁻¹ ∙ (g ∙ h1) ＝⟨ ap (g ⁻¹ ∙_) fact1 ⟩
  g ⁻¹ ∙ e        ＝⟨ ap ((g ⁻¹) ∙_) (sym fact2) ⟩
  g ⁻¹ ∙ (g ∙ h2) ＝⟨ sym (∙-assoc (g ⁻¹) g h2) ⟩
  g ⁻¹ ∙ g ∙ h2   ＝⟨ ap (_∙ h2) (cancel .pr₁) ⟩
  e ∙ h2          ＝⟨ neu-l h2 ⟩
  h2 ∎

ap 把等式裡的 expression 中沒有變化的部分抽出來用的，這樣才能操作其餘要改變的部分

Proposition 3

這個命題在說每個元素都可以取消，這是一個非常好用的事實，而且完全不必感到陌生，我等一下再解釋這點。我們先來看它的具體描述

如果 g • a = h • a，則 g = h
如果 a • g = a • h，則 g = h

proposition-3 : {G : 𝓤 ̇} {{_ : Group G}} {g h a : G} → (g ∙ a ＝ h ∙ a → g ＝ h) × (a ∙ g ＝ a ∙ h → g ＝ h)
proposition-3 {G}{_} {g}{h}{a} = I , II
  where
  I : g ∙ a ＝ h ∙ a → g ＝ h
  I fact =
    g              ＝⟨ sym (neu-r g) ⟩
    g ∙ e          ＝⟨ ap (g ∙_) (sym (cancel .pr₂)) ⟩
    g ∙ (a ∙ a ⁻¹) ＝⟨ sym (∙-assoc g a (a ⁻¹)) ⟩
    g ∙ a ∙ a ⁻¹   ＝⟨ ap (_∙ a ⁻¹) fact ⟩
    h ∙ a ∙ a ⁻¹   ＝⟨ ∙-assoc h a (a ⁻¹) ⟩
    h ∙ (a ∙ a ⁻¹) ＝⟨ ap (h ∙_) (cancel .pr₂) ⟩
    h ∙ e          ＝⟨ neu-r h ⟩
    h ∎

  II : a ∙ g ＝ a ∙ h → g ＝ h
  II fact =
    g              ＝⟨ sym (neu-l g) ⟩
    e ∙ g          ＝⟨ ap (_∙ g) (sym (cancel .pr₁)) ⟩
    a ⁻¹ ∙ a ∙ g   ＝⟨ ∙-assoc (a ⁻¹) a g ⟩
    a ⁻¹ ∙ (a ∙ g) ＝⟨ ap (a ⁻¹ ∙_) fact ⟩
    a ⁻¹ ∙ (a ∙ h) ＝⟨ sym (∙-assoc (a ⁻¹) a h) ⟩
    a ⁻¹ ∙ a ∙ h   ＝⟨ ap (_∙ h) (cancel .pr₁) ⟩
    e ∙ h          ＝⟨ neu-l h ⟩
    h ∎

為什麼不必對這個命題感到陌生呢？因為這其實是我們日常也很容易遇到的算術事實：如果 2x = 2y 那 x = y。

Definition. Group Homomorphism [Group.DefHom]

module Group.DefHom where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

open import Group.Def
open Group {{...}}

我們先看 group homomorphism 的定義：

IsGroupHomomorphism : (G H : 𝓤 ̇) {{_ : Group G}} {{_ : Group H}} → (φ : G → H) → 𝓤 ̇
IsGroupHomomorphism G H φ = (x y : G) → φ (x ∙ y) ＝ (φ x) ∙ (φ y)

基本上它的意思是，我們定義如果函數 φ : G → H 能讓

φ(a • b) = φ(a) • φ(b)

對所有 a, b ∈ G 成立，那 φ 是一個 group homomorphism。

這些 homomorphism 之所以特別，就是它們保留了一些結構，讓我們能夠對群整體做出推論，這種想法以範疇論為主，有非常多有趣又深刻的延伸。

Basic facts of group homomorphism [Group.HomBasic]

module Group.HomBasic where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

open import Group.Def
open Group {{...}}
open import Group.Basic
open import Group.DefHom

所以我們接著來看一個 group homomorphism 會有什麼特性。

Proposition 4

Group homomorphism 保留單位元素，也就是說 φ(e_G) = e_H。

注意到雖然我們在數學式裡面用下標 _G、_H 區分，但在 Agda 裡面它自己就知道這件事，所以不用特別寫出

proposition-4 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → φ e ＝ e

VI 的定義最後會出現，這裡先不用在意

proposition-4 φ is-hom = VI
  where
  I : e ⁻¹ ＝ e
  I = e ⁻¹     ＝⟨ sym (neu-r (e ⁻¹)) ⟩
      e ⁻¹ ∙ e ＝⟨ cancel .pr₁ ⟩
      e ∎

這裡我們先證明 φ(e_G) = φ(e_G) • φ(e_G)

  II : φ e ＝ (φ e) ∙ (φ e)
  II = φ e          ＝⟨ ap (λ x → φ x) (sym (cancel .pr₁)) ⟩
       φ (e ⁻¹ ∙ e) ＝⟨ ap (λ x → φ (x ∙ e)) I ⟩
       φ (e ∙ e)    ＝⟨ is-hom e e ⟩
       (φ e) ∙ (φ e) ∎

再證明 φ(e_G) • φ(e_G) = e_H • φ(e_G)

  III : (φ e) ∙ (φ e) ＝ e ∙ (φ e)
  III = (φ e) ∙ (φ e) ＝⟨ sym II ⟩
        φ e           ＝⟨ sym (neu-l (φ e)) ⟩
        e ∙ φ e ∎

那我們就可以用前面證明過的 [Proposition 3] 任何元素都能取消得出結論

  VI : (φ e) ＝ e
  VI = (proposition-3 .pr₁) III

Proposition 5

Group homomorphism 保留反元素，也就是說 φ(g⁻¹) = φ(g)⁻¹ 對所有 g ∈ G 成立。

proposition-5 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → (g : G)
  → φ (g ⁻¹) ＝ (φ g) ⁻¹
proposition-5 φ is-hom g = (proposition-3 .pr₁) V
  where
  I : φ (g ⁻¹ ∙ g) ＝ φ (g ⁻¹) ∙ φ g
  I = is-hom (g ⁻¹) g

這裡馬上就用到剛剛證明的保留 identity 性質

  II : φ (g ⁻¹ ∙ g) ＝ e
  II = φ (g ⁻¹ ∙ g) ＝⟨ ap (λ x → φ x) (cancel .pr₁) ⟩
       φ e          ＝⟨ proposition-4 φ is-hom ⟩
       e ∎

  III : φ (g ⁻¹) ∙ φ g ＝ e
  III = (sym I) then II

  IV : (φ g) ⁻¹ ∙ (φ g) ＝ e
  IV = cancel .pr₁

  V : φ (g ⁻¹) ∙ φ g ＝ (φ g) ⁻¹ ∙ (φ g)
  V = III then (sym IV)

Definition. 子群 Subgroup [Group.DefSubgroup]

module Group.DefSubgroup where

open import MLTT.Spartan

open import Group.Def
open import Group.DefHom

子群的定義是，如果存在一個 inclusion 函數 i : H → G 是一個 group homomorphism，那 H 是 G 的子群。

IsSubgroup : {𝓤 : Universe} (H G : 𝓤 ̇) {{_ : Group H}} {{_ : Group G}} → 𝓤 ̇
IsSubgroup H G = Σ i ꞉ (H → G) , left-cancellable i × IsGroupHomomorphism H G i

Basic facts about subgroups [Group.SubgroupBasic]

module Group.SubgroupBasic where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-Properties

open import Group.Def
open Group {{...}}
open import Group.Basic
open import Group.DefHom
open import Group.DefSubgroup

Proposition 6

這個命題是說，對所有群都有一個子群是 trivial group。

要證明之前，我們需要看一下什麼是 trivial group，基本上它就是只有一個估拎拎的 e 元素的集合，那因為只有一個元素，能定義的二元運算子也就只有一個，根據這些我們可以定義 trivial group（𝟙 是一個只有單一元素 ⋆ 的型別）

trivial-group : Group (𝟙 {𝓤})
trivial-group .size = props-are-sets 𝟙-is-prop
trivial-group ._∙_ = λ _ _ → ⋆
trivial-group .∙-assoc = λ _ _ _ → refl
trivial-group .e = ⋆
trivial-group .neu-l = λ _ → refl
trivial-group .neu-r = λ _ → refl
trivial-group ._⁻¹ = λ _ → ⋆
trivial-group .cancel = refl , refl

現在我們可以回到證明，因為 IsSubgroup 是一個 Sigma 類型，所以我們需要提出一個 map ι，然後證明這個 map 是 inclusion 而且是 group homomorphism。

proposition-6 : {G : 𝓤 ̇} {{∈G : Group G}} {{∈𝟙 : Group 𝟙}}
  → IsSubgroup 𝟙 G
proposition-6 {𝓤} {G} = ι , lc , is-hom
  where

這個 map 在數學上常被稱為 canonical map，用來指示「很明顯」會選這個的意思，這在不同數學領域都會有類似的 canonical 的用法，雖然那個「明顯」可能很不一樣。

  ι : 𝟙 → G
  ι ⋆ = e

它的 inclusion 特性很明顯，甚至都不用到 p，因為只有一個元素

  lc : left-cancellable ι
  lc p = refl

比較複雜的會是滿足 group homomorphism 的部分，大致的思考是利用 e 的一些特性攤開出我們需要的表達式

  is-hom : IsGroupHomomorphism 𝟙 G ι
  is-hom ⋆ ⋆ =
    ι (⋆ ∙ ⋆) ＝⟨by-definition⟩
    e         ＝⟨ sym (neu-l e) ⟩
    e ∙ e     ＝⟨by-definition⟩
    (ι ⋆) ∙ (ι ⋆) ∎

Proposition 7

這個命題說 H 是 G 的 subgroup 等價於說

H 是 G 的非空子集合，且

a • b⁻¹ ∈ H

下面只證明這個條件可以推出

H 是一個群
H 是 G 的子群

因為反過來非常明顯：一個群本身當然是封閉的。

跟之前一樣，子集合寫成 inclusion 函數

proposition-7 : {G H : 𝓤 ̇} {{∈G : Group G}}
  → (i : H → G)
  → left-cancellable i
  → is-set H

怎麼表達 H 不是空集呢？只要說存在一個元素就好

  → (h : H)

∀ (a b : G) → Σ y ꞉ H , a ∙ b ⁻¹ ＝ i y 這整個型別要這樣解讀「對所有 a, b ∈ G，存在 y ∈ H 使 a • b⁻¹ = i(y)」。這裡是目前第一次用到 Σ，也就是說 Σ 當命題時，其實就是用來表達「存在某某某滿足什麼什麼條件」的

  → (∀ (a b : G) → Σ y ꞉ H , a ∙ b ⁻¹ ＝ i y)
  → Σ is-grp ꞉ Group H , IsSubgroup {𝓤} H G {{is-grp}}
proposition-7 {𝓤}{G}{H} {{∈G}} i inclusion H-is-set h cond = H-is-group , i , inclusion , is-hom
  where

接下來的證明很大的複雜性都在 H 是群這點上，尤其是因為把 cond 的類型定義成存在 y ∈ H 映射到 a ∙ b ⁻¹ 這點上，會讓接下來很多簡單的東西都藏在定義後面。其實如果可以，技巧上最好是以 G 為類型，滿足某種條件的元素，而不是真的用另一個型別 H，事情會簡單很多

這裡先定義一些工具，像 I 就在說 H 一定有一個元素可以當單位元，也就是採用前面 inhabited 那個 h : H 然後取 i h ∙ i h ⁻¹ 為單位元（這邊就是技術細節導致的問題，i h ∙ i h ⁻¹ 的類型是 G 不能直接用，還需要取一次 pr₁ 才是 H 的 term）

  I : Σ y ꞉ H , i h ∙ i h ⁻¹ ＝ i y
  I = cond (i h) (i h)
  eH : H
  eH = I .pr₁
  prop-eH : i h ∙ i h ⁻¹ ＝ i eH
  prop-eH = I .pr₂
  eH-is-identity : i eH ＝ e
  eH-is-identity = (sym prop-eH) then (cancel .pr₂)

  II : (a b : H) → Σ y ꞉ H , i a ∙ i b ⁻¹ ⁻¹ ＝ i y
  II a b = cond (i a) (i b ⁻¹)

  III : (a : H) → Σ y ꞉ H , i eH ∙ i a ⁻¹ ＝ i y
  III a = cond (i eH) (i a)

  inv-inv : (a : G) → a ⁻¹ ⁻¹ ＝ a
  inv-inv a = proposition-2 F S
    where
    F : a ⁻¹ ∙ a ⁻¹ ⁻¹ ＝ e
    F = cancel .pr₂
    S : a ⁻¹ ∙ a ＝ e
    S = cancel .pr₁

H 可以用上面定義的工具滿足群的條件

  H-is-group : Group H
  H-is-group .size = H-is-set
  H-is-group ._∙_ a b = II a b .pr₁
  H-is-group .∙-assoc x y z = inclusion VII
    where
    IV : Σ xy ꞉ H , i x ∙ i y ⁻¹ ⁻¹ ＝ i xy
    IV = II x y
    xy = IV .pr₁
    Hxy : i x ∙ i y ⁻¹ ⁻¹ ＝ i xy
    Hxy = IV .pr₂
    V : Σ yz ꞉ H , i y ∙ i z ⁻¹ ⁻¹ ＝ i yz
    V = II y z
    yz = V .pr₁
    Hyz : i y ∙ i z ⁻¹ ⁻¹ ＝ i yz
    Hyz = V .pr₂
    left = II xy z .pr₁
    right = II x yz .pr₁
    help1 = II xy z .pr₂
    help2 = II x yz .pr₂
    mid : i xy ∙ i z ⁻¹ ⁻¹ ＝ i x ∙ i yz ⁻¹ ⁻¹
    mid =
      i xy ∙ i z ⁻¹ ⁻¹        ＝⟨ ap (i xy ∙_) (inv-inv (i z)) ⟩
      i xy ∙ i z              ＝⟨ ap (_∙ i z) (sym Hxy) ⟩
      i x ∙ i y ⁻¹ ⁻¹ ∙ i z   ＝⟨ ap (λ y → i x ∙ y ∙ i z) (inv-inv (i y)) ⟩
      i x ∙ i y ∙ i z         ＝⟨ ap (i x ∙ i y ∙_) (sym (inv-inv (i z))) ⟩
      i x ∙ i y ∙ i z ⁻¹ ⁻¹   ＝⟨ ∙-assoc (i x) (i y) (i z ⁻¹ ⁻¹) ⟩
      i x ∙ (i y ∙ i z ⁻¹ ⁻¹) ＝⟨ ap (i x ∙_) Hyz ⟩
      i x ∙ i yz              ＝⟨ ap (i x ∙_) (sym (inv-inv (i yz))) ⟩
      i x ∙ i yz ⁻¹ ⁻¹ ∎
    VII : i left ＝ i right
    VII = (sym help1) then mid then help2
  H-is-group .e = eH
  H-is-group .neu-l x = inclusion VI
    where
    IV : Σ y ꞉ H , i eH ∙ i x ⁻¹ ⁻¹ ＝ i y
    IV = II eH x
    y = IV .pr₁
    V : i eH ∙ i x ⁻¹ ⁻¹ ＝ i y
    V = IV .pr₂
    VI : i y ＝ i x
    VI =
      i y              ＝⟨ sym V ⟩
      i eH ∙ i x ⁻¹ ⁻¹ ＝⟨ ap (_∙ i x ⁻¹ ⁻¹) eH-is-identity ⟩
      e ∙ i x ⁻¹ ⁻¹    ＝⟨ neu-l (i x ⁻¹ ⁻¹) ⟩
      i x ⁻¹ ⁻¹        ＝⟨ inv-inv (i x) ⟩
      i x ∎
  H-is-group .neu-r x = inclusion VI
    where
    IV : Σ y ꞉ H , i x ∙ i eH ⁻¹ ⁻¹ ＝ i y
    IV = II x eH
    y = IV .pr₁
    V : i x ∙ i eH ⁻¹ ⁻¹ ＝ i y
    V = IV .pr₂
    VI : i y ＝ i x
    VI =
      i y              ＝⟨ sym V ⟩
      i x ∙ i eH ⁻¹ ⁻¹ ＝⟨ ap (i x ∙_) (inv-inv (i eH)) ⟩
      i x ∙ i eH       ＝⟨ ap (i x ∙_) eH-is-identity ⟩
      i x ∙ e          ＝⟨ neu-r (i x) ⟩
      i x ∎
  H-is-group ._⁻¹ x = III x .pr₁
  H-is-group .cancel {x} = left , right
    where
    x' = III x .pr₁
    Hx' : i eH ∙ i x ⁻¹ ＝ i x'
    Hx' = III x .pr₂

    l = II x' x .pr₁
    Hl : i x' ∙ i x ⁻¹ ⁻¹ ＝ i l
    Hl = II x' x .pr₂
    step-left : i x' ∙ i x ⁻¹ ⁻¹ ＝ i eH
    step-left =
      i x' ∙ i x ⁻¹ ⁻¹            ＝⟨ ap (_∙ i x ⁻¹ ⁻¹) (sym Hx') ⟩
      i eH ∙ i x ⁻¹ ∙ i x ⁻¹ ⁻¹   ＝⟨ ∙-assoc (i eH) (i x ⁻¹) (i x ⁻¹ ⁻¹) ⟩
      i eH ∙ (i x ⁻¹ ∙ i x ⁻¹ ⁻¹) ＝⟨ ap (i eH ∙_) (cancel .pr₂) ⟩
      i eH ∙ e                    ＝⟨ neu-r (i eH) ⟩
      i eH ∎

    r = II x x' .pr₁
    Hr : i x ∙ i x' ⁻¹ ⁻¹ ＝ i r
    Hr = II x x' .pr₂
    step-right : i x ∙ i x' ⁻¹ ⁻¹ ＝ i eH
    step-right =
      i x ∙ i x' ⁻¹ ⁻¹      ＝⟨ ap (i x ∙_) (inv-inv (i x')) ⟩
      i x ∙ i x'            ＝⟨ ap (i x ∙_) (sym Hx') ⟩
      i x ∙ (i eH ∙ i x ⁻¹) ＝⟨ ap (i x ∙_) (ap (_∙ i x ⁻¹) eH-is-identity) ⟩
      i x ∙ (e ∙ i x ⁻¹)    ＝⟨ ap (i x ∙_) (neu-l (i x ⁻¹)) ⟩
      i x ∙ i x ⁻¹          ＝⟨ cancel .pr₂ ⟩
      e                     ＝⟨ sym eH-is-identity ⟩
      i eH ∎

    left : (l ＝ eH)
    left = inclusion ((sym Hl) then step-left)
    right : (II x x' .pr₁ ＝ eH)
    right = inclusion ((sym Hr) then step-right)

證明的最後一個部分是推論出這樣的 inclusion map 一定是 group homomorphism

  is-hom : IsGroupHomomorphism H G {{H-is-group}} i
  is-hom x y =
    i (II x y .pr₁) ＝⟨ sym (II x y .pr₂) ⟩
    i x ∙ i y ⁻¹ ⁻¹ ＝⟨ ap (i x ∙_) (inv-inv (i y)) ⟩
    i x ∙ i y ∎

Definition. Kernel [Group.DefKer]

module Group.DefKer where

open import MLTT.Spartan

open import Group.Def
open Group {{...}}
open import Group.DefHom

一個 Kernel 是指一個 group homomorphism 的 domain 的子集裡面，那些 maps 到 codomain 的 identity 的元素，所以這裡定義成

Ker : {𝓤 : Universe} (H G : 𝓤 ̇) {{_ : Group H}} {{_ : Group G}} (i : H → G) → IsGroupHomomorphism H G i → 𝓤 ̇
Ker H G i _ = Σ h ꞉ H , i h ＝ e

Basic facts of Kernel [Group.KerBasic]

{-# OPTIONS --allow-unsolved-metas #-}
module Group.KerBasic where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import UF.Base
open import UF.Equiv

open import Group.Def
open Group {{...}}
open import Group.DefHom
open import Group.DefKer
open import Group.HomBasic

Proposition 8

這個命題是說，如果 group homomorphism i : H → G 是 inclusion，那 Kernel 的元素其實只有單位元素 e_H。

proposition-8 : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}}
  (i : H → G) → (is-hom : IsGroupHomomorphism H G i)
  → left-cancellable i
  → ((y : Ker H G i is-hom) → e ＝ y .pr₁)
proposition-8 {𝓤} {H}{G}{{∈H}}{{∈G}} i is-hom inclusion (h , p) = inclusion I
  where
  I : i e ＝ i h
  I = (proposition-4 i is-hom) then (sym p)

這也順便說明了，用 Propopsition 4 就已經知道 Ker i 最少最少也有一個 e_H，因此任何 Kernel 都不是空集合。事實上這還可以說成，這樣 Kernel 就會跟 𝟙 同構，因為只有一個元素，這也表示這時候 Kernel 是 trivial group。

proposition-8' : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}}
  (i : H → G) → (is-hom : IsGroupHomomorphism H G i)
  → left-cancellable i
  → Ker H G i is-hom ≃ 𝟙 {𝓤}
proposition-8' {𝓤} {H}{G}{{∈H}}{{∈G}} i is-hom inclusion =
  ι , (ρ , λ x → refl) , ρ , final
  where
  ι : Ker H G i is-hom → 𝟙
  ι _ = ⋆
  P4 = proposition-4 i is-hom
  ρ : 𝟙 → Ker H G i is-hom
  ρ ⋆ = e , P4

  final : (x : Ker H G i is-hom) → ρ ⋆ ＝ x
  final (k , hk) =
    ρ ⋆    ＝⟨by-definition⟩
    e , P4 ＝⟨ to-Σ-＝ (I , size (transport (λ h → i h ＝ e) I P4) hk) ⟩
    k , hk ∎
    where
    I : e ＝ k
    I = inclusion (i e ＝⟨ P4 ⟩
                   e   ＝⟨ sym hk ⟩
                   i k ∎)

Definition. Normal subgroup [Group.Normal]

module Group.Normal where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)

open import Group.Def
open Group {{...}}
open import Group.DefHom
open import Group.HomBasic

如果 G 的子群 N 對所有 g ∈ G 跟 n ∈ N 滿足以下條件

g • h • g⁻¹ ∈ N

我們就說 N 是 Normal subgroup。

Proposition 9

為了避免複雜的編碼，下面直接根據需求定義。

這個命題是說，任何 φ : H → G 的 Kernel 都是 H 的 normal subgroup。所以我們想要證明的是對於任何屬於 Kernel 的元素 h，元素 g • h • g⁻¹ 也屬於 Kernel。

前面已經提過 φ 的 Kernel 的定義是 φh = e 的那些元素，因此定義 x ∈Ker[ φ , φ-is-hom ] 為 φ x = e。

_∈Ker[_,_] : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}} (h : H) → (φ : H → G) → IsGroupHomomorphism H G φ → 𝓤 ̇
h ∈Ker[ φ , is-hom ] = φ h ＝ e

明確提供 IsGroupHomomorphism 是無奈之舉，因為以目前的定義方式，如果把 IsGroupHomomorphism 設為隱式參數，agda 會找不到而留下一個未解的變量。

proposition-9 : {H G : 𝓤 ̇} {{∈H : Group H}} {{∈G : Group G}}
  (f : H → G) → (is-hom : IsGroupHomomorphism H G f)
  → ((h : H) → h ∈Ker[ f , is-hom ] → (g : H) → g ∙ h ∙ g ⁻¹ ∈Ker[ f , is-hom ])
proposition-9 {𝓤} {H}{G}{{∈H}}{{∈G}} f is-hom h in-ker g = I
  where
  I : f (g ∙ h ∙ g ⁻¹) ＝ e
  I = f (g ∙ h ∙ g ⁻¹)     ＝⟨ is-hom (g ∙ h) (g ⁻¹) ⟩
      f (g ∙ h) ∙ f (g ⁻¹) ＝⟨ ap (_∙ f (g ⁻¹)) (is-hom g h)  ⟩
      f g ∙ f h ∙ f (g ⁻¹) ＝⟨ ap (f g ∙ f h ∙_) (proposition-5 f is-hom g) ⟩
      f g ∙ f h ∙ f g ⁻¹   ＝⟨ ap (λ x → f g ∙ x ∙ f g ⁻¹) in-ker ⟩

因為 h 屬於 Kernel 所以 f h 可以換成 e

      f g ∙ e ∙ f g ⁻¹     ＝⟨ ap (_∙ f g ⁻¹) (neu-r (f g)) ⟩
      f g ∙ f g ⁻¹         ＝⟨ cancel .pr₂ ⟩
      e ∎

群可以視為一個範疇 [Group.IsCat]

open import UF.FunExt
module Group.IsCat (fe : Fun-Ext) where

open import MLTT.Spartan renaming (_⁻¹ to sym; _∙_ to _then_)
open import Categories.Category fe

open import Group.Def
open Group {{...}}

最後我們就用範疇論的常見笑話：群也可以視為一個範疇作為群論的收尾

group-is-cat : (G : 𝓥 ̇ ) {{_ : Group G}} → precategory 𝓤 𝓥
group-is-cat {𝓥}{𝓤} G = make str axioms
  where

這個範疇只會有一個物件，所以型別是 𝟙

  ob = 𝟙

這個範疇的 hom-set 就是群 G

  hom : 𝟙 → 𝟙 → 𝓥 ̇
  hom ⋆ ⋆ = G

物件 x 的 identity hom id_x 由 G 的 identity element 提供

  idn : 𝟙 → G
  idn ⋆ = e

⊚ 表示 hom 的組合，計算上由 G 的 operation 提供

  ⊚ : (A B C : 𝟙) → (f g : G) → G
  ⊚ ⋆ ⋆ ⋆ f g = f ∙ g

這些構成了範疇論需要的基本資料

  str : category-structure 𝓤 𝓥
  str = ob , hom , idn , ⊚

我們需要證明它滿足範疇論所有 hom 的性質

hom-set 是一個集合
id_x 接 f 等於 f
f 接 id_x 等於 f
associativity 的性質

這些都是直接繼承 G 自己的性質。

  axioms : precategory-axioms str
  axioms = (λ A B → size) , (λ A B → neu-l) , (λ A B → neu-r) , final
    where
    final : (A B C D : 𝟙) → (f g h : G) → ⊚ A B D f (⊚ B C D g h) ＝ ⊚ A C D (⊚ A B C f g) h
    final A B C D f g h =
      ⊚ A B D f (⊚ B C D g h) ＝⟨by-definition⟩
      f ∙ (g ∙ h)             ＝⟨ sym (∙-assoc f g h) ⟩
      (f ∙ g) ∙ h             ＝⟨by-definition⟩
      ⊚ A C D (⊚ A B C f g) h ∎