-- The Agda standard library
-- Properties of semimodules.

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

open import Algebra                using (CommutativeSemiring)
open import Algebra.Module.Bundles using (Semimodule)
open import Level                  using (Level)

module Algebra.Module.Properties.Semimodule
  {r ℓr m ℓm : Level}
  {semiring  : CommutativeSemiring r ℓr}
  (semimod   : Semimodule semiring m ℓm)

open CommutativeSemiring semiring
open Semimodule          semimod
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid

x≈0⇒x*y≈0 :  {x y}  x  0#  x *ₗ y ≈ᴹ 0ᴹ
x≈0⇒x*y≈0 {x} {y} x≈0 = begin
  x  *ₗ y ≈⟨ *ₗ-congʳ x≈0 
  0# *ₗ y ≈⟨ *ₗ-zeroˡ y 

y≈0⇒x*y≈0 :  {x y}  y ≈ᴹ 0ᴹ  x *ₗ y ≈ᴹ 0ᴹ
y≈0⇒x*y≈0 {x} {y} y≈0 = begin
  x *ₗ y  ≈⟨ *ₗ-congˡ y≈0 
  x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x 

x*y≉0⇒x≉0 :  {x y}  x *ₗ y ≉ᴹ 0ᴹ  x  0#
x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0

x*y≉0⇒y≉0 :  {x y}  x *ₗ y ≉ᴹ 0ᴹ  y ≉ᴹ 0ᴹ
x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0