------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic auxiliary definitions for magma-like structures
------------------------------------------------------------------------

-- You're unlikely to want to use this module directly. Instead you
-- probably want to be importing the appropriate module from
-- `Algebra.Properties.(Magma/Semigroup/...).Divisibility`

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

open import Algebra.Bundles using (RawMagma)
open import Data.Product.Base using (_×_; ∃)
open import Level using (_⊔_)
open import Relation.Binary.Core
open import Relation.Nullary.Negation using (¬_)

module Algebra.Definitions.RawMagma
  {a ℓ} (M : RawMagma a ℓ)
  where

open RawMagma M renaming (Carrier to A)

------------------------------------------------------------------------
-- Divisibility

infix  _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_

-- Divisibility from the left.
--
-- This and, the definition of right divisibility below, are defined as
-- records rather than in terms of the base product type in order to
-- make the use of pattern synonyms more ergonomic (see #2216 for
-- further details). The record field names are not designed to be
-- used explicitly and indeed aren't re-exported publicly by
-- `Algebra.X.Properties.Divisibility` modules.

record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where
  constructor _,_
  field
    quotient : A
    equality : x ∙ quotient ≈ y

_∤ˡ_ : Rel A (a ⊔ ℓ)
x ∤ˡ y = ¬ x ∣ˡ y

-- Divisibility from the right

record _∣ʳ_ (x y : A) : Set (a ⊔ ℓ) where
  constructor _,_
  field
    quotient : A
    equality : quotient ∙ x ≈ y

_∤ʳ_ : Rel A (a ⊔ ℓ)
x ∤ʳ y = ¬ x ∣ʳ y

-- General divisibility

-- The relations _∣ˡ_ and _∣ʳ_ are only equivalent when _∙_ is
-- commutative. When that is not the case we take `_∣ʳ_` to be the
-- primary one.

_∣_ : Rel A (a ⊔ ℓ)
_∣_ = _∣ʳ_

_∤_ : Rel A (a ⊔ ℓ)
x ∤ y = ¬ x ∣ y

------------------------------------------------------------------------
-- Mutual divisibility.

-- In a  monoid, this is an equivalence relation extending _≈_.
-- When in a cancellative monoid,  elements related by _∣∣_ are called
-- associated, and `x ∣∣ y` means that `x` and `y` differ by some
-- invertible factor.

-- Example: for ℕ  this is equivalent to x ≡ y,
--          for ℤ  this is equivalent to (x ≡ y or x ≡ - y).

_∣∣_ : Rel A (a ⊔ ℓ)
x ∣∣ y = x ∣ y × y ∣ x

_∤∤_ : Rel A (a ⊔ ℓ)
x ∤∤ y = ¬ x ∣∣ y