------------------------------------------------------------------------
-- 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
infixr
4
_,_
infix
5
_∣ˡ_
_∤ˡ_
_∣ʳ_
_∤ʳ_
_∣_
_∤_
_∥_
_∦_
-- 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.Properties.X.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
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.3
_∣∣_
=
_∥_
{-#
WARNING_ON_USAGE
_∣∣_
"Warning: _∣∣_ was deprecated in v2.3. Please use _∥_ instead."
#-}
_∤∤_
=
_∦_
{-#
WARNING_ON_USAGE
_∤∤_
"Warning: _∤∤_ was deprecated in v2.3. Please use _∦_ instead."
#-}