Definition. 環 Ring [ring-0000]

module ring-0000 where

open import MLTT.Spartan
open import UF.Sets

record Ring (R : 𝓤 ̇ ) : 𝓤 ̇ where
  field
    size : is-set R

    _+ᴿ_ : R → R → R
    +-assoc : associative _+ᴿ_
    +-comm : commutative _+ᴿ_

    0r : R
    +-neuL : left-neutral 0r _+ᴿ_
    +-neuR : right-neutral 0r _+ᴿ_

    -_ : R → R
    cancel : {x : R} → (x +ᴿ - x ＝ 0r)

    _·_ : R → R → R
    ·-assoc : associative _·_

    1r : R
    ·-neuL : left-neutral 1r _·_
    ·-neuR : right-neutral 1r _·_

    distribL : {r s t : R} → (r +ᴿ s) · t ＝ (r · t) +ᴿ (s · t)
    distribR : {r s t : R} → t · (r +ᴿ s) ＝ (t · r) +ᴿ (t · s)

  infixl 30 _+ᴿ_
  infixl 41 _·_
  infixl 50 -_

下面這個命題是因為 (R, ⊕, 0_R) 也可以看成一個 commutative group，因此也可以取消共相加的元素來得到結果。其實就是「若 x + 2 = y + 2 則 x = y」

open Ring {{...}}
ring-cancel-right : {R : 𝓤 ̇ } → {{_ : Ring R}} {r s t : R} → s +ᴿ r ＝ t +ᴿ r → s ＝ t
ring-cancel-right {R}{_} {r}{s}{t} fact =
  s               ＝⟨ +-neuR s ⁻¹ ⟩
  s +ᴿ 0r         ＝⟨ ap (s +ᴿ_) (cancel ⁻¹) ⟩
  s +ᴿ (r +ᴿ - r) ＝⟨ +-assoc s r (- r) ⁻¹ ⟩
  s +ᴿ r +ᴿ - r   ＝⟨ ap (_+ᴿ - r) fact ⟩
  t +ᴿ r +ᴿ - r   ＝⟨ +-assoc t r (- r) ⟩
  t +ᴿ (r +ᴿ - r) ＝⟨ ap (t +ᴿ_) cancel ⟩
  t +ᴿ 0r         ＝⟨ +-neuR t ⟩
  t ∎

Example. trivial ring [ring-0001]

module ring-0001 where

open import MLTT.Spartan
open import UF.Subsingletons
open import UF.Subsingletons-Properties
open import UF.Equiv

open import ring-0000
open Ring {{...}}
open import ring-0002

Trivial ring 就像前面群論提過的 trivial group，在 trivial ring 裡加法、乘法都一樣，因為作為只有一個元素的集合，能選擇的 n-元運算都只有一個。也因此下面的 terms 幾乎都可以由 agda 自動填滿

trivial-ring : Ring (𝟙 {𝓤})
trivial-ring .size = props-are-sets 𝟙-is-prop
trivial-ring ._+ᴿ_ _ _ = ⋆
trivial-ring .0r = ⋆
trivial-ring .+-assoc = λ x y z → refl
trivial-ring .+-neuL = λ x → refl
trivial-ring .+-neuR = λ x → refl
trivial-ring .-_ _ = ⋆
trivial-ring .cancel = refl
trivial-ring .+-comm = λ x y → refl
trivial-ring ._·_ _ _ = ⋆
trivial-ring .·-assoc = λ x y z → refl
trivial-ring .1r = ⋆
trivial-ring .·-neuL = λ x → refl
trivial-ring .·-neuR = λ x → refl
trivial-ring .distribL = refl
trivial-ring .distribR = refl

事實上如果 Ring R 的 1 = 0，那麼 R 只有一個元素

