From a18e51bb2efa962312c1184b28c6ab8894410f4a Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 6 Dec 2024 17:26:52 +0100 Subject: [PATCH] Consequences of module monomorphisms (#2276) * First shot at left semimodule monomorphism consequences * Weaken arguments of properties * Remember I made a variable declaration for this * Left module monomorphisms * Attempt using qualified names rather than renaming * Mark modules as private * Typo * These modules should be private * Monomorphisms over right semimodules * Monomorphisms over right modules * Add properties of bisemimodule monomorphisms * Make these modules private * Properties of bimodule monomorphisms * Properties of semimodule monomorphisms * Move modules to the right location * Add missing options * Properties of module monomorphisms * Fix somewhitespace * Use IsMagma rather than IsMonoid in several places * Spell re-exports consistently * Use modules to make type signatures of structures clearer * [ changelog ] listing the new modules --------- Co-authored-by: Guillaume Allais --- CHANGELOG.md | 12 ++ .../Module/Morphism/BimoduleMonomorphism.agda | 73 +++++++++ .../Morphism/BisemimoduleMonomorphism.agda | 149 ++++++++++++++++++ .../Morphism/LeftModuleMonomorphism.agda | 62 ++++++++ .../Morphism/LeftSemimoduleMonomorphism.agda | 147 +++++++++++++++++ .../Module/Morphism/ModuleMonomorphism.agda | 54 +++++++ .../Morphism/RightModuleMonomorphism.agda | 61 +++++++ .../Morphism/RightSemimoduleMonomorphism.agda | 147 +++++++++++++++++ .../Morphism/SemimoduleMonomorphism.agda | 75 +++++++++ 9 files changed, 780 insertions(+) create mode 100644 src/Algebra/Module/Morphism/BimoduleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/ModuleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/RightModuleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda create mode 100644 src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 9874c5593d..3f4b5ee350 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -91,6 +91,18 @@ New modules Algebra.Properties.IdempotentCommutativeMonoid ``` +* Consequences of module monomorphisms + ```agda + Algebra.Module.Morphism.BimoduleMonomorphism + Algebra.Module.Morphism.BisemimoduleMonomorphism + Algebra.Module.Morphism.LeftModuleMonomorphism + Algebra.Module.Morphism.LeftSemimoduleMonomorphism + Algebra.Module.Morphism.ModuleMonomorphism + Algebra.Module.Morphism.RightModuleMonomorphism + Algebra.Module.Morphism.RightSemimoduleMonomorphism + Algebra.Module.Morphism.SemimoduleMonomorphism + ``` + * Refactoring of the `Algebra.Solver.*Monoid` implementations, via a single `Solver` module API based on the existing `Expr`, and a common `Normal`-form API: diff --git a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda new file mode 100644 index 0000000000..6cbdb5d8ba --- /dev/null +++ b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda @@ -0,0 +1,73 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a monomorphism between bimodules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +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 +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- 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 + diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda new file mode 100644 index 0000000000..1a1142732b --- /dev/null +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -0,0 +1,149 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between bisemimodules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +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 +open import Algebra.Core +import Algebra.Module.Definitions.Bi as BiDefs +import Algebra.Module.Definitions.Left as LeftDefs +import Algebra.Module.Definitions.Right as RightDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Relation.Binary.Core +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 diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda new file mode 100644 index 0000000000..8aa4307fa6 --- /dev/null +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -0,0 +1,62 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between left modules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.LeftModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawLeftModule R a ℓ₁} {N : RawLeftModule R b ℓ₂} {⟦_⟧} + (isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧) + where + +open IsLeftModuleMonomorphism isLeftModuleMonomorphism +private + module M = RawLeftModule M + module N = RawLeftModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- 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.LeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Structures + +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-ring : Ring _ _ + R-ring = record { isRing = R-isRing } + open IsRing R-isRing + + isLeftModule + : IsLeftModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ + → IsLeftModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ + isLeftModule isLeftModule = record + { isLeftSemimodule = isLeftSemimodule isSemiring NN.isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module NN = IsLeftModule isLeftModule diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda new file mode 100644 index 0000000000..1976dc226c --- /dev/null +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -0,0 +1,147 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between left semimodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.LeftSemimoduleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M₁ : RawLeftSemimodule R a ℓ₁} {M₂ : RawLeftSemimodule R b ℓ₂} {⟦_⟧} + (isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ ⟦_⟧) + where + +open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism +private + module M = RawLeftSemimodule M₁ + module N = RawLeftSemimodule M₂ + +open import Algebra.Bundles +open import Algebra.Core +import Algebra.Module.Definitions.Left as LeftDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Level +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +private + variable + ℓr : Level + _≈_ : Rel R ℓr + _+_ _*_ : Op₂ R + 0# 1# : R + +------------------------------------------------------------------------ +-- Re-export most properties of monoid monomorphisms + +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 + ) + +---------------------------------------------------------------------------------- +-- Properties + +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where + + open IsMagma +ᴹ-isMagma + using (setoid) + renaming (∙-cong to +ᴹ-cong′) + open SetoidReasoning setoid + + module MDefs = LeftDefs R M._≈ᴹ_ + module NDefs = LeftDefs R N._≈ᴹ_ + + *ₗ-cong : NDefs.Congruent _≈_ N._*ₗ_ → MDefs.Congruent _≈_ M._*ₗ_ + *ₗ-cong *ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin + ⟦ x M.*ₗ u ⟧ ≈⟨ *ₗ-homo x u ⟩ + x N.*ₗ ⟦ u ⟧ ≈⟨ *ₗ-cong x≈y (⟦⟧-cong u≈ᴹv) ⟩ + y N.*ₗ ⟦ v ⟧ ≈˘⟨ *ₗ-homo y v ⟩ + ⟦ y M.*ₗ v ⟧ ∎ + + *ₗ-zeroˡ : NDefs.LeftZero 0# N.0ᴹ N._*ₗ_ → MDefs.LeftZero 0# M.0ᴹ M._*ₗ_ + *ₗ-zeroˡ {0# = 0#} *ₗ-zeroˡ x = injective $ begin + ⟦ 0# M.*ₗ x ⟧ ≈⟨ *ₗ-homo 0# x ⟩ + 0# N.*ₗ ⟦ x ⟧ ≈⟨ *ₗ-zeroˡ ⟦ x ⟧ ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ₗ-distribʳ : N._*ₗ_ NDefs.DistributesOverʳ _+_ ⟶ N._+ᴹ_ → M._*ₗ_ MDefs.DistributesOverʳ _+_ ⟶ M._+ᴹ_ + *ₗ-distribʳ {_+_ = _+_} *ₗ-distribʳ x m n = injective $ begin + ⟦ (m + n) M.*ₗ x ⟧ ≈⟨ *ₗ-homo (m + n) x ⟩ + (m + n) N.*ₗ ⟦ x ⟧ ≈⟨ *ₗ-distribʳ ⟦ x ⟧ m n ⟩ + m N.*ₗ ⟦ x ⟧ N.+ᴹ n N.*ₗ ⟦ x ⟧ ≈˘⟨ +ᴹ-cong′ (*ₗ-homo m x) (*ₗ-homo n x) ⟩ + ⟦ m M.*ₗ x ⟧ N.+ᴹ ⟦ n M.*ₗ x ⟧ ≈˘⟨ +ᴹ-homo (m M.*ₗ x) (n M.*ₗ x) ⟩ + ⟦ m M.*ₗ x M.+ᴹ n M.*ₗ x ⟧ ∎ + + *ₗ-identityˡ : NDefs.LeftIdentity 1# N._*ₗ_ → MDefs.LeftIdentity 1# M._*ₗ_ + *ₗ-identityˡ {1# = 1#} *ₗ-identityˡ m = injective $ begin + ⟦ 1# M.*ₗ m ⟧ ≈⟨ *ₗ-homo 1# m ⟩ + 1# N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-identityˡ ⟦ m ⟧ ⟩ + ⟦ m ⟧ ∎ + + *ₗ-assoc : NDefs.LeftCongruent N._*ₗ_ → NDefs.Associative _*_ N._*ₗ_ → MDefs.Associative _*_ M._*ₗ_ + *ₗ-assoc {_*_ = _*_} *ₗ-congˡ *ₗ-assoc x y m = injective $ begin + ⟦ (x * y) M.*ₗ m ⟧ ≈⟨ *ₗ-homo (x * y) m ⟩ + (x * y) N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-assoc x y ⟦ m ⟧ ⟩ + x N.*ₗ y N.*ₗ ⟦ m ⟧ ≈˘⟨ *ₗ-congˡ (*ₗ-homo y m) ⟩ + x N.*ₗ ⟦ y M.*ₗ m ⟧ ≈˘⟨ *ₗ-homo x (y M.*ₗ m) ⟩ + ⟦ x M.*ₗ y M.*ₗ m ⟧ ∎ + + *ₗ-zeroʳ : NDefs.LeftCongruent N._*ₗ_ → NDefs.RightZero N.0ᴹ N._*ₗ_ → MDefs.RightZero M.0ᴹ M._*ₗ_ + *ₗ-zeroʳ *ₗ-congˡ *ₗ-zeroʳ x = injective $ begin + ⟦ x M.*ₗ M.0ᴹ ⟧ ≈⟨ *ₗ-homo x M.0ᴹ ⟩ + x N.*ₗ ⟦ M.0ᴹ ⟧ ≈⟨ *ₗ-congˡ 0ᴹ-homo ⟩ + x N.*ₗ N.0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ₗ-distribˡ : NDefs.LeftCongruent N._*ₗ_ → N._*ₗ_ NDefs.DistributesOverˡ N._+ᴹ_ → M._*ₗ_ MDefs.DistributesOverˡ M._+ᴹ_ + *ₗ-distribˡ *ₗ-congˡ *ₗ-distribˡ x m n = injective $ begin + ⟦ x M.*ₗ (m M.+ᴹ n) ⟧ ≈⟨ *ₗ-homo x (m M.+ᴹ n) ⟩ + x N.*ₗ ⟦ m M.+ᴹ n ⟧ ≈⟨ *ₗ-congˡ (+ᴹ-homo m n) ⟩ + x N.*ₗ (⟦ m ⟧ N.+ᴹ ⟦ n ⟧) ≈⟨ *ₗ-distribˡ x ⟦ m ⟧ ⟦ n ⟧ ⟩ + x N.*ₗ ⟦ m ⟧ N.+ᴹ x N.*ₗ ⟦ n ⟧ ≈˘⟨ +ᴹ-cong′ (*ₗ-homo x m) (*ₗ-homo x n) ⟩ + ⟦ x M.*ₗ m ⟧ N.+ᴹ ⟦ x M.*ₗ n ⟧ ≈˘⟨ +ᴹ-homo (x M.*ₗ m) (x M.*ₗ n) ⟩ + ⟦ x M.*ₗ m M.+ᴹ x M.*ₗ n ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +module _ (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) where + + private + R-semiring : Semiring _ _ + R-semiring = record { isSemiring = R-isSemiring } + + isLeftSemimodule + : IsLeftSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ + → IsLeftSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ + isLeftSemimodule isLeftSemimodule = 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ˡ + } + } where module NN = IsLeftSemimodule isLeftSemimodule diff --git a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda new file mode 100644 index 0000000000..29b9f68311 --- /dev/null +++ b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda @@ -0,0 +1,54 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between modules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.ModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawModule R a ℓ₁} {N : RawModule R b ℓ₂} {⟦_⟧} + (isModuleMonomorphism : IsModuleMonomorphism M N ⟦_⟧) + where + +open IsModuleMonomorphism isModuleMonomorphism +private + module M = RawModule M + module N = RawModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- Re-exports + +open import Algebra.Module.Morphism.BimoduleMonomorphism isBimoduleMonomorphism public +open import Algebra.Module.Morphism.SemimoduleMonomorphism isSemimoduleMonomorphism public + using (*ₗ-*ᵣ-coincident; isSemimodule) + +------------------------------------------------------------------------ +-- Structures + +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-commutativeRing : CommutativeRing _ _ + R-commutativeRing = record { isCommutativeRing = R-isCommutativeRing } + + open IsCommutativeRing R-isCommutativeRing + + isModule + : IsModule R-commutativeRing N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsModule R-commutativeRing M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ + isModule isModule = record + { isBimodule = isBimodule isRing isRing NN.isBimodule + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident + } + where + module NN = IsModule isModule diff --git a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda new file mode 100644 index 0000000000..23a6f68248 --- /dev/null +++ b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between right modules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.RightModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightModule R a ℓ₁} {N : RawRightModule R b ℓ₂} {⟦_⟧} + (isRightModuleMonomorphism : IsRightModuleMonomorphism M N ⟦_⟧) + where + +open IsRightModuleMonomorphism isRightModuleMonomorphism +module M = RawRightModule M +module N = RawRightModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- 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.RightSemimoduleMonomorphism isRightSemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Structures + +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-ring : Ring _ _ + R-ring = record { isRing = R-isRing} + open IsRing R-isRing + + isRightModule + : IsRightModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ᵣ_ + → IsRightModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ᵣ_ + isRightModule isRightModule = record + { isRightSemimodule = isRightSemimodule isSemiring NN.isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module NN = IsRightModule isRightModule diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda new file mode 100644 index 0000000000..b3d0c312a0 --- /dev/null +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -0,0 +1,147 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomomorphism between right semimodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.RightSemimoduleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightSemimodule R a ℓ₁} {N : RawRightSemimodule R b ℓ₂} {⟦_⟧} + (isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M N ⟦_⟧) + where + +open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism +private + module M = RawRightSemimodule M + module N = RawRightSemimodule N + +open import Algebra.Bundles +open import Algebra.Core +import Algebra.Module.Definitions.Right as RightDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Level +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +private + variable + ℓr : Level + _≈_ : Rel R ℓr + _+_ _*_ : Op₂ R + 0# 1# : R + +------------------------------------------------------------------------ +-- 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 + ) + +------------------------------------------------------------------------ +-- Properties + +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where + + open IsMagma +ᴹ-isMagma + using (setoid) + renaming (∙-cong to +ᴹ-cong′) + open SetoidReasoning setoid + + module MDefs = RightDefs R M._≈ᴹ_ + module NDefs = RightDefs R N._≈ᴹ_ + + *ᵣ-cong : NDefs.Congruent _≈_ N._*ᵣ_ → MDefs.Congruent _≈_ M._*ᵣ_ + *ᵣ-cong *ᵣ-cong {x} {y} {u} {v} x≈ᴹy u≈v = injective $ begin + ⟦ x M.*ᵣ u ⟧ ≈⟨ *ᵣ-homo u x ⟩ + ⟦ x ⟧ N.*ᵣ u ≈⟨ *ᵣ-cong (⟦⟧-cong x≈ᴹy) u≈v ⟩ + ⟦ y ⟧ N.*ᵣ v ≈˘⟨ *ᵣ-homo v y ⟩ + ⟦ y M.*ᵣ v ⟧ ∎ + + *ᵣ-zeroʳ : NDefs.RightZero 0# N.0ᴹ N._*ᵣ_ → MDefs.RightZero 0# M.0ᴹ M._*ᵣ_ + *ᵣ-zeroʳ {0# = 0#} *ᵣ-zeroʳ x = injective $ begin + ⟦ x M.*ᵣ 0# ⟧ ≈⟨ *ᵣ-homo 0# x ⟩ + ⟦ x ⟧ N.*ᵣ 0# ≈⟨ *ᵣ-zeroʳ ⟦ x ⟧ ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ᵣ-distribˡ : N._*ᵣ_ NDefs.DistributesOverˡ _+_ ⟶ N._+ᴹ_ → M._*ᵣ_ MDefs.DistributesOverˡ _+_ ⟶ M._+ᴹ_ + *ᵣ-distribˡ {_+_ = _+_} *ᵣ-distribˡ x m n = injective $ begin + ⟦ x M.*ᵣ (m + n) ⟧ ≈⟨ *ᵣ-homo (m + n) x ⟩ + ⟦ x ⟧ N.*ᵣ (m + n) ≈⟨ *ᵣ-distribˡ ⟦ x ⟧ m n ⟩ + ⟦ x ⟧ N.*ᵣ m N.+ᴹ ⟦ x ⟧ N.*ᵣ n ≈˘⟨ +ᴹ-cong′ (*ᵣ-homo m x) (*ᵣ-homo n x) ⟩ + ⟦ x M.*ᵣ m ⟧ N.+ᴹ ⟦ x M.*ᵣ n ⟧ ≈˘⟨ +ᴹ-homo (x M.*ᵣ m) (x M.*ᵣ n) ⟩ + ⟦ x M.*ᵣ m M.+ᴹ x M.*ᵣ n ⟧ ∎ + + *ᵣ-identityʳ : NDefs.RightIdentity 1# N._*ᵣ_ → MDefs.RightIdentity 1# M._*ᵣ_ + *ᵣ-identityʳ {1# = 1#} *ᵣ-identityʳ m = injective $ begin + ⟦ m M.*ᵣ 1# ⟧ ≈⟨ *ᵣ-homo 1# m ⟩ + ⟦ m ⟧ N.*ᵣ 1# ≈⟨ *ᵣ-identityʳ ⟦ m ⟧ ⟩ + ⟦ m ⟧ ∎ + + *ᵣ-assoc : NDefs.RightCongruent N._*ᵣ_ → NDefs.Associative _*_ N._*ᵣ_ → MDefs.Associative _*_ M._*ᵣ_ + *ᵣ-assoc {_*_ = _*_} *ᵣ-congʳ *ᵣ-assoc m x y = injective $ begin + ⟦ m M.*ᵣ x M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (m M.*ᵣ x) ⟩ + ⟦ m M.*ᵣ x ⟧ N.*ᵣ y ≈⟨ *ᵣ-congʳ (*ᵣ-homo x m) ⟩ + ⟦ m ⟧ N.*ᵣ x N.*ᵣ y ≈⟨ *ᵣ-assoc ⟦ m ⟧ x y ⟩ + ⟦ m ⟧ N.*ᵣ (x * y) ≈˘⟨ *ᵣ-homo (x * y) m ⟩ + ⟦ m M.*ᵣ (x * y) ⟧ ∎ + + *ᵣ-zeroˡ : NDefs.RightCongruent N._*ᵣ_ → NDefs.LeftZero N.0ᴹ N._*ᵣ_ → MDefs.LeftZero M.0ᴹ M._*ᵣ_ + *ᵣ-zeroˡ *ᵣ-congʳ *ᵣ-zeroˡ x = injective $ begin + ⟦ M.0ᴹ M.*ᵣ x ⟧ ≈⟨ *ᵣ-homo x M.0ᴹ ⟩ + ⟦ M.0ᴹ ⟧ N.*ᵣ x ≈⟨ *ᵣ-congʳ 0ᴹ-homo ⟩ + N.0ᴹ N.*ᵣ x ≈⟨ *ᵣ-zeroˡ x ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ᵣ-distribʳ : NDefs.RightCongruent N._*ᵣ_ → N._*ᵣ_ NDefs.DistributesOverʳ N._+ᴹ_ → M._*ᵣ_ MDefs.DistributesOverʳ M._+ᴹ_ + *ᵣ-distribʳ *ᵣ-congʳ *ᵣ-distribʳ x m n = injective $ begin + ⟦ (m M.+ᴹ n) M.*ᵣ x ⟧ ≈⟨ *ᵣ-homo x (m M.+ᴹ n) ⟩ + ⟦ m M.+ᴹ n ⟧ N.*ᵣ x ≈⟨ *ᵣ-congʳ (+ᴹ-homo m n) ⟩ + (⟦ m ⟧ N.+ᴹ ⟦ n ⟧) N.*ᵣ x ≈⟨ *ᵣ-distribʳ x ⟦ m ⟧ ⟦ n ⟧ ⟩ + ⟦ m ⟧ N.*ᵣ x N.+ᴹ ⟦ n ⟧ N.*ᵣ x ≈˘⟨ +ᴹ-cong′ (*ᵣ-homo x m) (*ᵣ-homo x n) ⟩ + ⟦ m M.*ᵣ x ⟧ N.+ᴹ ⟦ n M.*ᵣ x ⟧ ≈˘⟨ +ᴹ-homo (m M.*ᵣ x) (n M.*ᵣ x) ⟩ + ⟦ m M.*ᵣ x M.+ᴹ n M.*ᵣ x ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +module _ (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) where + + private + R-semiring : Semiring _ _ + R-semiring = record { isSemiring = R-isSemiring } + + isRightSemimodule + : IsRightSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ᵣ_ + → IsRightSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ᵣ_ + isRightSemimodule isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; 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ʳ + } + } where module NN = IsRightSemimodule isRightSemimodule diff --git a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda new file mode 100644 index 0000000000..396230bee3 --- /dev/null +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -0,0 +1,75 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a monomorphism between semimodules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +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 +open import Algebra.Core +import Algebra.Module.Definitions.Bi.Simultaneous as SimulDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Relation.Binary.Core +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