------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a monomorphism between semimodules
------------------------------------------------------------------------

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

open import Algebra.Module.Bundles.Raw using (RawSemimodule)
open import Algebra.Module.Morphism.Structures using (IsSemimoduleMonomorphism)

module Algebra.Module.Morphism.SemimoduleMonomorphism
  {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawSemimodule R a ℓ₁} {N : RawSemimodule R b ℓ₂} {⟦_⟧}
  (isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧)
  where

open IsSemimoduleMonomorphism isSemimoduleMonomorphism
private
  module M = RawSemimodule M
  module N = RawSemimodule N

open import Algebra.Bundles using (CommutativeSemiring)
open import Algebra.Core using (Op₂)
import Algebra.Module.Definitions.Bi.Simultaneous as SimulDefs
open import Algebra.Module.Structures using (IsSemimodule)
open import Algebra.Structures using (IsCommutativeSemiring; IsMagma)
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.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public

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

module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where
  open IsMagma +ᴹ-isMagma
    using (setoid)
    renaming (∙-cong to +ᴹ-cong)
  open SetoidReasoning setoid

  private
    module MDefs = SimulDefs R M._≈ᴹ_
    module NDefs = SimulDefs R N._≈ᴹ_

  *ₗ-*ᵣ-coincident : NDefs.Coincident N._*ₗ_ N._*ᵣ_ → MDefs.Coincident M._*ₗ_ M._*ᵣ_
  *ₗ-*ᵣ-coincident *ₗ-*ᵣ-coincident x m = injective $ begin
    ⟦ x M.*ₗ m ⟧ ≈⟨ *ₗ-homo x m ⟩
    x N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-*ᵣ-coincident x ⟦ m ⟧ ⟩
    ⟦ m ⟧ N.*ᵣ x ≈˘⟨ *ᵣ-homo x m ⟩
    ⟦ m M.*ᵣ x ⟧ ∎

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

module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ 0# 1#} (R-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#) where

  private
    R-commutativeSemiring : CommutativeSemiring _ _
    R-commutativeSemiring = record { isCommutativeSemiring = R-isCommutativeSemiring }

  open IsCommutativeSemiring R-isCommutativeSemiring

  isSemimodule
    : IsSemimodule R-commutativeSemiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
    → IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
  isSemimodule isSemimodule = record
    { isBisemimodule = isBisemimodule isSemiring isSemiring NN.isBisemimodule
    ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident
    }
    where
      module NN = IsSemimodule isSemimodule