0=1-leads-trivial-ring : {R : 𝓤 ̇ } → {{∈R : Ring R}} → 1r ＝ 0r → 𝟙 {𝓤} ≃ R
0=1-leads-trivial-ring {𝓤}{R} 1=0 = (λ _ → 0r) , (ι , λ x → every-elem-is-0 x ⁻¹) , (ι , λ _ → refl)
  where
  ι : R → 𝟙 {𝓤}
  ι _ = ⋆

  every-elem-is-0 : ∀ (x : R) → x ＝ 0r
  every-elem-is-0 x =
    x      ＝⟨ ·-neuR x ⁻¹ ⟩
    x · 1r ＝⟨ ap (x ·_) 1=0 ⟩
    x · 0r ＝⟨ lemma-1 x .pr₁ ⟩

這裡雖然用了等一下才要證明的定理，但任何元素乘上 0 等於 0 應該是很直覺的想法

    0r ∎

Lemma. Multiply 0 is 0 [ring-0002]

module ring-0002 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

lemma-1 : {R : 𝓤 ̇ } {{_ : Ring R}} → (r : R) → (r · 0r ＝ 0r) × (0r · r ＝ 0r)
lemma-1 r = (ring-cancel-right I ⁻¹) , (ring-cancel-right II ⁻¹)
  where
  I : 0r +ᴿ r · 0r ＝ r · 0r +ᴿ r · 0r
  I =
    0r +ᴿ r · 0r   ＝⟨ +-neuL (r · 0r) ⟩
    r · 0r         ＝⟨ ap (r ·_) (+-neuL 0r ⁻¹) ⟩
    r · (0r +ᴿ 0r) ＝⟨ distribR ⟩
    r · 0r +ᴿ r · 0r ∎

  II : 0r +ᴿ 0r · r ＝ 0r · r +ᴿ 0r · r
  II =
    0r +ᴿ 0r · r   ＝⟨ +-neuL (0r · r) ⟩
    0r · r         ＝⟨ ap (_· r) (+-neuL 0r ⁻¹) ⟩
    (0r +ᴿ 0r) · r ＝⟨ distribL ⟩
    0r · r +ᴿ 0r · r ∎

Proposition. 負負得正 [ring-0003]

module ring-0003 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}
open import ring-0002

負負得正通常可能在說兩件事。第一，− − a = a，因為 −a 的反元素是 a 也可以是 − − a，因此 − − a 一定等於 a（因為 Ring 的加法部分是一個 commutative group）。

neg-neg-lemma : {R : 𝓤 ̇ } {{_ : Ring R}} (x : R) → - - x ＝ x
neg-neg-lemma x = ring-cancel-right (I ∙ II ⁻¹)
  where
  I : - - x +ᴿ - x ＝ 0r
  I = (+-comm (- - x) (- x)) ∙ cancel
  II : x +ᴿ - x ＝ 0r
  II = cancel

或是更重要的 −a × −b = a × b，也就是這裡要證明的命題

neg-lemma-left : {R : 𝓤 ̇ } {{_ : Ring R}} (a b : R) → - a · b ＝ - (a · b)
neg-lemma-left a b = ring-cancel-right (II ∙ I ⁻¹)
  where
  I : (- (a · b)) +ᴿ a · b ＝ 0r
  I = (- (a · b)) +ᴿ a · b ＝⟨ (+-comm (- (a · b)) (a · b)) ∙ cancel ⟩
      0r ∎
  II : (- a · b) +ᴿ a · b ＝ 0r
  II = (- a · b) +ᴿ a · b ＝⟨ distribL ⁻¹ ⟩
      (- a +ᴿ a) · b      ＝⟨ ap (_· b) ((+-comm (- a) a) ∙ cancel) ⟩
      0r · b              ＝⟨ lemma-1 b .pr₂ ⟩
      0r ∎
