------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between ring-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles
open import Algebra.Morphism.Structures
import Algebra.Morphism.GroupMonomorphism  as GroupMonomorphism
import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism
open import Relation.Binary.Core

module Algebra.Morphism.RingMonomorphism
  {a b ℓ₁ ℓ₂} {R₁ : RawRing a ℓ₁} {R₂ : RawRing b ℓ₂} {⟦_⟧}
  (isRingMonomorphism : IsRingMonomorphism R₁ R₂ ⟦_⟧)
  where

open IsRingMonomorphism isRingMonomorphism
open RawRing R₁ renaming (Carrier to A; _≈_ to _≈₁_)
open RawRing R₂ renaming
  ( Carrier to B; _≈_ to _≈₂_; _+_ to _⊕_
  ; _*_ to _⊛_; 1# to 1#₂; 0# to 0#₂; -_ to ⊝_)

open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product.Base using (proj₁; proj₂; _,_)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

------------------------------------------------------------------------
-- Re-export all properties of group and monoid monomorphisms

open GroupMonomorphism +-isGroupMonomorphism public
  renaming
  ( assoc   to +-assoc
  ; comm    to +-comm
  ; cong    to +-cong
  ; idem    to +-idem
  ; sel     to +-sel
  ; ⁻¹-cong to neg-cong

  ; identity to +-identity; identityˡ to +-identityˡ; identityʳ to +-identityʳ
  ; cancel   to +-cancel;   cancelˡ   to +-cancelˡ;   cancelʳ   to +-cancelʳ
  ; zero     to +-zero;     zeroˡ     to +-zeroˡ;     zeroʳ     to +-zeroʳ

  ; isMagma             to +-isMagma
  ; isSemigroup         to +-isSemigroup
  ; isMonoid            to +-isMonoid
  ; isSelectiveMagma    to +-isSelectiveMagma
  ; isBand              to +-isBand
  ; isCommutativeMonoid to +-isCommutativeMonoid
  )

open MonoidMonomorphism *-isMonoidMonomorphism public
  renaming
  ( assoc to *-assoc
  ; comm  to *-comm
  ; cong  to *-cong
  ; idem  to *-idem
  ; sel   to *-sel

  ; identity to *-identity; identityˡ to *-identityˡ; identityʳ to *-identityʳ
  ; cancel   to *-cancel;   cancelˡ   to *-cancelˡ;   cancelʳ   to *-cancelʳ
  ; zero     to *-zero;     zeroˡ     to *-zeroˡ;     zeroʳ     to *-zeroʳ

  ; isMagma             to *-isMagma
  ; isSemigroup         to *-isSemigroup
  ; isMonoid            to *-isMonoid
  ; isSelectiveMagma    to *-isSelectiveMagma
  ; isBand              to *-isBand
  ; isCommutativeMonoid to *-isCommutativeMonoid
  )

------------------------------------------------------------------------
-- Properties

module _ (+-isGroup : IsGroup _≈₂_ _⊕_ 0#₂ ⊝_)
         (*-isMagma : IsMagma _≈₂_ _⊛_) where

  open IsGroup +-isGroup hiding (setoid; refl; sym)
  open IsMagma *-isMagma renaming (∙-cong to ◦-cong)
  open ≈-Reasoning setoid

  distribˡ : _DistributesOverˡ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverˡ_ _≈₁_ _*_ _+_
  distribˡ distribˡ x y z = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3123}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3125}{\htmlClass{Function Operator}{\text{*}}}}\, (\,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3128}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3130}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3132}{\htmlClass{Bound}{\text{z}}}}\,) \end{pmatrix}$               ≈⟨ *-homo x (y + z) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3179}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3187}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3189}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3191}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$             ≈⟨ ◦-cong refl (+-homo y z) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3243}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3252}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3260}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$)       ≈⟨ distribˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3285}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3291}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3297}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3309}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3317}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3325}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3333}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ ∙-cong (*-homo x y) (*-homo x z) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3381}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3383}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3385}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3393}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3395}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3397}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$         ≈⟨ +-homo (x * y) (x * z) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3443}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3445}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3094}{\htmlId{3447}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3449}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3092}{\htmlId{3451}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3453}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3096}{\htmlId{3455}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ∎)

  distribʳ : _DistributesOverʳ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverʳ_ _≈₁_ _*_ _+_
  distribʳ distribˡ x y z = injective (begin
    $\begin{pmatrix} (\,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3594}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3596}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3598}{\htmlClass{Bound}{\text{z}}}}\,) \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3601}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3603}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$               ≈⟨ *-homo (y + z) x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3649}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3651}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3653}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3661}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$             ≈⟨ ◦-cong (+-homo y z) refl ⟩
    ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3714}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3722}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$) ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3731}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$       ≈⟨ distribˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3755}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3761}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3767}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3779}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3787}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3795}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3803}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ∙-cong (*-homo y x) (*-homo z x) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3851}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3853}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3855}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3863}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3865}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3867}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$         ≈⟨ +-homo (y * x) (z * x) ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3564}{\htmlId{3913}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3915}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3917}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5442}{\htmlId{3919}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3566}{\htmlId{3921}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{3923}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3562}{\htmlId{3925}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)

  distrib : _DistributesOver_ _≈₂_ _⊛_ _⊕_ → _DistributesOver_ _≈₁_ _*_ _+_
  distrib distrib = distribˡ (proj₁ distrib) , distribʳ (proj₂ distrib)

  zeroˡ : LeftZero _≈₂_ 0#₂ _⊛_ → LeftZero _≈₁_ 0# _*_
  zeroˡ zeroˡ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4178}{\htmlClass{Function}{\text{0#}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{4181}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4151}{\htmlId{4183}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$     ≈⟨ *-homo 0# x ⟩
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4214}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4151}{\htmlId{4223}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong 0#-homo refl ⟩
    0#₂ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4151}{\htmlId{4264}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$    ≈⟨ zeroˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4151}{\htmlId{4282}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    0#₂            ≈⟨ 0#-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4326}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$         ∎)

  zeroʳ : RightZero _≈₂_ 0#₂ _⊛_ → RightZero _≈₁_ 0# _*_
  zeroʳ zeroʳ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4414}{\htmlId{4441}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{4443}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4445}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$     ≈⟨ *-homo x 0# ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4414}{\htmlId{4477}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4485}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl 0#-homo ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4414}{\htmlId{4521}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ 0#₂    ≈⟨ zeroʳ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4414}{\htmlId{4545}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    0#₂            ≈⟨ 0#-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5520}{\htmlId{4589}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$         ∎)

  zero : Zero _≈₂_ 0#₂ _⊛_ → Zero _≈₁_ 0# _*_
  zero zero = zeroˡ (proj₁ zero) , zeroʳ (proj₂ zero)

  neg-distribˡ-* : (∀ x y → (⊝ (x ⊛ y)) ≈₂ ((⊝ x) ⊛ y)) → (∀ x y → (- (x * y)) ≈₁ ((- x) * y))
  neg-distribˡ-* neg-distribˡ-* x y = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{4863}{\htmlClass{Function Operator}{\text{-}}}}\, (\,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{4866}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{4868}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{4870}{\htmlClass{Bound}{\text{y}}}}\,) \end{pmatrix}$     ≈⟨ -‿homo (x * y) ⟩
    ⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{4907}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{4909}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{4911}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$       ≈⟨ ⁻¹-cong (*-homo x y) ⟩
    ⊝ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{4956}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{4964}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ≈⟨ neg-distribˡ-* $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{4989}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{4995}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    ⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{5009}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{5017}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$   ≈⟨ ◦-cong (sym (-‿homo x)) refl ⟩
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{5063}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{5065}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{5073}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$   ≈⟨ sym (*-homo (- x) y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{5111}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4834}{\htmlId{5113}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{5115}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4836}{\htmlId{5117}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$       ∎)

  neg-distribʳ-* : (∀ x y → (⊝ (x ⊛ y)) ≈₂ (x ⊛ (⊝ y))) → (∀ x y → (- (x * y)) ≈₁ (x * (- y)))
  neg-distribʳ-* neg-distribʳ-* x y = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{5287}{\htmlClass{Function Operator}{\text{-}}}}\, (\,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5290}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{5292}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5294}{\htmlClass{Bound}{\text{y}}}}\,) \end{pmatrix}$     ≈⟨ -‿homo (x * y) ⟩
    ⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5331}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{5333}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5335}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$       ≈⟨ ⁻¹-cong (*-homo x y) ⟩
    ⊝ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5380}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5388}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ≈⟨ neg-distribʳ-* $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5413}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5419}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5431}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ ⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5441}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$   ≈⟨ ◦-cong refl (sym (-‿homo y)) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5487}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{5495}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5497}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$   ≈⟨ sym (*-homo x (- y)) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5258}{\htmlId{5535}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5468}{\htmlId{5537}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Bundles.Raw.html#5494}{\htmlId{5539}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5260}{\htmlId{5541}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$       ∎)

isRing : IsRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ → IsRing _≈₁_ _+_ _*_ -_ 0# 1#
isRing isRing = record
  { +-isAbelianGroup = isAbelianGroup R.+-isAbelianGroup
  ; *-cong           = *-cong R.*-isMagma
  ; *-assoc          = *-assoc R.*-isMagma R.*-assoc
  ; *-identity       = *-identity R.*-isMagma R.*-identity
  ; distrib          = distrib R.+-isGroup R.*-isMagma R.distrib
  } where module R = IsRing isRing

isCommutativeRing : IsCommutativeRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ →
                    IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1#
isCommutativeRing isCommRing = record
  { isRing = isRing C.isRing
  ; *-comm = *-comm C.*-isMagma C.*-comm
  } where module C = IsCommutativeRing isCommRing