------------------------------------------------------------------------
-- 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