------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between magma-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 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)
------------------------------------------------------------------------
-- Properties
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
⟦ x ∙ u ⟧ ≈⟨ homo x u ⟩
⟦ x ⟧ ◦ ⟦ u ⟧ ≈⟨ ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
⟦ y ⟧ ◦ ⟦ v ⟧ ≈⟨ homo y v ⟨
⟦ y ∙ v ⟧ ∎)
assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
assoc assoc x y z = injective (begin
⟦ (x ∙ y) ∙ z ⟧ ≈⟨ homo (x ∙ y) z ⟩
⟦ x ∙ y ⟧ ◦ ⟦ z ⟧ ≈⟨ ◦-cong (homo x y) refl ⟩
(⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧ ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧) ≈⟨ ◦-cong refl (homo y z) ⟨
⟦ x ⟧ ◦ ⟦ y ∙ z ⟧ ≈⟨ homo x (y ∙ z) ⟨
⟦ x ∙ (y ∙ z) ⟧ ∎)
comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
comm comm x y = injective (begin
⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩
⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ comm ⟦ x ⟧ ⟦ y ⟧ ⟩
⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ homo y x ⟨
⟦ y ∙ x ⟧ ∎)
idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
idem idem x = injective (begin
⟦ x ∙ x ⟧ ≈⟨ homo x x ⟩
⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩
⟦ x ⟧ ∎)
sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧
... | inj₁ x◦y≈x = inj₁ (injective (begin
⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩
⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ x◦y≈x ⟩
⟦ x ⟧ ∎))
... | inj₂ x◦y≈y = inj₂ (injective (begin
⟦ x ∙ y ⟧ ≈⟨ homo x y ⟩
⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ x◦y≈y ⟩
⟦ y ⟧ ∎))
cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
⟦ x ⟧ ◦ ⟦ y ⟧ ≈⟨ homo x y ⟨
⟦ x ∙ y ⟧ ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩
⟦ x ∙ z ⟧ ≈⟨ homo x z ⟩
⟦ x ⟧ ◦ ⟦ z ⟧ ∎))
cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
⟦ y ⟧ ◦ ⟦ x ⟧ ≈⟨ homo y x ⟨
⟦ y ∙ x ⟧ ≈⟨ ⟦⟧-cong y∙x≈z∙x ⟩
⟦ z ∙ x ⟧ ≈⟨ homo z x ⟩
⟦ z ⟧ ◦ ⟦ x ⟧ ∎))
cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_
cancel = map cancelˡ cancelʳ
------------------------------------------------------------------------
-- Structures
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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4