{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (RawMagma)
open import Algebra.Morphism.Structures using (IsMagmaMonomorphism)
module Algebra.Morphism.MagmaMonomorphism
{a b ℓ₁ ℓ₂} {M₁ : RawMagma a ℓ₁} {M₂ : RawMagma b ℓ₂} {⟦_⟧}
(isMagmaMonomorphism : IsMagmaMonomorphism M₁ M₂ ⟦_⟧)
where
open IsMagmaMonomorphism isMagmaMonomorphism
open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
open import Algebra.Structures
using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma)
open import Algebra.Definitions
using (Congruent₂; Associative; Commutative; Idempotent ; Selective
; LeftCancellative; RightCancellative; Cancellative)
open import Data.Product.Base using (map)
open import Data.Sum.Base using (inj₁; inj₂)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
open import Relation.Binary.Core using (Rel)
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
open ≈-Reasoning setoid
cong : Congruent₂ _≈₁_ _∙_
cong {x} {y} {u} {v} x≈y u≈v = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1663}{\htmlId{1711}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{1713}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1671}{\htmlId{1715}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$ ≈⟨ homo x u ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1663}{\htmlId{1745}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1671}{\htmlId{1753}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1667}{\htmlId{1805}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1675}{\htmlId{1813}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ≈⟨ homo y v ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1667}{\htmlId{1838}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{1840}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1675}{\htmlId{1842}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ∎)
assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
assoc assoc x y z = injective (begin
$\begin{pmatrix} \,\htmlId{1954}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{1955}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{1957}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{1959}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{1960}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{1962}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{1964}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ homo (x ∙ y) z ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2004}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2006}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2008}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2016}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (homo x y) refl ⟩
($\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2063}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2071}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2080}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ assoc $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2097}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2103}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2109}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2121}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ($\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2130}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2138}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$) ≈⟨ ◦-cong refl (homo y z) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2178}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2186}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2188}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2190}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ homo x (y ∙ z) ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#1923}{\htmlId{2227}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2229}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{2231}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.MagmaMonomorphism.html#1925}{\htmlId{2232}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2234}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#1927}{\htmlId{2236}{\htmlClass{Bound}{\text{z}}}}\,\,\htmlId{2237}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ∎)
comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
comm comm x y = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2319}{\htmlId{2348}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2350}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2321}{\htmlId{2352}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ homo x y ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2319}{\htmlId{2382}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2321}{\htmlId{2390}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ comm $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2319}{\htmlId{2406}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2321}{\htmlId{2412}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2321}{\htmlId{2424}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2319}{\htmlId{2432}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo y x ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2321}{\htmlId{2457}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2459}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2319}{\htmlId{2461}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
idem idem x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2564}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2566}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2568}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo x x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2596}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2604}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ idem $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2618}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2537}{\htmlId{2630}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
sel sel x y with sel $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2704}{\htmlId{2719}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#2706}{\htmlId{2725}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$
... | inj₁ x◦y≈x = inj₁ (injective (begin
$\begin{pmatrix} \,\htmlId{2779}{\htmlClass{Bound}{\text{x}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2781}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{2783}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$ ≈⟨ homo x y ⟩
$\begin{pmatrix} \,\htmlId{2812}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\htmlId{2820}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$ ≈⟨ x◦y≈x ⟩
$\begin{pmatrix} \,\htmlId{2842}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$ ∎))
... | inj₂ x◦y≈y = inj₂ (injective (begin
$\begin{pmatrix} \,\htmlId{2909}{\htmlClass{Bound}{\text{x}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{2911}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{2913}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$ ≈⟨ homo x y ⟩
$\begin{pmatrix} \,\htmlId{2942}{\htmlClass{Bound}{\text{x}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\htmlId{2950}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$ ≈⟨ x◦y≈y ⟩
$\begin{pmatrix} \,\htmlId{2972}{\htmlClass{Bound}{\text{y}}}\, \end{pmatrix}$ ∎))
cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3074}{\htmlId{3111}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3076}{\htmlId{3117}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3078}{\htmlId{3123}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3074}{\htmlId{3140}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3076}{\htmlId{3148}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ homo x y ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3074}{\htmlId{3173}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{3175}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3076}{\htmlId{3177}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3074}{\htmlId{3214}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{3216}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3078}{\htmlId{3218}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ≈⟨ homo x z ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3074}{\htmlId{3248}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3078}{\htmlId{3256}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ∎))
cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3352}{\htmlId{3389}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3354}{\htmlId{3395}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3356}{\htmlId{3401}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3354}{\htmlId{3418}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3352}{\htmlId{3426}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo y x ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3354}{\htmlId{3451}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{3453}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3352}{\htmlId{3455}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ⟦⟧-cong y∙x≈z∙x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3356}{\htmlId{3492}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#819}{\htmlId{3494}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MagmaMonomorphism.html#3352}{\htmlId{3496}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo z x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3356}{\htmlId{3526}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MagmaMonomorphism.html#3352}{\htmlId{3534}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎))
cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_
cancel = map cancelˡ cancelʳ
isMagma : IsMagma _≈₂_ _◦_ → IsMagma _≈₁_ _∙_
isMagma isMagma = record
{ isEquivalence = RelMorphism.isEquivalence M.isEquivalence
; ∙-cong = cong isMagma
} where module M = IsMagma isMagma
isSemigroup : IsSemigroup _≈₂_ _◦_ → IsSemigroup _≈₁_ _∙_
isSemigroup isSemigroup = record
{ isMagma = isMagma S.isMagma
; assoc = assoc S.isMagma S.assoc
} where module S = IsSemigroup isSemigroup
isBand : IsBand _≈₂_ _◦_ → IsBand _≈₁_ _∙_
isBand isBand = record
{ isSemigroup = isSemigroup B.isSemigroup
; idem = idem B.isMagma B.idem
} where module B = IsBand isBand
isSelectiveMagma : IsSelectiveMagma _≈₂_ _◦_ → IsSelectiveMagma _≈₁_ _∙_
isSelectiveMagma isSelMagma = record
{ isMagma = isMagma S.isMagma
; sel = sel S.isMagma S.sel
} where module S = IsSelectiveMagma isSelMagma