------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a monomorphism between bimodules
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
open import Algebra.Module.Bundles.Raw using (RawBimodule)
open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
module Algebra.Module.Morphism.BimoduleMonomorphism
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBimodule R S a ℓ₁} {N : RawBimodule R S b ℓ₂} {⟦_⟧}
(isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧)
where
open IsBimoduleMonomorphism isBimoduleMonomorphism
private
module M = RawBimodule M
module N = RawBimodule N
open import Algebra.Bundles using (Ring)
open import Algebra.Module.Structures using (IsBimodule)
open import Algebra.Structures using (IsRing)
open import Relation.Binary.Core using (Rel)
------------------------------------------------------------------------
-- Re-exports
open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public
using () renaming
( inverseˡ to -ᴹ‿inverseˡ
; inverseʳ to -ᴹ‿inverseʳ
; inverse to -ᴹ‿inverse
; ⁻¹-cong to -ᴹ‿cong
; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ
; isGroup to +ᴹ-isGroup
; isAbelianGroup to +ᴹ-isAbelianGroup
)
open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public
------------------------------------------------------------------------
-- Structures
module _
{ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ -r_ 0r 1r}
{ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ -s_ 0s 1s}
(R-isRing : IsRing _≈r_ _+r_ _*r_ -r_ 0r 1r)
(S-isRing : IsRing _≈s_ _+s_ _*s_ -s_ 0s 1s)
where
private
R-ring : Ring _ _
R-ring = record { isRing = R-isRing }
S-ring : Ring _ _
S-ring = record { isRing = S-isRing }
module R = IsRing R-isRing
module S = IsRing S-isRing
isBimodule
: IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_
→ IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_
isBimodule isBimodule = record
{ isBisemimodule = isBisemimodule R.isSemiring S.isSemiring NN.isBisemimodule
; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong
; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse
}
where
module NN = IsBimodule isBimodule
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