------------------------------------------------------------------------
-- 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.Raw using (RawMagma)
open import Data.Product.Base using (_×_; ∃)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Negation.Core 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