------------------------------------------------------------------------
-- 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
open import Algebra.Module.Bundles
open import 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