neg-lemma-right : {R : 𝓤 ̇ } {{_ : Ring R}} (a b : R) → a · - b ＝ - (a · b)
neg-lemma-right a b = ring-cancel-right (II ∙ I ⁻¹)
  where
  I : (- (a · b)) +ᴿ a · b ＝ 0r
  I = (+-comm (- (a · b)) (a · b)) ∙ cancel
  II : (a · - b) +ᴿ a · b ＝ 0r
  II = (a · - b) +ᴿ a · b ＝⟨ distribR ⁻¹ ⟩
      a · (- b +ᴿ b)      ＝⟨ ap (a ·_) ((+-comm (- b) b) ∙ cancel) ⟩
      a · 0r              ＝⟨ lemma-1 a .pr₁ ⟩
      0r ∎

proposition-2 : {R : 𝓤 ̇ } {{_ : Ring R}} → (a b : R) → - a · - b ＝ a · b
proposition-2 {_}{R} a b =
  (- a · - b) ＝⟨ neg-lemma-left a (- b) ⟩
  - (a · - b) ＝⟨ ap -_ (neg-lemma-right a b) ⟩
  - - (a · b) ＝⟨ neg-neg-lemma (a · b) ⟩
  a · b ∎

Definition. Non zero-divisor [ring-0004]

module ring-0004 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

一個 Ring R 中的元素 a 是 zero divisor 就表示存在 b ≠ 0 ∈ R 使 ab = 0。所以我們稱 a 是 non zero-divisor 指如果 ab = 0，那 b 一定等於 0。

NonZeroDivisor : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → 𝓤 ̇
NonZeroDivisor {_}{R} a = (b : R) → (a · b ＝ 0r → b ＝ 0r)

(Left) Action [ring-0006]

module ring-0006 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

一個 Ring R 中的元素 a 所謂的 (left) action 是指

x ↦ a ⋅ x

R → R 這樣的 map，通常記為 L_a。所謂的 (right) action 可想而知，在乘法交換的 commutative ring 中兩種 action 並沒有差異，這時候定義通常跟那個領域的慣例有關。

left-action : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → R → R
left-action a x = a · x

right-action : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → R → R
right-action a x = x · a

Proposition. An element is not a (left) zero divisor if and only if (left) action is injective [ring-0005]

$a \in R$ 不是 zero divisor 若且唯若其 left action $x \mapsto a x$ 是 injective（也就是 left-cancellable）

module ring-0005 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}
open import ring-0002
open import ring-0003
open import ring-0004
open import ring-0006

proposition-3 : {R : 𝓤 ̇ } {{_ : Ring R}} {a : R} → NonZeroDivisor a ↔ left-cancellable (left-action a)
proposition-3 {_}{R}{a} = if , only-if
  where
  if : NonZeroDivisor a → left-cancellable (left-action a)
  if is-not-zd {x}{y} Ax=Ay = ring-cancel-right (II ∙ III ⁻¹)
    where
    I : left-action a (x +ᴿ - y) ＝ 0r
    I =
      left-action a (x +ᴿ - y) ＝⟨by-definition⟩
      a · (x +ᴿ - y)           ＝⟨ distribR ⟩
      a · x +ᴿ a · - y         ＝⟨ ap (a · x +ᴿ_) (neg-lemma-right a y) ⟩
      a · x +ᴿ - (a · y)       ＝⟨ ap (_+ᴿ - (a · y)) Ax=Ay ⟩
      a · y +ᴿ - (a · y)       ＝⟨ cancel ⟩
      0r ∎
    II : x +ᴿ - y ＝ 0r
    II = is-not-zd (x +ᴿ - y) I
    III : y +ᴿ - y ＝ 0r
    III = cancel
  only-if : left-cancellable (left-action a) → NonZeroDivisor a
  only-if inj b ab=0 = inj I
    where
    I : a · b ＝ a · 0r
    I = left-action a b ＝⟨by-definition⟩
        a · b           ＝⟨ ab=0 ⟩
        0r              ＝⟨ lemma-1 a .pr₁ ⁻¹ ⟩
        a · 0r          ＝⟨by-definition⟩
        left-action a 0r ∎

(Left) Unit [ring-0007]

module ring-0007 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

u 是 left unit 的意思是存在 v 使 u ⋅ v = 1
u 是 right unit 的意思是存在 v 使 v ⋅ u = 1

