-
Notifications
You must be signed in to change notification settings - Fork 234
/
RawMagma.agda
73 lines (51 loc) · 2.04 KB
/
RawMagma.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
------------------------------------------------------------------------
-- 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 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_
-- Divisibility from the left
_∣ˡ_ : Rel A (a ⊔ ℓ)
x ∣ˡ y = ∃ λ q → (x ∙ q) ≈ y
_∤ˡ_ : Rel A (a ⊔ ℓ)
x ∤ˡ y = ¬ x ∣ˡ y
-- Divisibility from the right
_∣ʳ_ : Rel A (a ⊔ ℓ)
x ∣ʳ y = ∃ λ q → (q ∙ 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