------------------------------------------------------------------------
-- The Agda standard library
--
-- This module provides alternative ways of providing instances of
-- structures in the Algebra.Module hierarchy.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
module Algebra.Module.Structures.Biased 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ᵣ)
open import Algebra.Module.Consequences
open import Algebra.Module.Structures
using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule;
IsSemimodule; IsLeftModule; IsRightModule; IsModule)
open import Function.Base using (flip)
open import Level using (Level; _⊔_)
private
variable
m ℓm r ℓr s ℓs : Level
M : Set m
module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
open CommutativeSemiring commutativeSemiring renaming (Carrier to R)
-- A left semimodule over a commutative semiring is already a semimodule.
record IsSemimoduleFromLeft (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
(*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isLeftSemimodule : IsLeftSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
open IsLeftSemimodule isLeftSemimodule
isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
isBisemimodule = record
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
; isPreleftSemimodule = isPreleftSemimodule
; isPrerightSemimodule = record
{ *ᵣ-cong = flip *ₗ-cong
; *ᵣ-zeroʳ = *ₗ-zeroˡ
; *ᵣ-distribˡ = *ₗ-distribʳ
; *ᵣ-identityʳ = *ₗ-identityˡ
; *ᵣ-assoc =
*ₗ-assoc∧comm⇒*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
; *ᵣ-zeroˡ = *ₗ-zeroʳ
; *ᵣ-distribʳ = *ₗ-distribˡ
}
; *ₗ-*ᵣ-assoc =
*ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
}
isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
isSemimodule = record
{ isBisemimodule = isBisemimodule
; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
}
-- Similarly, a right semimodule over a commutative semiring
-- is already a semimodule.
record IsSemimoduleFromRight (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
(*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isRightSemimodule : IsRightSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
open IsRightSemimodule isRightSemimodule
isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
isBisemimodule = record
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
; isPreleftSemimodule = record
{ *ₗ-cong = flip *ᵣ-cong
; *ₗ-zeroˡ = *ᵣ-zeroʳ
; *ₗ-distribʳ = *ᵣ-distribˡ
; *ₗ-identityˡ = *ᵣ-identityʳ
; *ₗ-assoc =
*ᵣ-assoc∧comm⇒*ₗ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
; *ₗ-zeroʳ = *ᵣ-zeroˡ
; *ₗ-distribˡ = *ᵣ-distribʳ
}
; isPrerightSemimodule = isPrerightSemimodule
; *ₗ-*ᵣ-assoc =
*ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
}
isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
isSemimodule = record
{ isBisemimodule = isBisemimodule
; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
}
module _ (commutativeRing : CommutativeRing r ℓr) where
open CommutativeRing commutativeRing renaming (Carrier to R)
-- A left module over a commutative ring is already a module.
record IsModuleFromLeft (≈ᴹ : Rel {m} M ℓm)
(+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M) (*ₗ : Opₗ R M)
: Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isLeftModule : IsLeftModule ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ
open IsLeftModule isLeftModule
isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ (flip *ₗ)
isModule = record
{ isBimodule = record
{ isBisemimodule = IsSemimoduleFromLeft.isBisemimodule
{commutativeSemiring = commutativeSemiring}
(record { isLeftSemimodule = isLeftSemimodule })
; -ᴹ‿cong = -ᴹ‿cong
; -ᴹ‿inverse = -ᴹ‿inverse
}
; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
}
-- Similarly, a right module over a commutative ring is already a module.
record IsModuleFromRight (≈ᴹ : Rel {m} M ℓm)
(+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M) (*ᵣ : Opᵣ R M)
: Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
field
isRightModule : IsRightModule ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ
open IsRightModule isRightModule
isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ (flip *ᵣ) *ᵣ
isModule = record
{ isBimodule = record
{ isBisemimodule = IsSemimoduleFromRight.isBisemimodule
{commutativeSemiring = commutativeSemiring}
(record { isRightSemimodule = isRightSemimodule })
; -ᴹ‿cong = -ᴹ‿cong
; -ᴹ‿inverse = -ᴹ‿inverse
}
; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
}
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