module ring-0000 where

open import MLTT.Spartan
open import UF.Sets

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

    _⊕_ : R → R → R
    𝟘R : R
    ⊕-assoc : associative _⊕_
    0l-neu : left-neutral 𝟘R _⊕_
    0r-neu : right-neutral 𝟘R _⊕_
    -_ : R → R
    cancel : {x : R} → (- x ⊕ x ＝ 𝟘R) × (x ⊕ - x ＝ 𝟘R)
    ⊕-comm : {a b : R} → a ⊕ b ＝ b ⊕ a

    _⊗_ : R → R → R
    ⊗-assoc : associative _⊗_

    𝟙R : R
    1l-neu : left-neutral 𝟙R _⊗_
    1r-neu : right-neutral 𝟙R _⊗_

    distrib1 : {r s t : R} → (r ⊕ s) ⊗ t ＝ (r ⊗ t) ⊕ (s ⊗ t)
    distrib2 : {r s t : R} → t ⊗ (r ⊕ s) ＝ (t ⊗ r) ⊕ (t ⊗ s)

  infixl  _⊕_
  infixl  _⊗_
  infixl  -_

下面這個命題是因為 (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             ＝⟨ 0r-neu s ⁻¹ ⟩
  s ⊕ 𝟘R        ＝⟨ ap (s ⊕_) (cancel .pr₂ ⁻¹) ⟩
  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 .pr₂) ⟩
  t ⊕ 𝟘R        ＝⟨ 0r-neu t ⟩
  t ∎

module ring-0001 where

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

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

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

trivial-ring : Ring (𝟙 {𝓤})
trivial-ring .size = props-are-sets 𝟙-is-prop
trivial-ring ._⊕_ _ _ = ⋆
trivial-ring .𝟘R = ⋆
trivial-ring .⊕-assoc = λ x y z → refl
trivial-ring .0l-neu = λ x → refl
trivial-ring .0r-neu = λ x → refl
trivial-ring .-_ _ = ⋆
trivial-ring .cancel = refl , refl
trivial-ring .⊕-comm = refl
trivial-ring ._⊗_ _ _ = ⋆
trivial-ring .⊗-assoc = λ x y z → refl
trivial-ring .𝟙R = ⋆
trivial-ring .1l-neu = λ x → refl
trivial-ring .1r-neu = λ x → refl
trivial-ring .distrib1 = refl
trivial-ring .distrib2 = refl

module ring-0002 where

open import MLTT.Spartan

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

lemma-1 : {R : 𝓤 ̇ } {{_ : Ring R}} → (r : R) → (r ⊗ 𝟘R ＝ 𝟘R) × (𝟘R ⊗ r ＝ 𝟘R)
lemma-1 r = (ring-cancel-right I ⁻¹) , (ring-cancel-right II ⁻¹)
  where
  I : 𝟘R ⊕ r ⊗ 𝟘R ＝ r ⊗ 𝟘R ⊕ r ⊗ 𝟘R
  I =
    𝟘R ⊕ r ⊗ 𝟘R   ＝⟨ 0l-neu (r ⊗ 𝟘R) ⟩
    r ⊗ 𝟘R        ＝⟨ ap (r ⊗_) (0l-neu 𝟘R ⁻¹) ⟩
    r ⊗ (𝟘R ⊕ 𝟘R) ＝⟨ distrib2 ⟩
    r ⊗ 𝟘R ⊕ r ⊗ 𝟘R ∎

  II : 𝟘R ⊕ 𝟘R ⊗ r ＝ 𝟘R ⊗ r ⊕ 𝟘R ⊗ r
  II =
    𝟘R ⊕ 𝟘R ⊗ r   ＝⟨ 0l-neu (𝟘R ⊗ r) ⟩
    𝟘R ⊗ r        ＝⟨ ap (_⊗ r) (0l-neu 𝟘R ⁻¹) ⟩
    (𝟘R ⊕ 𝟘R) ⊗ r ＝⟨ distrib1 ⟩
    𝟘R ⊗ r ⊕ 𝟘R ⊗ r ∎

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 ＝ 𝟘R
  I = cancel .pr₁
  II : x ⊕ - x ＝ 𝟘R
  II = cancel .pr₂

或是更重要的 −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 ＝ 𝟘R
  I = (- (a ⊗ b)) ⊕ a ⊗ b ＝⟨ cancel .pr₁ ⟩
      𝟘R ∎
  II : (- a ⊗ b) ⊕ a ⊗ b ＝ 𝟘R
  II = (- a ⊗ b) ⊕ a ⊗ b ＝⟨ distrib1 ⁻¹ ⟩
      (- a ⊕ a) ⊗ b      ＝⟨ ap (_⊗ b) (cancel .pr₁) ⟩
      𝟘R ⊗ b             ＝⟨ lemma-1 b .pr₂ ⟩
      𝟘R ∎
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 ＝ 𝟘R
  I = cancel .pr₁
  II : (a ⊗ - b) ⊕ a ⊗ b ＝ 𝟘R
  II = (a ⊗ - b) ⊕ a ⊗ b ＝⟨ distrib2 ⁻¹ ⟩
      a ⊗ (- b ⊕ b)      ＝⟨ ap (a ⊗_) (cancel .pr₁) ⟩
      a ⊗ 𝟘R             ＝⟨ lemma-1 a .pr₁ ⟩
      𝟘R ∎

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 ∎

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 ＝ 𝟘R → b ＝ 𝟘R)

$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

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

proposition-3 : {R : 𝓤 ̇ } {{_ : Ring R}} {a : R} →
  (NonZeroDivisor a → left-cancellable (left-action a)) × (left-cancellable (left-action a) → NonZeroDivisor 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) ＝ 𝟘R
    I =
      left-action a (x ⊕ - y) ＝⟨by-definition⟩
      a ⊗ (x ⊕ - y)           ＝⟨ distrib2 ⟩
      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 .pr₂ ⟩
      𝟘R ∎
    II : x ⊕ - y ＝ 𝟘R
    II = is-not-zd (x ⊕ - y) I
    III : y ⊕ - y ＝ 𝟘R
    III = cancel .pr₂
  only-if : left-cancellable (left-action a) → NonZeroDivisor a
  only-if inj b ab=0 = inj I
    where
    I : a ⊗ b ＝ a ⊗ 𝟘R
    I = left-action a b ＝⟨by-definition⟩
        a ⊗ b           ＝⟨ ab=0 ⟩
        𝟘R              ＝⟨ lemma-1 a .pr₁ ⁻¹ ⟩
        a ⊗ 𝟘R          ＝⟨by-definition⟩
        left-action a 𝟘R ∎