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