------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a monomorphism between semimodules
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
open import Algebra.Module.Bundles.Raw using (RawSemimodule)
open import Algebra.Module.Morphism.Structures using (IsSemimoduleMonomorphism)
module Algebra.Module.Morphism.SemimoduleMonomorphism
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawSemimodule R a ℓ₁} {N : RawSemimodule R b ℓ₂} {⟦_⟧}
(isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧)
where
open IsSemimoduleMonomorphism isSemimoduleMonomorphism
private
module M = RawSemimodule M
module N = RawSemimodule N
open import Algebra.Bundles using (CommutativeSemiring)
open import Algebra.Core using (Op₂)
import Algebra.Module.Definitions.Bi.Simultaneous as SimulDefs
open import Algebra.Module.Structures using (IsSemimodule)
open import Algebra.Structures using (IsCommutativeSemiring; IsMagma)
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.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public
------------------------------------------------------------------------
-- Properties
module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where
open IsMagma +ᴹ-isMagma
using (setoid)
renaming (∙-cong to +ᴹ-cong)
open SetoidReasoning setoid
private
module MDefs = SimulDefs R M._≈ᴹ_
module NDefs = SimulDefs R N._≈ᴹ_
*ₗ-*ᵣ-coincident : NDefs.Coincident N._*ₗ_ N._*ᵣ_ → MDefs.Coincident M._*ₗ_ M._*ᵣ_
*ₗ-*ᵣ-coincident *ₗ-*ᵣ-coincident x m = injective $ begin
⟦ x M.*ₗ m ⟧ ≈⟨ *ₗ-homo x m ⟩
x N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-*ᵣ-coincident x ⟦ m ⟧ ⟩
⟦ m ⟧ N.*ᵣ x ≈˘⟨ *ᵣ-homo x m ⟩
⟦ m M.*ᵣ x ⟧ ∎
------------------------------------------------------------------------
-- Structures
module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ 0# 1#} (R-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#) where
private
R-commutativeSemiring : CommutativeSemiring _ _
R-commutativeSemiring = record { isCommutativeSemiring = R-isCommutativeSemiring }
open IsCommutativeSemiring R-isCommutativeSemiring
isSemimodule
: IsSemimodule R-commutativeSemiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
→ IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
isSemimodule isSemimodule = record
{ isBisemimodule = isBisemimodule isSemiring isSemiring NN.isBisemimodule
; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident
}
where
module NN = IsSemimodule isSemimodule
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