is-left-unit : {R : 𝓤 ̇ } {{_ : Ring R}} → R → 𝓤 ̇
is-left-unit {_} {R} u = Σ v ꞉ R , u · v ＝ 1r

is-right-unit : {R : 𝓤 ̇ } {{_ : Ring R}} → R → 𝓤 ̇
is-right-unit {_} {R} u = Σ v ꞉ R , v · u ＝ 1r

Proposition. An element is a (left) unit if and only if (left) action has a section [ring-0008]

module ring-0008 where

open import MLTT.Spartan
open import UF.Retracts

open import ring-0000
open Ring {{...}}
open import ring-0006
open import ring-0007

proposition-4 : {R : 𝓤 ̇ } {{_ : Ring R}} → (u : R) → is-left-unit u ↔ has-section (left-action u)
proposition-4 {_} {R} u = if , only-if
  where
  if : is-left-unit u → has-section (left-action u)
  if (v , mul-to-one) = left-action v , iso-to-id
    where
    iso-to-id : (r : R) → (left-action u (left-action v r)) ＝ r
    iso-to-id r =
      (left-action u (left-action v r)) ＝⟨by-definition⟩
      u · (v · r)                       ＝⟨ ·-assoc u v r ⁻¹ ⟩
      (u · v) · r                       ＝⟨ ap (_· r) mul-to-one ⟩
      1r · r                            ＝⟨ ·-neuL r ⟩
      r ∎

  only-if : has-section (left-action u) → is-left-unit u
  only-if (sec , to-id) = sec 1r , to-id 1r

Proposition. If an element is a (left) unit then its (right) action is injective [ring-0009]

module ring-0009 where

open import MLTT.Spartan
open import UF.Retracts

open import ring-0000
open Ring {{...}}
open import ring-0006
open import ring-0007

proposition-5 : {R : 𝓤 ̇ } {{_ : Ring R}} → (u : R) → is-left-unit u → left-cancellable (right-action u)
proposition-5 u (v , uv＝1) {x}{y} xu＝yu =
  x           ＝⟨ ·-neuR x ⁻¹ ⟩
  x · 1r      ＝⟨ ap (x ·_) (uv＝1 ⁻¹) ⟩
  x · (u · v) ＝⟨ ·-assoc x u v ⁻¹ ⟩
  x · u · v   ＝⟨ ap (_· v) xu＝yu ⟩
  y · u · v   ＝⟨ ·-assoc y u v ⟩
  y · (u · v) ＝⟨ ap (y ·_) uv＝1 ⟩
  y · 1r      ＝⟨ ·-neuR y ⟩
  y ∎

Proposition. Multiplication inverse of two sided unit is unique [ring-000A]

module ring-000A where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}
open import ring-0007

proposition-6 : {R : 𝓤 ̇ } {{_ : Ring R}} → (u : R) → (L : is-left-unit u) → (R : is-right-unit u) → L .pr₁ ＝ R .pr₁
proposition-6 u (v , uv=1) (k , ku=1) =
  v           ＝⟨ ·-neuL v ⁻¹ ⟩
  1r · v      ＝⟨ ap (_· v) (ku=1 ⁻¹) ⟩
  k · u · v   ＝⟨ ·-assoc k u v ⟩
  k · (u · v) ＝⟨ ap (k ·_) uv=1 ⟩
  k · 1r      ＝⟨ ·-neuR k ⟩
  k ∎

Definition. Ideal [ring-000B]

module ring-000B where

open import MLTT.Spartan
open import UF.Powerset

open import ring-0000
open Ring {{...}}

record IsIdeal {R : 𝓤 ̇ } {{_ : Ring R}} (I : 𝓟 R) : 𝓤 ̇  where
  no-eta-equality
  field
    close-+ : ∀ {i} {i2} → i ∈ I → i2 ∈ I → (i +ᴿ i2) ∈ I
    close-neg : ∀ {i} → i ∈ I → (- i) ∈ I
    closeL : ∀ r {i} → i ∈ I → r · i ∈ I
    closeR : ∀ r {i} → i ∈ I → i · r ∈ I

