{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (RawMonoid)
open import Algebra.Morphism.Structures using (IsMonoidMonomorphism)
module Algebra.Morphism.MonoidMonomorphism
{a b ℓ₁ ℓ₂} {M₁ : RawMonoid a ℓ₁} {M₂ : RawMonoid b ℓ₂} {⟦_⟧}
(isMonoidMonomorphism : IsMonoidMonomorphism M₁ M₂ ⟦_⟧)
where
open IsMonoidMonomorphism isMonoidMonomorphism
open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
open import Algebra.Definitions
using (Identity; Zero; LeftIdentity; RightIdentity; LeftZero; RightZero)
open import Algebra.Structures
using (IsMagma; IsMonoid; IsCommutativeMonoid)
open import Data.Product.Base using (map)
open import Relation.Binary.Core using (Rel)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Algebra.Morphism.MagmaMonomorphism
isMagmaMonomorphism public
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
open ≈-Reasoning setoid
identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
identityˡ idˡ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{1777}{\htmlClass{Function}{\text{ε₁}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#830}{\htmlId{1780}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#1750}{\htmlId{1782}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo ε₁ x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{1812}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1750}{\htmlId{1821}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong ε-homo refl ⟩
ε₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1750}{\htmlId{1861}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ idˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1750}{\htmlId{1879}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1750}{\htmlId{1891}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
identityʳ idʳ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1993}{\htmlId{2020}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#830}{\htmlId{2022}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2024}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ≈⟨ homo x ε₁ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1993}{\htmlId{2055}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2063}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl ε-homo ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1993}{\htmlId{2099}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ε₂ ≈⟨ idʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1993}{\htmlId{2122}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#1993}{\htmlId{2134}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
identity : Identity _≈₂_ ε₂ _◦_ → Identity _≈₁_ ε₁ _∙_
identity = map identityˡ identityʳ
zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
zeroˡ zeˡ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2340}{\htmlClass{Function}{\text{ε₁}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#830}{\htmlId{2343}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#2313}{\htmlId{2345}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ homo ε₁ x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2375}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2313}{\htmlId{2384}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong ε-homo refl ⟩
ε₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2313}{\htmlId{2426}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ zeˡ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2313}{\htmlId{2442}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
ε₂ ≈⟨ ε-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2485}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ∎)
zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
zeroʳ zeʳ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2570}{\htmlId{2597}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#830}{\htmlId{2599}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2601}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ≈⟨ homo x ε₁ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2570}{\htmlId{2632}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2640}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl ε-homo ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2570}{\htmlId{2676}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ ε₂ ≈⟨ zeʳ $\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#2570}{\htmlId{2699}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
ε₂ ≈⟨ ε-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.MonoidMonomorphism.html#840}{\htmlId{2742}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ∎)
zero : Zero _≈₂_ ε₂ _◦_ → Zero _≈₁_ ε₁ _∙_
zero = map zeroˡ zeroʳ
isMonoid : IsMonoid _≈₂_ _◦_ ε₂ → IsMonoid _≈₁_ _∙_ ε₁
isMonoid isMonoid = record
{ isSemigroup = isSemigroup M.isSemigroup
; identity = identity M.isMagma M.identity
} where module M = IsMonoid isMonoid
isCommutativeMonoid : IsCommutativeMonoid _≈₂_ _◦_ ε₂ →
IsCommutativeMonoid _≈₁_ _∙_ ε₁
isCommutativeMonoid isCommMonoid = record
{ isMonoid = isMonoid C.isMonoid
; comm = comm C.isMagma C.comm
} where module C = IsCommutativeMonoid isCommMonoid