------------------------------------------------------------------------
-- The Agda standard library
--
-- Some algebraic structures defined over some other structure
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Module.Structures where
open import Algebra.Bundles
using (Semiring; Ring; CommutativeSemiring; CommutativeRing)
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Module.Core using (Opₗ; Opᵣ)
import Algebra.Definitions as Defs
open import Algebra.Module.Definitions
using (module LeftDefs; module RightDefs; module BiDefs
; module SimultaneousBiDefs)
open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
private
variable
m ℓm r ℓr s ℓs : Level
M : Set m
module _ (semiring : Semiring r ℓr) (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
where
open Semiring semiring renaming (Carrier to R)
record IsPreleftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open LeftDefs R ≈ᴹ
field
*ₗ-cong : Congruent _≈_ *ₗ
*ₗ-zeroˡ : LeftZero 0# 0ᴹ *ₗ
*ₗ-distribʳ : *ₗ DistributesOverʳ _+_ ⟶ +ᴹ
*ₗ-identityˡ : LeftIdentity 1# *ₗ
*ₗ-assoc : Associative _*_ *ₗ
*ₗ-zeroʳ : RightZero 0ᴹ *ₗ
*ₗ-distribˡ : *ₗ DistributesOverˡ +ᴹ
record IsLeftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open LeftDefs R ≈ᴹ
field
+ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
isPreleftSemimodule : IsPreleftSemimodule *ₗ
open IsPreleftSemimodule isPreleftSemimodule public
open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
using () renaming
( assoc to +ᴹ-assoc
; comm to +ᴹ-comm
; identity to +ᴹ-identity
; identityʳ to +ᴹ-identityʳ
; identityˡ to +ᴹ-identityˡ
; isEquivalence to ≈ᴹ-isEquivalence
; isMagma to +ᴹ-isMagma
; isMonoid to +ᴹ-isMonoid
; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
; isSemigroup to +ᴹ-isSemigroup
; refl to ≈ᴹ-refl
; reflexive to ≈ᴹ-reflexive
; setoid to ≈ᴹ-setoid
; sym to ≈ᴹ-sym
; trans to ≈ᴹ-trans
; ∙-cong to +ᴹ-cong
; ∙-congʳ to +ᴹ-congʳ
; ∙-congˡ to +ᴹ-congˡ
)
*ₗ-congˡ : LeftCongruent *ₗ
*ₗ-congˡ mm = *ₗ-cong refl mm
*ₗ-congʳ : RightCongruent _≈_ *ₗ
*ₗ-congʳ xx = *ₗ-cong xx ≈ᴹ-refl
record IsPrerightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open RightDefs R ≈ᴹ
field
*ᵣ-cong : Congruent _≈_ *ᵣ
*ᵣ-zeroʳ : RightZero 0# 0ᴹ *ᵣ
*ᵣ-distribˡ : *ᵣ DistributesOverˡ _+_ ⟶ +ᴹ
*ᵣ-identityʳ : RightIdentity 1# *ᵣ
*ᵣ-assoc : Associative _*_ *ᵣ
*ᵣ-zeroˡ : LeftZero 0ᴹ *ᵣ
*ᵣ-distribʳ : *ᵣ DistributesOverʳ +ᴹ
record IsRightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open RightDefs R ≈ᴹ
field
+ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
isPrerightSemimodule : IsPrerightSemimodule *ᵣ
open IsPrerightSemimodule isPrerightSemimodule public
open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
using () renaming
( assoc to +ᴹ-assoc
; comm to +ᴹ-comm
; identity to +ᴹ-identity
; identityʳ to +ᴹ-identityʳ
; identityˡ to +ᴹ-identityˡ
; isEquivalence to ≈ᴹ-isEquivalence
; isMagma to +ᴹ-isMagma
; isMonoid to +ᴹ-isMonoid
; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
; isSemigroup to +ᴹ-isSemigroup
; refl to ≈ᴹ-refl
; reflexive to ≈ᴹ-reflexive
; setoid to ≈ᴹ-setoid
; sym to ≈ᴹ-sym
; trans to ≈ᴹ-trans
; ∙-cong to +ᴹ-cong
; ∙-congʳ to +ᴹ-congʳ
; ∙-congˡ to +ᴹ-congˡ
)
*ᵣ-congˡ : LeftCongruent _≈_ *ᵣ
*ᵣ-congˡ xx = *ᵣ-cong ≈ᴹ-refl xx
*ᵣ-congʳ : RightCongruent *ᵣ
*ᵣ-congʳ mm = *ᵣ-cong mm refl
module _ (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs)
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
where
open Semiring R-semiring using () renaming (Carrier to R)
open Semiring S-semiring using () renaming (Carrier to S)
record IsBisemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
: Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
open BiDefs R S ≈ᴹ
field
+ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
isPreleftSemimodule : IsPreleftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
isPrerightSemimodule : IsPrerightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
*ₗ-*ᵣ-assoc : Associative *ₗ *ᵣ
isLeftSemimodule : IsLeftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
isLeftSemimodule = record
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
; isPreleftSemimodule = isPreleftSemimodule
}
isRightSemimodule : IsRightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
isRightSemimodule = record
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
; isPrerightSemimodule = isPrerightSemimodule
}
open IsLeftSemimodule isLeftSemimodule public
hiding (+ᴹ-isCommutativeMonoid; isPreleftSemimodule)
open IsPrerightSemimodule isPrerightSemimodule public
open IsRightSemimodule isRightSemimodule public
using (*ᵣ-congˡ; *ᵣ-congʳ)
module _ (commutativeSemiring : CommutativeSemiring r ℓr)
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
where
open CommutativeSemiring commutativeSemiring renaming (Carrier to R)
-- An R-semimodule is an R-R-bisemimodule where R is commutative.
-- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
-- may be that they do not coincide up to definitional equality.
open SimultaneousBiDefs R ≈ᴹ
record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
: Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
*ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
open IsBisemimodule isBisemimodule public
module _ (ring : Ring r ℓr)
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
where
open Ring ring renaming (Carrier to R)
record IsLeftModule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open Defs ≈ᴹ
field
isLeftSemimodule : IsLeftSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
-ᴹ‿cong : Congruent₁ -ᴹ
-ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ
open IsLeftSemimodule isLeftSemimodule public
+ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
+ᴹ-isAbelianGroup = record
{ isGroup = record
{ isMonoid = +ᴹ-isMonoid
; inverse = -ᴹ‿inverse
; ⁻¹-cong = -ᴹ‿cong
}
; comm = +ᴹ-comm
}
open IsAbelianGroup +ᴹ-isAbelianGroup public
using () renaming
( isGroup to +ᴹ-isGroup
; inverseˡ to -ᴹ‿inverseˡ
; inverseʳ to -ᴹ‿inverseʳ
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
)
{-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
"Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
Please use Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ instead."
#-}
{-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
"Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
Please use Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ instead."
#-}
record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
open Defs ≈ᴹ
field
isRightSemimodule : IsRightSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
-ᴹ‿cong : Congruent₁ -ᴹ
-ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ
open IsRightSemimodule isRightSemimodule public
+ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
+ᴹ-isAbelianGroup = record
{ isGroup = record
{ isMonoid = +ᴹ-isMonoid
; inverse = -ᴹ‿inverse
; ⁻¹-cong = -ᴹ‿cong
}
; comm = +ᴹ-comm
}
open IsAbelianGroup +ᴹ-isAbelianGroup public
using () renaming
( isGroup to +ᴹ-isGroup
; inverseˡ to -ᴹ‿inverseˡ
; inverseʳ to -ᴹ‿inverseʳ
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
)
{-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
"Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
Please use Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ instead."
#-}
{-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
"Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
Please use Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ instead."
#-}
module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
where
open Ring R-ring renaming (Carrier to R; semiring to R-semiring)
open Ring S-ring renaming (Carrier to S; semiring to S-semiring)
record IsBimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
: Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
open Defs ≈ᴹ
field
isBisemimodule : IsBisemimodule R-semiring S-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
-ᴹ‿cong : Congruent₁ -ᴹ
-ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ
open IsBisemimodule isBisemimodule public
isLeftModule : IsLeftModule R-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ
isLeftModule = record
{ isLeftSemimodule = isLeftSemimodule
; -ᴹ‿cong = -ᴹ‿cong
; -ᴹ‿inverse = -ᴹ‿inverse
}
open IsLeftModule isLeftModule public
using ( +ᴹ-isAbelianGroup; +ᴹ-isGroup; -ᴹ‿inverseˡ; -ᴹ‿inverseʳ
; uniqueˡ‿-ᴹ; uniqueʳ‿-ᴹ)
isRightModule : IsRightModule S-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ
isRightModule = record
{ isRightSemimodule = isRightSemimodule
; -ᴹ‿cong = -ᴹ‿cong
; -ᴹ‿inverse = -ᴹ‿inverse
}
module _ (commutativeRing : CommutativeRing r ℓr)
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
where
open CommutativeRing commutativeRing renaming (Carrier to R)
-- An R-module is an R-R-bimodule where R is commutative.
-- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
-- may be that they do not coincide up to definitional equality.
open SimultaneousBiDefs R ≈ᴹ
record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ
*ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
open IsBimodule isBimodule public
isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident }
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