------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between bisemimodules
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical-compatible #-}

open import Algebra.Module.Bundles.Raw using (RawBisemimodule)
open import Algebra.Module.Morphism.Structures using (IsBisemimoduleMonomorphism)

module Algebra.Module.Morphism.BisemimoduleMonomorphism
  {r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧}
  (isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
  where

open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
private
  module M = RawBisemimodule M
  module N = RawBisemimodule N

open import Algebra.Bundles using (Semiring)
open import Algebra.Core using (Op₂)
import Algebra.Module.Definitions.Bi as BiDefs using (Associative)
import Algebra.Module.Definitions.Left as LeftDefs using (LeftCongruent)
import Algebra.Module.Definitions.Right as RightDefs using (RightCongruent)
open import Algebra.Module.Structures using (IsBisemimodule)
open import Algebra.Structures using (IsMagma; IsSemiring)
open import Function.Base using (flip; _$_)
open import Relation.Binary.Core using (Rel)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

------------------------------------------------------------------------
-- Re-exports

open import Algebra.Morphism.MonoidMonomorphism
  +ᴹ-isMonoidMonomorphism public
    using ()
    renaming
      ( cong to +ᴹ-cong
      ; assoc to +ᴹ-assoc
      ; comm to +ᴹ-comm
      ; identityˡ to +ᴹ-identityˡ
      ; identityʳ to +ᴹ-identityʳ
      ; identity to +ᴹ-identity
      ; isMagma to +ᴹ-isMagma
      ; isSemigroup to +ᴹ-isSemigroup
      ; isMonoid to +ᴹ-isMonoid
      ; isCommutativeMonoid to +ᴹ-isCommutativeMonoid
      )

open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism
  isLeftSemimoduleMonomorphism public
  using
    ( *ₗ-cong
    ; *ₗ-zeroˡ
    ; *ₗ-distribʳ
    ; *ₗ-identityˡ
    ; *ₗ-assoc
    ; *ₗ-zeroʳ
    ; *ₗ-distribˡ
    ; isLeftSemimodule
    )

open import Algebra.Module.Morphism.RightSemimoduleMonomorphism
  isRightSemimoduleMonomorphism public
  using
    ( *ᵣ-cong
    ; *ᵣ-zeroʳ
    ; *ᵣ-distribˡ
    ; *ᵣ-identityʳ
    ; *ᵣ-assoc
    ; *ᵣ-zeroˡ
    ; *ᵣ-distribʳ
    ; isRightSemimodule
    )

------------------------------------------------------------------------
-- Properties

module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where

  open IsMagma +ᴹ-isMagma
    using (setoid)
    renaming (∙-cong to +ᴹ-cong)
  open SetoidReasoning setoid

  private
    module MDefs = BiDefs R S M._≈ᴹ_
    module NDefs = BiDefs R S N._≈ᴹ_
    module LDefs = LeftDefs R N._≈ᴹ_
    module RDefs = RightDefs S N._≈ᴹ_

  *ₗ-*ᵣ-assoc
    : LDefs.LeftCongruent N._*ₗ_ → RDefs.RightCongruent N._*ᵣ_
    → NDefs.Associative N._*ₗ_ N._*ᵣ_
    → MDefs.Associative M._*ₗ_ M._*ᵣ_
  *ₗ-*ᵣ-assoc *ₗ-congˡ *ᵣ-congʳ *ₗ-*ᵣ-assoc x m y = injective $ begin
    ⟦ (x M.*ₗ m) M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (x M.*ₗ m) ⟩
    ⟦ x M.*ₗ m ⟧ N.*ᵣ y   ≈⟨ *ᵣ-congʳ (*ₗ-homo x m) ⟩
    (x N.*ₗ ⟦ m ⟧) N.*ᵣ y ≈⟨ *ₗ-*ᵣ-assoc x ⟦ m ⟧ y ⟩
    x N.*ₗ (⟦ m ⟧ N.*ᵣ y) ≈˘⟨ *ₗ-congˡ (*ᵣ-homo y m) ⟩
    x N.*ₗ ⟦ m M.*ᵣ y ⟧   ≈˘⟨ *ₗ-homo x (m M.*ᵣ y) ⟩
    ⟦ x M.*ₗ (m M.*ᵣ y) ⟧ ∎

------------------------------------------------------------------------
-- Structures

module _
  {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ 0r 1r}
  {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ 0s 1s}
  (R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r)
  (S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s)
  where

  private
    R-semiring : Semiring _ _
    R-semiring = record { isSemiring = R-isSemiring }

    S-semiring : Semiring _ _
    S-semiring = record { isSemiring = S-isSemiring }

  isBisemimodule
    : IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
    → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
  isBisemimodule isBisemimodule = record
    { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid
    ; isPreleftSemimodule = record
      { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong
      ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ
      ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ
      ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ
      ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc
      ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ
      ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ
      }
    ; isPrerightSemimodule = record
      { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong
      ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ
      ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ
      ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ
      ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc
      ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ
      ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ
      }
    ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc
    }
    where
      module NN = IsBisemimodule isBisemimodule