{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (RawRing)
open import Algebra.Morphism.Structures using (IsRingMonomorphism)
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 ⊝_)
import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism
import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism
open import Relation.Binary.Core using (Rel)
open import Algebra.Definitions
using (_DistributesOverˡ_; _DistributesOverʳ_ ; _DistributesOver_
; LeftZero; RightZero; Zero)
open import Algebra.Structures
using (IsRing; IsCommutativeRing; IsGroup; IsMagma)
open import Data.Product.Base using (proj₁; proj₂; _,_)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
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
)
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#3306}{\htmlId{3337}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3339}{\htmlClass{Function Operator}{\text{*}}}}\, \,\htmlId{3341}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3342}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{3344}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3346}{\htmlClass{Bound}{\text{z}}}}\,\,\htmlId{3347}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ≈⟨ *-homo x (y + z) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3393}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3401}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{3403}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3405}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl (+-homo y z) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3457}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3466}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3474}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$) ≈⟨ distribˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3499}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3505}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3511}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3523}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3531}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3539}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3547}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ ∙-cong (*-homo x y) (*-homo x z) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3595}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3597}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3599}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3607}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3609}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3611}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ +-homo (x * y) (x * z) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3657}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3659}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3308}{\htmlId{3661}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{3663}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3306}{\htmlId{3665}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3667}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3310}{\htmlId{3669}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ∎)
distribʳ : _DistributesOverʳ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverʳ_ _≈₁_ _*_ _+_
distribʳ distribˡ x y z = injective (begin
$\begin{pmatrix} \,\htmlId{3807}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{3808}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{3810}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{3812}{\htmlClass{Bound}{\text{z}}}}\,\,\htmlId{3813}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{3815}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{3817}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ *-homo (y + z) x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{3863}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{3865}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{3867}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{3875}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (+-homo y z) refl ⟩
($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{3928}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{3936}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$) ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{3945}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ distribˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{3969}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{3975}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{3981}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{3993}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4001}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{4009}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4017}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ∙-cong (*-homo y x) (*-homo z x) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{4065}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4067}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4069}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊕ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{4077}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4079}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4081}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ +-homo (y * x) (z * x) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#3778}{\htmlId{4127}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4129}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4131}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5405}{\htmlId{4133}{\htmlClass{Function Operator}{\text{+}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3780}{\htmlId{4135}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4137}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#3776}{\htmlId{4139}{\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#5483}{\htmlId{4392}{\htmlClass{Function}{\text{0#}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4395}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#4365}{\htmlId{4397}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ *-homo 0# x ⟩
$\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5483}{\htmlId{4428}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4365}{\htmlId{4437}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong 0#-homo refl ⟩
0#₂ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4365}{\htmlId{4478}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ zeroˡ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4365}{\htmlId{4496}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
0#₂ ≈⟨ 0#-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5483}{\htmlId{4540}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ∎)
zeroʳ : RightZero _≈₂_ 0#₂ _⊛_ → RightZero _≈₁_ 0# _*_
zeroʳ zeroʳ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4628}{\htmlId{4655}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{4657}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Bundles.Raw.html#5483}{\htmlId{4659}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ≈⟨ *-homo x 0# ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4628}{\htmlId{4691}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5483}{\htmlId{4699}{\htmlClass{Function}{\text{0#}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl 0#-homo ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4628}{\htmlId{4735}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ 0#₂ ≈⟨ zeroʳ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#4628}{\htmlId{4759}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
0#₂ ≈⟨ 0#-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5483}{\htmlId{4803}{\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#5457}{\htmlId{5077}{\htmlClass{Function Operator}{\text{-}}}}\, \,\htmlId{5079}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5080}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5082}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5084}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{5085}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ≈⟨ -‿homo (x * y) ⟩
⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5121}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5123}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5125}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⁻¹-cong (*-homo x y) ⟩
⊝ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5170}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5178}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ≈⟨ neg-distribˡ-* $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5203}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5209}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5223}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5231}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (sym (-‿homo x)) refl ⟩
$\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5457}{\htmlId{5277}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5279}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5287}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ sym (*-homo (- x) y) ⟩
$\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5457}{\htmlId{5325}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5048}{\htmlId{5327}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5329}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5050}{\htmlId{5331}{\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#5457}{\htmlId{5501}{\htmlClass{Function Operator}{\text{-}}}}\, \,\htmlId{5503}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5504}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5506}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5508}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{5509}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ≈⟨ -‿homo (x * y) ⟩
⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5545}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5547}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5549}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⁻¹-cong (*-homo x y) ⟩
⊝ ($\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5594}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5602}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ≈⟨ neg-distribʳ-* $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5627}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5633}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5645}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ ⊝ $\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5655}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl (sym (-‿homo y)) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5701}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊛ $\begin{pmatrix} \,\href{Algebra.Bundles.Raw.html#5457}{\htmlId{5709}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5711}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ sym (*-homo x (- y)) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.RingMonomorphism.html#5472}{\htmlId{5749}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Bundles.Raw.html#5431}{\htmlId{5751}{\htmlClass{Function Operator}{\text{*}}}}\, \,\href{Algebra.Bundles.Raw.html#5457}{\htmlId{5753}{\htmlClass{Function Operator}{\text{-}}}}\, \,\href{Algebra.Morphism.RingMonomorphism.html#5474}{\htmlId{5755}{\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