------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between bisemimodules
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
open import Algebra.Module.Bundles.Raw using (RawBisemimodule)
open import Algebra.Module.Morphism.Structures using (IsBisemimoduleMonomorphism)
module Algebra.Module.Morphism.BisemimoduleMonomorphism
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧}
(isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
where
open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
private
module M = RawBisemimodule M
module N = RawBisemimodule N
open import Algebra.Bundles using (Semiring)
open import Algebra.Core using (Op₂)
import Algebra.Module.Definitions.Bi as BiDefs using (Associative)
import Algebra.Module.Definitions.Left as LeftDefs using (LeftCongruent)
import Algebra.Module.Definitions.Right as RightDefs using (RightCongruent)
open import Algebra.Module.Structures using (IsBisemimodule)
open import Algebra.Structures using (IsMagma; IsSemiring)
open import Function.Base using (flip; _$_)
open import Relation.Binary.Core using (Rel)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
------------------------------------------------------------------------
-- Re-exports
open import Algebra.Morphism.MonoidMonomorphism
+ᴹ-isMonoidMonomorphism public
using ()
renaming
( cong to +ᴹ-cong
; assoc to +ᴹ-assoc
; comm to +ᴹ-comm
; identityˡ to +ᴹ-identityˡ
; identityʳ to +ᴹ-identityʳ
; identity to +ᴹ-identity
; isMagma to +ᴹ-isMagma
; isSemigroup to +ᴹ-isSemigroup
; isMonoid to +ᴹ-isMonoid
; isCommutativeMonoid to +ᴹ-isCommutativeMonoid
)
open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism
isLeftSemimoduleMonomorphism public
using
( *ₗ-cong
; *ₗ-zeroˡ
; *ₗ-distribʳ
; *ₗ-identityˡ
; *ₗ-assoc
; *ₗ-zeroʳ
; *ₗ-distribˡ
; isLeftSemimodule
)
open import Algebra.Module.Morphism.RightSemimoduleMonomorphism
isRightSemimoduleMonomorphism public
using
( *ᵣ-cong
; *ᵣ-zeroʳ
; *ᵣ-distribˡ
; *ᵣ-identityʳ
; *ᵣ-assoc
; *ᵣ-zeroˡ
; *ᵣ-distribʳ
; isRightSemimodule
)
------------------------------------------------------------------------
-- Properties
module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where
open IsMagma +ᴹ-isMagma
using (setoid)
renaming (∙-cong to +ᴹ-cong)
open SetoidReasoning setoid
private
module MDefs = BiDefs R S M._≈ᴹ_
module NDefs = BiDefs R S N._≈ᴹ_
module LDefs = LeftDefs R N._≈ᴹ_
module RDefs = RightDefs S N._≈ᴹ_
*ₗ-*ᵣ-assoc
: LDefs.LeftCongruent N._*ₗ_ → RDefs.RightCongruent N._*ᵣ_
→ NDefs.Associative N._*ₗ_ N._*ᵣ_
→ MDefs.Associative M._*ₗ_ M._*ᵣ_
*ₗ-*ᵣ-assoc *ₗ-congˡ *ᵣ-congʳ *ₗ-*ᵣ-assoc x m y = injective $ begin
⟦ (x M.*ₗ m) M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (x M.*ₗ m) ⟩
⟦ x M.*ₗ m ⟧ N.*ᵣ y ≈⟨ *ᵣ-congʳ (*ₗ-homo x m) ⟩
(x N.*ₗ ⟦ m ⟧) N.*ᵣ y ≈⟨ *ₗ-*ᵣ-assoc x ⟦ m ⟧ y ⟩
x N.*ₗ (⟦ m ⟧ N.*ᵣ y) ≈˘⟨ *ₗ-congˡ (*ᵣ-homo y m) ⟩
x N.*ₗ ⟦ m M.*ᵣ y ⟧ ≈˘⟨ *ₗ-homo x (m M.*ᵣ y) ⟩
⟦ x M.*ₗ (m M.*ᵣ y) ⟧ ∎
------------------------------------------------------------------------
-- Structures
module _
{ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ 0r 1r}
{ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ 0s 1s}
(R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r)
(S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s)
where
private
R-semiring : Semiring _ _
R-semiring = record { isSemiring = R-isSemiring }
S-semiring : Semiring _ _
S-semiring = record { isSemiring = S-isSemiring }
isBisemimodule
: IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
→ IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
isBisemimodule isBisemimodule = record
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid
; isPreleftSemimodule = record
{ *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong
; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ
; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ
; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ
; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc
; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ
; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ
}
; isPrerightSemimodule = record
{ *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong
; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ
; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ
; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ
; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc
; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ
; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ
}
; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc
}
where
module NN = IsBisemimodule isBisemimodule
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