------------------------------------------------------------------------
-- The Agda standard library
--
-- This module constructs the unit of the monoidal structure on
-- R-modules, and similar for weaker module-like structures.
-- The intended universal property is that the maps out of the tensor
-- unit into M are isomorphic to the elements of M.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Module.Construct.TensorUnit where
open import Algebra.Bundles
using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring
; CommutativeRing)
open import Algebra.Module.Bundles
using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule
; RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule
; RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule
; Module)
open import Level using (Level; _⊔_)
private
variable
c ℓ : Level
------------------------------------------------------------------------
-- Raw bundles
rawLeftSemimodule : {R : RawSemiring c ℓ} → RawLeftSemimodule _ c ℓ
rawLeftSemimodule {R = R} = record
{ _≈ᴹ_ = _≈_
; _+ᴹ_ = _+_
; _*ₗ_ = _*_
; 0ᴹ = 0#
} where open RawSemiring R
rawLeftModule : {R : RawRing c ℓ} → RawLeftModule _ c ℓ
rawLeftModule {R = R} = record
{ RawLeftSemimodule (rawLeftSemimodule {R = rawSemiring})
; -ᴹ_ = -_
} where open RawRing R
rawRightSemimodule : {R : RawSemiring c ℓ} → RawRightSemimodule _ c ℓ
rawRightSemimodule {R = R} = record
{ _≈ᴹ_ = _≈_
; _+ᴹ_ = _+_
; _*ᵣ_ = _*_
; 0ᴹ = 0#
} where open RawSemiring R
rawRightModule : {R : RawRing c ℓ} → RawRightModule _ c ℓ
rawRightModule {R = R} = record
{ RawRightSemimodule (rawRightSemimodule {R = rawSemiring})
; -ᴹ_ = -_
} where open RawRing R
rawBisemimodule : {R : RawSemiring c ℓ} → RawBisemimodule _ _ c ℓ
rawBisemimodule {R = R} = record
{ _≈ᴹ_ = _≈_
; _+ᴹ_ = _+_
; _*ₗ_ = _*_
; _*ᵣ_ = _*_
; 0ᴹ = 0#
} where open RawSemiring R
rawBimodule : {R : RawRing c ℓ} → RawBimodule _ _ c ℓ
rawBimodule {R = R} = record
{ RawBisemimodule (rawBisemimodule {R = rawSemiring})
; -ᴹ_ = -_
} where open RawRing R
rawSemimodule : {R : RawSemiring c ℓ} → RawSemimodule _ c ℓ
rawSemimodule {R = R} = rawBisemimodule {R = R}
rawModule : {R : RawRing c ℓ} → RawModule _ c ℓ
rawModule {R = R} = rawBimodule {R = R}
------------------------------------------------------------------------
-- Bundles
leftSemimodule : {R : Semiring c ℓ} → LeftSemimodule R c ℓ
leftSemimodule {R = semiring} = record
{ Carrierᴹ = Carrier
; _≈ᴹ_ = _≈_
; _+ᴹ_ = _+_
; _*ₗ_ = _*_
; 0ᴹ = 0#
; isLeftSemimodule = record
{ +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
; isPreleftSemimodule = record
{ *ₗ-cong = *-cong
; *ₗ-zeroˡ = zeroˡ
; *ₗ-distribʳ = distribʳ
; *ₗ-identityˡ = *-identityˡ
; *ₗ-assoc = *-assoc
; *ₗ-zeroʳ = zeroʳ
; *ₗ-distribˡ = distribˡ
}
}
} where open Semiring semiring
rightSemimodule : {R : Semiring c ℓ} → RightSemimodule R c ℓ
rightSemimodule {R = semiring} = record
{ Carrierᴹ = Carrier
; _≈ᴹ_ = _≈_
; _+ᴹ_ = _+_
; _*ᵣ_ = _*_
; 0ᴹ = 0#
; isRightSemimodule = record
{ +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
; isPrerightSemimodule = record
{ *ᵣ-cong = *-cong
; *ᵣ-zeroʳ = zeroʳ
; *ᵣ-distribˡ = distribˡ
; *ᵣ-identityʳ = *-identityʳ
; *ᵣ-assoc = *-assoc
; *ᵣ-zeroˡ = zeroˡ
; *ᵣ-distribʳ = distribʳ
}
}
} where open Semiring semiring
bisemimodule : {R : Semiring c ℓ} → Bisemimodule R R c ℓ
bisemimodule {R = semiring} = record
{ isBisemimodule = record
{ +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
; isPreleftSemimodule =
LeftSemimodule.isPreleftSemimodule leftSemimodule
; isPrerightSemimodule =
RightSemimodule.isPrerightSemimodule rightSemimodule
; *ₗ-*ᵣ-assoc = *-assoc
}
} where open Semiring semiring
semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ
semimodule {R = commutativeSemiring} = record
{ isSemimodule = record
{ isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
; *ₗ-*ᵣ-coincident = *-comm
}
} where open CommutativeSemiring commutativeSemiring
leftModule : {R : Ring c ℓ} → LeftModule R c ℓ
leftModule {R = ring} = record
{ -ᴹ_ = -_
; isLeftModule = record
{ isLeftSemimodule = LeftSemimodule.isLeftSemimodule leftSemimodule
; -ᴹ‿cong = -‿cong
; -ᴹ‿inverse = -‿inverse
}
} where open Ring ring
rightModule : {R : Ring c ℓ} → RightModule R c ℓ
rightModule {R = ring} = record
{ -ᴹ_ = -_
; isRightModule = record
{ isRightSemimodule = RightSemimodule.isRightSemimodule rightSemimodule
; -ᴹ‿cong = -‿cong
; -ᴹ‿inverse = -‿inverse
}
} where open Ring ring
bimodule : {R : Ring c ℓ} → Bimodule R R c ℓ
bimodule {R = ring} = record
{ isBimodule = record
{ isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
; -ᴹ‿cong = -‿cong
; -ᴹ‿inverse = -‿inverse
}
} where open Ring ring
⟨module⟩ : {R : CommutativeRing c ℓ} → Module R c ℓ
⟨module⟩ {R = commutativeRing} = record
{ isModule = record
{ isBimodule = Bimodule.isBimodule bimodule
; *ₗ-*ᵣ-coincident = *-comm
}
} where open CommutativeRing commutativeRing
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