Β« Home

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
    𝟘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 30 _βŠ•_
  infixl 40 _βŠ—_
  infixl 50 -_

    δΈ‹ι’ι€™ε€‹ε‘½ι‘Œζ˜―ε› η‚Ί (R,β€†βŠ•, 0R) 也可δ»₯ηœ‹ζˆδΈ€ε€‹ 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 ∎