Proposition. Ideals contain zero [ring-000C]

module ring-000C where

open import MLTT.Spartan
open import UF.Powerset

open import ring-0000
open Ring {{...}}
open import ring-000B

這個命題說每個 Ideal 都有元素 0

proposition-7 : {R : 𝓤 ̇ } {{_ : Ring R}} {i : R} (I : 𝓟 R) → IsIdeal I → i ∈ I → 0r ∈ I
proposition-7 {_}{R} {i} I is-ideal i∈I = transport (_∈ I) cancel m
  where
  open IsIdeal is-ideal

  neg : - i ∈ I
  neg = close-neg i∈I
  m : (i +ᴿ - i) ∈ I
  m = close-+ i∈I neg

Proposition. Ideals 相加的構造還是一個 ideal [ring-000D]

open import UF.PropTrunc
module ring-000D (pt : propositional-truncations-exist) where

open import MLTT.Spartan
open import UF.Powerset
open import UF.SubtypeClassifier
open import UF.Subsingletons

open import ring-0000
open Ring {{...}}
open import ring-000B
open import ring-000C

open PropositionalTruncation pt

如果 I 跟 J 是 R 的 ideals，那麼

I + J := {i + j ∣ i ∈ I, j ∈ J}

也是 R 的 ideal。

T : {R : 𝓤 ̇ } {{_ : Ring R}} → (I J : 𝓟 R) → (r : R) → 𝓤 ̇
T {_}{R} I J r = Σ i ꞉ R , Σ j ꞉ R , (i ∈ I) × (j ∈ J) × (r ＝ i +ᴿ j)

_+ᴵ_ : {R : 𝓤 ̇ } {{_ : Ring R}} → (I J : 𝓟 R) → 𝓟 R
_+ᴵ_ {_}{R} I J r = ∥ T I J r ∥ , ∥∥-is-prop

使用 propositional truncation ∥_∥ 來表示「存在某種分解」。下面開始證明

