Consequences of module monomorphisms

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:

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
+

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

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