Skip to content

Commit dc8f69e

Browse files
LorenzoMolenahexwell
LorenzoMolena
and
hexwell
authored
Definition of OrderedCommRing (#1246)
* Definition of `OrderedCommRing` Co-authored-by: Lorenzo Molena <[email protected]> * namespace work * add `<-≤-weaken` to `OrderedCommRing` --------- Co-authored-by: Ettore Forigo <[email protected]>
1 parent 629503a commit dc8f69e

File tree

4 files changed

+201
-0
lines changed

4 files changed

+201
-0
lines changed

‎Cubical/Algebra/OrderedCommRing.agda‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
module Cubical.Algebra.OrderedCommRing where
2+
3+
open import Cubical.Algebra.OrderedCommRing.Base public

‎Cubical/Algebra/OrderedCommRing/Base.agda‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
module Cubical.Algebra.OrderedCommRing.Base where
2+
{-
3+
Definition of an commutative ordered ring.
4+
-}
5+
6+
open import Cubical.Foundations.Prelude
7+
open import Cubical.Foundations.Equiv
8+
open import Cubical.Foundations.SIP
9+
10+
import Cubical.Functions.Logic as L
11+
12+
open import Cubical.Relation.Nullary.Base
13+
14+
open import Cubical.Algebra.CommRing.Base
15+
16+
open import Cubical.Relation.Binary.Base
17+
open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice)
18+
open import Cubical.Relation.Binary.Order.StrictOrder
19+
20+
open import Cubical.Relation.Binary.Order.Pseudolattice
21+
22+
open BinaryRelation
23+
24+
private
25+
variable
26+
ℓ ℓ' : Level
27+
28+
record IsOrderedCommRing
29+
{R : Type ℓ}
30+
(0r 1r : R )
31+
(_+_ _·_ : R → R → R)
32+
(-_ : R → R)
33+
(_<_ _≤_ : R → R → Type ℓ') : Type (ℓ-max ℓ ℓ') where
34+
constructor isorderedcommring
35+
field
36+
isCommRing : IsCommRing 0r 1r _+_ _·_ -_
37+
isPseudolattice : IsPseudolattice _≤_
38+
isStrictOrder : IsStrictOrder _<_
39+
<-≤-weaken : ∀ x y → x < y → x ≤ y
40+
≤≃¬> : ∀ x y → (x ≤ y) ≃ (¬ (y < x))
41+
+MonoR≤ : ∀ x y z → x ≤ y → (x + z) ≤ (y + z)
42+
+MonoR< : ∀ x y z → x < y → (x + z) < (y + z)
43+
posSum→pos∨pos : ∀ x y → 0r < (x + y) → (0r < x) L.⊔′ (0r < y)
44+
<-≤-trans : ∀ x y z → x < y → y ≤ z → x < z
45+
≤-<-trans : ∀ x y z → x ≤ y → y < z → x < z
46+
·MonoR≤ : ∀ x y z → 0r ≤ z → x ≤ y → (x · z) ≤ (y · z)
47+
·MonoR< : ∀ x y z → 0r < z → x < y → (x · z) < (y · z)
48+
0<1 : 0r < 1r
49+
50+
open IsCommRing isCommRing public
51+
open IsPseudolattice isPseudolattice hiding (is-set) renaming (is-prop-valued to is-prop-valued≤ ; is-trans to is-trans≤
52+
; isPseudolattice to is-pseudolattice
53+
; _∧l_ to _⊓_ ; _∨l_ to _⊔_) public
54+
open IsStrictOrder isStrictOrder hiding (is-set) renaming (is-prop-valued to is-prop-valued< ; is-trans to is-trans<) public
55+
56+
record OrderedCommRingStr (ℓ' : Level) (R : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
57+
constructor orderedcommringstr
58+
field
59+
0r 1r : R
60+
_+_ _·_ : R → R → R
61+
-_ : R → R
62+
_<_ _≤_ : R → R → Type ℓ'
63+
isOrderedCommRing : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
64+
65+
open IsOrderedCommRing isOrderedCommRing public
66+
67+
infix 8 -_
68+
infixl 7 _·_
69+
infixl 6 _+_
70+
infix 4 _<_ _≤_
71+
72+
OrderedCommRing : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
73+
OrderedCommRing ℓ ℓ' = TypeWithStr ℓ (OrderedCommRingStr ℓ')
74+
75+
module _ {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R }
76+
{_<_ _≤_ : R → R → Type ℓ'}
77+
(is-setR : isSet R)
78+
(+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
79+
(+IdR : (x : R) → x + 0r ≡ x)
80+
(+InvR : (x : R) → x + (- x) ≡ 0r)
81+
(+Comm : (x y : R) → x + y ≡ y + x)
82+
(·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
83+
(·IdR : (x : R) → x · 1r ≡ x)
84+
(·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
85+
(·Comm : (x y : R) → x · y ≡ y · x)
86+
(is-prop-valued≤ : isPropValued _≤_)
87+
(is-refl : isRefl _≤_)
88+
(is-trans≤ : isTrans _≤_)
89+
(is-antisym : isAntisym _≤_)
90+
(is-meet-semipseudolattice : isMeetSemipseudolattice (poset R _≤_ (isposet is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym)))
91+
(is-join-semipseudolattice : isJoinSemipseudolattice (poset R _≤_ (isposet is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym)))
92+
(is-prop-valued : isPropValued _<_)
93+
(is-irrefl : isIrrefl _<_)
94+
(is-trans : isTrans _<_)
95+
(is-asym : isAsym _<_)
96+
(is-weakly-linear : isWeaklyLinear _<_)
97+
(<-≤-weaken : ∀ x y → x < y → x ≤ y)
98+
(≤≃¬> : ∀ x y → (x ≤ y) ≃ (¬ (y < x)))
99+
(+MonoR≤ : ∀ x y z → x ≤ y → (x + z) ≤ (y + z))
100+
(+MonoR< : ∀ x y z → x < y → (x + z) < (y + z))
101+
(posSum→pos∨pos : ∀ x y → 0r < (x + y) → 0r < x L.⊔′ 0r < y)
102+
(<-≤-trans : ∀ x y z → x < y → y ≤ z → x < z)
103+
(≤-<-trans : ∀ x y z → x ≤ y → y < z → x < z)
104+
(·MonoR≤ : ∀ x y z → 0r ≤ z → x ≤ y → (x · z) ≤ (y · z))
105+
(·MonoR< : ∀ x y z → 0r < z → x < y → (x · z) < (y · z))
106+
(0<1 : 0r < 1r) where
107+
makeIsOrderedCommRing : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
108+
makeIsOrderedCommRing = OCR where
109+
OCR : IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_
110+
IsOrderedCommRing.isCommRing OCR = makeIsCommRing
111+
is-setR +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistR+ ·Comm
112+
IsOrderedCommRing.isPseudolattice OCR = makeIsPseudolattice
113+
is-setR is-prop-valued≤ is-refl is-trans≤ is-antisym
114+
is-meet-semipseudolattice is-join-semipseudolattice
115+
IsOrderedCommRing.isStrictOrder OCR =
116+
isstrictorder is-setR is-prop-valued is-irrefl is-trans is-asym is-weakly-linear
117+
IsOrderedCommRing.<-≤-weaken OCR = <-≤-weaken
118+
IsOrderedCommRing.≤≃¬> OCR = ≤≃¬>
119+
IsOrderedCommRing.+MonoR≤ OCR = +MonoR≤
120+
IsOrderedCommRing.+MonoR< OCR = +MonoR<
121+
IsOrderedCommRing.posSum→pos∨pos OCR = posSum→pos∨pos
122+
IsOrderedCommRing.<-≤-trans OCR = <-≤-trans
123+
IsOrderedCommRing.≤-<-trans OCR = ≤-<-trans
124+
IsOrderedCommRing.·MonoR≤ OCR = ·MonoR≤
125+
IsOrderedCommRing.·MonoR< OCR = ·MonoR<
126+
IsOrderedCommRing.0<1 OCR = 0<1
127+
128+
OrderedCommRing→PseudoLattice : OrderedCommRing ℓ ℓ' → Pseudolattice ℓ ℓ'
129+
OrderedCommRing→PseudoLattice R .fst = R .fst
130+
OrderedCommRing→PseudoLattice R .snd = pseudolatticestr _ isPseudolattice where
131+
open OrderedCommRingStr (str R)
132+
133+
OrderedCommRing→CommRing : OrderedCommRing ℓ ℓ' → CommRing ℓ
134+
OrderedCommRing→CommRing R .fst = R .fst
135+
OrderedCommRing→CommRing R .snd = commringstr _ _ _ _ _ isCommRing where
136+
open OrderedCommRingStr (str R)

‎Cubical/Relation/Binary/Order/Pseudolattice.agda‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
module Cubical.Relation.Binary.Order.Pseudolattice where
2+
3+
open import Cubical.Relation.Binary.Order.Pseudolattice.Base public

‎Cubical/Relation/Binary/Order/Pseudolattice/Base.agda‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
module Cubical.Relation.Binary.Order.Pseudolattice.Base where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.SIP
5+
6+
open import Cubical.Relation.Binary.Base
7+
open import Cubical.Relation.Binary.Order.Poset renaming (isPseudolattice to pseudolattice)
8+
open import Cubical.Relation.Binary.Order.StrictOrder
9+
10+
open BinaryRelation
11+
12+
private
13+
variable
14+
ℓ ℓ' : Level
15+
16+
record IsPseudolattice {L : Type ℓ} (_≤_ : L → L → Type ℓ') : Type (ℓ-max ℓ ℓ') where
17+
constructor ispseudolattice
18+
19+
field
20+
isPoset : IsPoset _≤_
21+
isPseudolattice : pseudolattice (poset L _≤_ isPoset)
22+
23+
open IsPoset isPoset public
24+
25+
_∧l_ : L → L → L
26+
a ∧l b = (isPseudolattice .fst a b) .fst
27+
28+
_∨l_ : L → L → L
29+
a ∨l b = (isPseudolattice .snd a b) .fst
30+
31+
infixl 7 _∧l_
32+
infixl 6 _∨l_
33+
34+
record PseudolatticeStr (ℓ' : Level) (L : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
35+
constructor pseudolatticestr
36+
37+
field
38+
_≤_ : L → L → Type ℓ'
39+
is-pseudolattice : IsPseudolattice _≤_
40+
41+
open IsPseudolattice is-pseudolattice public
42+
43+
Pseudolattice : ∀ ℓ ℓ' → Type (ℓ-suc (ℓ-max ℓ ℓ'))
44+
Pseudolattice ℓ ℓ' = TypeWithStr ℓ (PseudolatticeStr ℓ')
45+
46+
makeIsPseudolattice : {L : Type ℓ} {_≤_ : L → L → Type ℓ'}
47+
(is-setL : isSet L)
48+
(is-prop-valued : isPropValued _≤_)
49+
(is-refl : isRefl _≤_)
50+
(is-trans : isTrans _≤_)
51+
(is-antisym : isAntisym _≤_)
52+
(is-meet-semipseudolattice : isMeetSemipseudolattice (poset L _≤_ (isposet is-setL is-prop-valued is-refl is-trans is-antisym)))
53+
(is-join-semipseudolattice : isJoinSemipseudolattice (poset L _≤_ (isposet is-setL is-prop-valued is-refl is-trans is-antisym)))
54+
→ IsPseudolattice _≤_
55+
makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-antisym is-meet-semipseudolattice is-join-semipseudolattice = PS
56+
where
57+
PS : IsPseudolattice _≤_
58+
PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
59+
PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice

0 commit comments

Comments
 (0)