proposition-8 : {R : 𝓤 ̇ } {{_ : Ring R}} {I J : 𝓟 R} → IsIdeal I → IsIdeal J → IsIdeal (I +ᴵ J)
proposition-8 {_}{R}{I}{J} I-is-ideal J-is-ideal = main
  where
  open IsIdeal
  main : IsIdeal (I +ᴵ J)
  main .close-+ {i1}{i2} = ∥∥-rec₂ ∥∥-is-prop helper
    where
    helper : T I J i1 → T I J i2 → ∥ T I J (i1 +ᴿ i2) ∥
    helper (a1 , a2 , a1∈I , a2∈J , i=a1+a2) (b1 , b2 , b1∈I , b2∈J , j=b1+b2) = ∣ a1 +ᴿ b1 , a2 +ᴿ b2 , I-is-ideal .close-+ a1∈I b1∈I , J-is-ideal .close-+ a2∈J b2∈J , res ∣
      where
      res : i1 +ᴿ i2 ＝ (a1 +ᴿ b1) +ᴿ (a2 +ᴿ b2)
      res = i1 +ᴿ i2                 ＝⟨ ap (_+ᴿ i2) i=a1+a2 ⟩
            (a1 +ᴿ a2) +ᴿ i2         ＝⟨ ap (a1 +ᴿ a2 +ᴿ_) j=b1+b2 ⟩
            (a1 +ᴿ a2) +ᴿ (b1 +ᴿ b2) ＝⟨ +-assoc (a1 +ᴿ a2) b1 b2 ⁻¹ ⟩
            (a1 +ᴿ a2 +ᴿ b1) +ᴿ b2   ＝⟨ ap (_+ᴿ b2) (+-assoc a1 a2 b1) ⟩
            (a1 +ᴿ (a2 +ᴿ b1)) +ᴿ b2 ＝⟨ ap (λ - → a1 +ᴿ - +ᴿ b2) (+-comm a2 b1) ⟩
            (a1 +ᴿ (b1 +ᴿ a2)) +ᴿ b2 ＝⟨ ap (_+ᴿ b2) (+-assoc a1 b1 a2 ⁻¹) ⟩
            (a1 +ᴿ b1 +ᴿ a2) +ᴿ b2   ＝⟨ +-assoc (a1 +ᴿ b1) a2 b2 ⟩
            (a1 +ᴿ b1) +ᴿ (a2 +ᴿ b2) ∎
  main .close-neg {i} = ∥∥-rec ∥∥-is-prop helper
    where
    helper : T I J i → ∥ T I J (- i) ∥
    helper (a , b , a∈I , b∈J , i=a+b) = ∣ - a , - b , (I-is-ideal .close-neg a∈I , J-is-ideal .close-neg b∈J , res) ∣
      where
      P : ((- a) +ᴿ (- b)) +ᴿ (a +ᴿ b) ＝ 0r
      P = ((- a) +ᴿ (- b)) +ᴿ (a +ᴿ b) ＝⟨ ap (_+ᴿ (a +ᴿ b)) (+-comm (- a) (- b)) ⟩
          ((- b) +ᴿ (- a)) +ᴿ (a +ᴿ b) ＝⟨ +-assoc (- b) (- a) (a +ᴿ b) ⟩
          (- b) +ᴿ ((- a) +ᴿ (a +ᴿ b)) ＝⟨ ap ((- b) +ᴿ_) (+-assoc (- a) a b ⁻¹) ⟩
          (- b) +ᴿ ((- a) +ᴿ a +ᴿ b)   ＝⟨ ap (- b +ᴿ_) (ap (_+ᴿ b) ((+-comm (- a) a) ∙ cancel)) ⟩
          (- b) +ᴿ (0r +ᴿ b)           ＝⟨ ap (- b +ᴿ_) (+-neuL b) ⟩
          (- b) +ᴿ b                   ＝⟨ ((+-comm (- b) b) ∙ cancel) ⟩
          0r ∎
      Q : - (a +ᴿ b) +ᴿ (a +ᴿ b) ＝ 0r
      Q = - (a +ᴿ b) +ᴿ (a +ᴿ b) ＝⟨ +-comm (- (a +ᴿ b)) (a +ᴿ b) ⟩
          (a +ᴿ b) +ᴿ - (a +ᴿ b) ＝⟨ cancel ⟩
          0r ∎
      res : - i ＝ (- a) +ᴿ (- b)
      res =
        - i        ＝⟨ ap -_ i=a+b ⟩
        - (a +ᴿ b) ＝⟨ ring-cancel-right (Q ∙ P ⁻¹) ⟩
        (- a) +ᴿ (- b) ∎
  main .closeL r {i} = ∥∥-rec ∥∥-is-prop helper
    where
    helper : T I J i → ∥ T I J (r · i) ∥
    helper (a , b , a∈I , b∈J , i=a+b) = ∣ r · a , r · b , I-is-ideal .closeL r a∈I , J-is-ideal .closeL r b∈J , res ∣
      where
      res : r · i ＝ r · a +ᴿ r · b
      res = r · i        ＝⟨ ap (r ·_) i=a+b ⟩
            r · (a +ᴿ b) ＝⟨ distribR ⟩
            r · a +ᴿ r · b ∎
  main .closeR r {i} = ∥∥-rec ∥∥-is-prop helper
    where
    helper : T I J i → ∥ T I J (i · r) ∥
    helper (a , b , a∈I , b∈J , i=a+b) = ∣ a · r , b · r , I-is-ideal .closeR r a∈I , J-is-ideal .closeR r b∈J , res ∣
      where
      res : i · r ＝ a · r +ᴿ b · r
      res = i · r        ＝⟨ ap (_· r) i=a+b ⟩
            (a +ᴿ b) · r ＝⟨ distribL ⟩
            a · r +ᴿ b · r ∎