patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-12 23:28:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

Total order on the rationals (#17)

Browse Source
This commit is contained in:
Patrick Stevens
2019-01-13 12:05:30 +00:00
committed by GitHub
parent 9e22ba78f5
commit 2866b11be6
9 changed files with 624 additions and 52 deletions
Download Patch File Download Diff File Expand all files Collapse all files

38
Fields/FieldOfFractions.agda
View File

@@ -2,6 +2,7 @@
open import LogicalFormulae open import LogicalFormulae
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
open import Groups.GroupsLemmas open import Groups.GroupsLemmas
open import Rings.RingDefinition open import Rings.RingDefinition
open import Rings.RingLemmas open import Rings.RingLemmas
@@ -9,7 +10,6 @@ open import Rings.IntegralDomains
open import Fields.Fields open import Fields.Fields
open import Functions open import Functions
open import Setoids.Setoids open import Setoids.Setoids
open import Setoids.Orders
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
@@ -229,39 +229,3 @@ module Fields.FieldOfFractions where
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S)) open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S)) open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S)) open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsNonnegDenom : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → (a1 : fieldOfFractionsSet I) → Sg (fieldOfFractionsSet I) (λ b1 → (Setoid._∼_ (fieldOfFractionsSetoid I) a1 b1) && ((Ring.0R R) < underlying (_&&_.snd b1)))
fieldOfFractionsNonnegDenom {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denom
fieldOfFractionsNonnegDenom {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inl (inl 0<denom) = (num ,, (denom , denom!=0)) , ((Ring.multCommutative R) ,, 0<denom)
fieldOfFractionsNonnegDenom {S = S} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inl (inr denom<0) = ((Group.inverse (Ring.additiveGroup R) num ,, (Group.inverse (Ring.additiveGroup R) denom , λ p → denom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (transitive (symmetric (Group.invLeft (Ring.additiveGroup R) {denom})) (transitive (Group.wellDefined (Ring.additiveGroup R) p reflexive) (Group.multIdentLeft (Ring.additiveGroup R)))))))) , (transitive (ringMinusExtracts R) (transitive (inverseWellDefined (Ring.additiveGroup R) (Ring.multCommutative R)) (symmetric (ringMinusExtracts R))) ,, ringMinusFlipsOrder' order (SetoidPartialOrder.wellDefined pOrder (symmetric (invInv (Ring.additiveGroup R))) reflexive denom<0))
where
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Ring R
open Group additiveGroup
fieldOfFractionsNonnegDenom {S = S} {R = R} {tOrder = tOrder} I order (num ,, (denom , denom!=0)) | inr 0=denom = exFalso (denom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denom))
fieldOfFractionsComparison : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → Rel (fieldOfFractionsSet I)
fieldOfFractionsComparison {_*_ = _*_} {R = R} {_<_ = _<_} {tOrder = tOrder} I oring x y with fieldOfFractionsNonnegDenom I oring x
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} I oring x y | (numA ,, (denomA , _)) , b with fieldOfFractionsNonnegDenom I oring y
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} I oring x y | (numA ,, (denomA , _)) , prA | (numB ,, (denomB , _)) , prB = (numA * denomB) < (numB * denomA)
fieldOfFractionsOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidPartialOrder (fieldOfFractionsSetoid I) (fieldOfFractionsComparison I order)
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_ = _+_} {_*_ = _*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c with fieldOfFractionsNonnegDenom I order x
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) with fieldOfFractionsNonnegDenom I order z
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) with fieldOfFractionsNonnegDenom I order w
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {w} {x} {y} {z} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) | (numW ,, (denomW , denomW!=0)) , (numW/denomW ,, 0<denomW) with fieldOfFractionsNonnegDenom I order y
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder {S = S} {_+_} {_*_} {_<_ = _<_} I order) {numW' ,, (denomW' , denomW'!=0)} {numX' ,, (denomX' , denomX'!=0)} {numY' ,, (denomY' , denomY'!=0)} {numZ' ,, (denomZ' , denomZ'!=0)} a~b c~d a<c | (numX ,, (denomX , denomX!=0)) , (x~numX/denomX ,, 0<denomX) | (numZ ,, (denomZ , denomZ!=0)) , (numZ/denomZ ,, 0<denomZ) | (numW ,, (denomW , denomW!=0)) , (numW/denomW ,, 0<denomW) | (numY ,, (denomY , denomY!=0)) , (numY/denomY ,, 0<denomY) = {!!}
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {x} x<x with fieldOfFractionsNonnegDenom I oRing x
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {x} x<x | (numA ,, (denomA , _)) , pr with fieldOfFractionsNonnegDenom I oRing x
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {fst₁ ,, (a , a!=0)} x<x | (numA ,, (denomA , _)) , (fst₂ ,, 0<denomA) | (numA' ,, (denomA' , _)) , (fst ,, 0<denomA') = {!!}
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order) {numA ,, (denomA , _)} {(numB ,, (denomB , _))} {numC ,, (denomC , _)} a<b b<c = {!!}
fieldOfFractionsTotalOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidTotalOrder (fieldOfFractionsOrder I order)
fieldOfFractionsTotalOrder I order = {!!}
fieldOfFractionsOrderedRing : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → OrderedRing (fieldOfFractionsRing I) (fieldOfFractionsTotalOrder I order)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing I order) a<b c = {!!}
OrderedRing.orderRespectsMultiplication (fieldOfFractionsOrderedRing {_+_ = _+_} {_*_ = _*_} {_<_ = _<_} I order) {numA ,, (denomA , _)} {numB ,, (denomB , _)} 0<a 0<b = {!!}

425
Fields/FieldOfFractionsOrder.agda Normal file
View File

@@ -0,0 +1,425 @@
{-# OPTIONS --safe --warning=error #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.GroupDefinition
open import Groups.GroupsLemmas
open import Rings.RingDefinition
open import Rings.RingLemmas
open import Rings.IntegralDomains
open import Fields.Fields
open import Functions
open import Setoids.Setoids
open import Setoids.Orders
open import Fields.FieldOfFractions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Fields.FieldOfFractionsOrder where
fieldOfFractionsComparison : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → Rel (fieldOfFractionsSet I)
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) = (numA * denomB) < (numB * denomA)
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) = (numB * denomA) < (numA * denomB)
fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) = (numB * denomA) < (numA * denomB)
fieldOfFractionsComparison {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) = (numA * denomB) < (numB * denomA)
fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsComparison {S = S} {_*_ = _*_} {R} {_<_} {tOrder = tOrder} i oring (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inr 0=denomA = exFalso (denomA!=0 (symmetric 0=denomA))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison I order x y → Setoid._∼_ (fieldOfFractionsSetoid I) x z → fieldOfFractionsComparison I order z y
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} I order {(numX ,, (denomX , denomX!=0))} {(numY ,, (denomY , denomY!=0))} {(numZ ,, (denomZ , denomZ!=0))} x<y x=z with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inl _) = s
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
have = ringCanMultiplyByPositive order 0<denomZ x<y
p : ((numX * denomZ) * denomY) < ((numY * denomX) * denomZ)
p = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive have
q : ((denomX * numZ) * denomY) < ((numY * denomX) * denomZ)
q = SetoidPartialOrder.wellDefined pOrder (multWellDefined x=z reflexive) reflexive p
r : ((numZ * denomY) * denomX) < ((numY * denomZ) * denomX)
r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) multCommutative) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) q
s : (numZ * denomY) < (numY * denomZ)
s = ringCanCancelPositive order 0<denomX r
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (symmetric x))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inl _) = ringCanCancelNegative order denomX<0 r
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
p : ((numY * denomX) * denomZ) < ((numX * denomZ) * denomY)
p = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y)
q : ((numY * denomX) * denomZ) < ((denomX * numZ) * denomY)
q = SetoidPartialOrder.wellDefined pOrder reflexive (multWellDefined x=z reflexive) p
r : ((numY * denomZ) * denomX) < ((numZ * denomY) * denomX)
r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) multCommutative) q
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inl 0<denomY) | inr 0=denomX = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomX))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inr _) = ringCanCancelPositive order 0<denomX r
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
p : ((numY * denomX) * denomZ) < ((numX * denomY) * denomZ)
p = ringCanMultiplyByPositive order 0<denomZ x<y
q : ((numY * denomX) * denomZ) < ((denomX * numZ) * denomY)
q = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (multWellDefined x=z reflexive)))) p
r : ((numY * denomZ) * denomX) < ((numZ * denomY) * denomX)
r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) multCommutative) q
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inr _) = ringCanCancelNegative order denomX<0 q
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
p : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
p = ringCanMultiplyByPositive order 0<denomZ x<y
q : ((numZ * denomY) * denomX) < ((numY * denomZ) * denomX)
q = SetoidPartialOrder.wellDefined pOrder (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive multCommutative (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) p
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inl (inr denomY<0) | inr 0=denomX = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomX))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) | inr 0=denomY = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomY))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inl _) = ringCanCancelPositive order 0<denomX (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive (multWellDefined reflexive (multCommutative)) (transitive multAssoc (multWellDefined multCommutative reflexive))))) p)
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
p : ((numY * denomX) * denomZ) < ((denomY * numX) * denomZ)
p = ringCanMultiplyByNegative order denomZ<0 (SetoidPartialOrder.wellDefined pOrder multCommutative reflexive x<y)
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inl (inr denomY<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inl _) = ringCanCancelNegative order denomX<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined x=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) p)
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
p : ((numX * denomY) * denomZ) < ((numY * denomX) * denomZ)
p = ringCanMultiplyByNegative order denomZ<0 x<y
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inl (inr denomY<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder denomY<0 0<denomY))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inl (inr denomX<0) | inr 0=denomY = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=denomY))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inl 0<denomY) | inr x = exFalso (denomX!=0 (symmetric x))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inl (inr _) = ringCanCancelPositive order 0<denomX (SetoidPartialOrder.wellDefined pOrder (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive multAssoc (transitive multCommutative multAssoc))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inl 0<denomX) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inl 0<denomY) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomY denomY<0))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inl (inr _) = ringCanCancelNegative order denomX<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (multWellDefined multCommutative reflexive) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive x=z) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (multWellDefined multCommutative reflexive)))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inl (inr denomX<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inl (inr denomY<0) | inr x = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (symmetric x))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedLeft {S = S} {_*_ = _*_} {R} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inr 0=denomZ = exFalso (denomZ!=0 (symmetric 0=denomZ))
where
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison I order x y → Setoid._∼_ (fieldOfFractionsSetoid I) y z → fieldOfFractionsComparison I order x z
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z with SetoidTotalOrder.totality tOrder (Ring.0R R) denomX
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByPositive order 0<denomZ x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inl 0<denomZ) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive (multAssoc) (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) | inr x = exFalso (denomZ!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomZ
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive order 0<denomZ x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByPositive order 0<denomZ x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inl 0<denomZ) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomY
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inl (inl 0<denomY) = ringCanCancelPositive order 0<denomY (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inl (inr denomY<0) = ringCanCancelNegative order denomY<0 (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) (transitive multAssoc (transitive (multWellDefined y=z reflexive) (transitive (symmetric multAssoc) multCommutative))))) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByNegative order denomZ<0 x<y))
where
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inl (inr denomZ<0) | inr x = exFalso (denomY!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inr denomX<0) | inr x = exFalso (denomZ!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsOrderWellDefinedRight {S = S} {_*_ = _*_} {R} {pOrder = pOrder} {tOrder} I order {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inr x = exFalso (denomX!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
swapLemma : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) {x y z : A} → Setoid._∼_ S ((x * y) * z) ((x * z) * y)
swapLemma {S = S} R = transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
fieldOfFractionsOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidPartialOrder (fieldOfFractionsSetoid I) (fieldOfFractionsComparison I order)
SetoidPartialOrder.wellDefined (fieldOfFractionsOrder I oRing) {a} {b} {c} {d} a=b c=d a<c = fieldOfFractionsOrderWellDefinedRight I oRing {b} {c} {d} (fieldOfFractionsOrderWellDefinedLeft I oRing {a} {c} {b} a<c a=b) c=d
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inl (inl _) = SetoidPartialOrder.irreflexive pOrder pr
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inl (inr aDenom<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<aDenom aDenom<0))
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) aDenom
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inl 0<aDenom) = SetoidPartialOrder.irreflexive pOrder pr
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inl (inr _) = SetoidPartialOrder.irreflexive pOrder pr
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inr aDenom<0) | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {aNum ,, (aDenom , aDenom!=0)} pr | inr x = exFalso (aDenom!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder = tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl x) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inl _) = ringCanCancelPositive oRing 0<denomB p
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
inter : ((numA * denomB) * denomC) < ((numB * denomA) * denomC)
inter = ringCanMultiplyByPositive oRing 0<denomC a<b
p : ((numA * denomC) * denomB) < ((numC * denomA) * denomB)
p = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive inter) (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive oRing 0<denomA b<c))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inl _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) reflexive (ringCanMultiplyByPositive oRing 0<denomA b<c)) (SetoidPartialOrder.wellDefined pOrder (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (transitive (symmetric multAssoc) (transitive (multWellDefined reflexive multCommutative) multAssoc)) (ringCanMultiplyByPositive oRing 0<denomC a<b)))
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inl 0<denomC) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inr _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomC<0 a<b)))
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numC * denomA) * denomB) < ((numB * denomC) * denomA)
have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive oRing 0<denomA b<c)
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
... | (inl (inl 0<denomC)) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
... | (inl (inr _)) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByPositive oRing 0<denomA b<c)))
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative oRing denomC<0 a<b)
... | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inl (inr denomC<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inl 0<denomA) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inl _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)) have)
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
have = SetoidPartialOrder.wellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByPositive oRing 0<denomC a<b)
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inl _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)))
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByPositive oRing 0<denomC a<b)
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inl (inr denomC<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {a} {b} {c} {A} {S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inl 0<denomC) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inl (inr _) = ringCanCancelPositive oRing 0<denomB (SetoidPartialOrder.transitive pOrder have (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)))
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numA * denomC) * denomB) < ((numB * denomA) * denomC)
have = SetoidPartialOrder.wellDefined pOrder (swapLemma R) reflexive (ringCanMultiplyByNegative oRing denomC<0 a<b)
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inl 0<denomB) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomC
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inl (inl 0<denomC) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomC denomC<0))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {_*_ = _*_} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inl (inr _) = ringCanCancelNegative oRing denomB<0 (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.wellDefined pOrder (swapLemma R) (swapLemma R) (ringCanMultiplyByNegative oRing denomA<0 b<c)) have)
where
open Setoid S
open Ring R
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
have : ((numB * denomA) * denomC) < ((numA * denomC) * denomB)
have = SetoidPartialOrder.wellDefined pOrder reflexive (swapLemma R) (ringCanMultiplyByNegative oRing denomC<0 a<b)
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inl (inr denomB<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inl (inr denomC<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inl (inr denomA<0) | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidPartialOrder.transitive (fieldOfFractionsOrder {S = S} {R = R} {pOrder = pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} {numC ,, (denomC , denomC!=0)} a<b b<c | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
fieldOfFractionsTotalOrder : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → SetoidTotalOrder (fieldOfFractionsOrder I order)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) with SetoidTotalOrder.totality tOrder (numA * denomB) (numB * denomA)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inl (inl x) = inl (inl x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inl (inr x) = inl (inr x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inl _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) x (Ring.multCommutative R))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inl (inr denomA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) with SetoidTotalOrder.totality tOrder (numB * denomA) (numA * denomB)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inl (inl x) = inl (inl x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inl (inr x) = inl (inr x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inl _) | inr x = inr (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) (Ring.multCommutative R) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inl (inr denomA<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inl 0<denomA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) with SetoidTotalOrder.totality tOrder (numB * denomA) (numA * denomB)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inl (inl x) = inl (inl x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inl (inr x) = inl (inr x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inl (inr _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x) (Ring.multCommutative R))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inl 0<denomB) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inl 0<denomA) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder 0<denomA denomA<0))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) with SetoidTotalOrder.totality tOrder (numA * denomB) (numB * denomA)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inl (inl x) = inl (inl x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inl (inr x) = inl (inr x)
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inl (inr _) | inr x = inr (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) x (Ring.multCommutative R))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inl (inr denomB<0) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inr denomA<0) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
SetoidTotalOrder.totality (fieldOfFractionsTotalOrder {S = S} {_*_ = _*_} {R} {_<_} {pOrder} {tOrder} I oRing) (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
{-
fieldOfFractionsOrderedRing : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (I : IntegralDomain R) → (order : OrderedRing R tOrder) → OrderedRing (fieldOfFractionsRing I) (fieldOfFractionsTotalOrder I order)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) with SetoidTotalOrder.totality tOrder (Ring.0R R) (denomA * denomC)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) with SetoidTotalOrder.totality tOrder (Ring.0R R) (denomB * denomC)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomA
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) with SetoidTotalOrder.totality tOrder (Ring.0R R) denomB
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inl 0<dB) = {!!}
where
open Ring R
0<dC : 0R < denomC
0<dC with SetoidTotalOrder.totality tOrder 0R denomC
0<dC | inl (inl x) = x
0<dC | inl (inr dC<0) = {!!}
0<dC | inr x = exFalso (denomC!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inl (inr dB<0) = {!!}
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inl 0<dA) | inr x = exFalso (denomB!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inl (inr dA<0) = {!!}
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) | inr x = exFalso (denomA!=0 (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x))
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inr dBdC<0) = {!!}
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC with IntegralDomain.intDom I (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=dBdC)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC | inl x = exFalso (denomB!=0 x)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inr 0=dBdC | inr x = exFalso (denomC!=0 x)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inr dAdC<0) = {!!}
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr (0=dAdC) with IntegralDomain.intDom I (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) 0=dAdC)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr 0=dAdC | inl x = exFalso (denomA!=0 x)
OrderedRing.orderRespectsAddition (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inr 0=dAdC | inr x = exFalso (denomC!=0 x)
OrderedRing.orderRespectsMultiplication (fieldOfFractionsOrderedRing {S = S} {_+_} {_*_} {R} {_<_} {pOrder} {tOrder} I oRing) = {!!}
-}

44
Fields/Fields.agda
View File

@@ -2,8 +2,11 @@
open import LogicalFormulae open import LogicalFormulae
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
open import Rings.RingDefinition open import Rings.RingDefinition
open import Rings.RingLemmas
open import Setoids.Setoids open import Setoids.Setoids
open import Setoids.Orders
open import Orders open import Orders
open import Rings.IntegralDomains open import Rings.IntegralDomains
open import Functions open import Functions
@@ -19,6 +22,47 @@ module Fields.Fields where
allInvertible : (a : A) → ((a ∼ Group.identity (Ring.additiveGroup R)) → False) → Sg A (λ t → t * a ∼ 1R) allInvertible : (a : A) → ((a ∼ Group.identity (Ring.additiveGroup R)) → False) → Sg A (λ t → t * a ∼ 1R)
nontrivial : (0R ∼ 1R) → False nontrivial : (0R ∼ 1R) → False
orderedFieldIsIntDom : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (O : OrderedRing R tOrder) (F : Field R) → IntegralDomain R
IntegralDomain.intDom (orderedFieldIsIntDom {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} O F) {a} {b} ab=0 with SetoidTotalOrder.totality tOrder (Ring.0R R) a
IntegralDomain.intDom (orderedFieldIsIntDom {A = A} {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} O F) {a} {b} ab=0 | inl (inl x) = inr (transitive (transitive (symmetric multIdentIsIdent) (multWellDefined q reflexive)) p')
where
open Setoid S
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Ring R
a!=0 : (a ∼ Group.identity additiveGroup) → False
a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (symmetric pr) reflexive x)
invA : A
invA = underlying (Field.allInvertible F a a!=0)
q : 1R ∼ (invA * a)
q with Field.allInvertible F a a!=0
... | invA , pr = symmetric pr
p : invA * (a * b) ∼ invA * Group.identity additiveGroup
p = multWellDefined reflexive ab=0
p' : (invA * a) * b ∼ Group.identity additiveGroup
p' = transitive (symmetric multAssoc) (transitive p (ringTimesZero R))
IntegralDomain.intDom (orderedFieldIsIntDom {A = A} {S = S} {_*_ = _*_} {R = R} {pOrder = pOrder} {tOrder = tOrder} O F) {a} {b} ab=0 | inl (inr x) = inr (transitive (transitive (symmetric multIdentIsIdent) (multWellDefined q reflexive)) p')
where
open Setoid S
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Ring R
a!=0 : (a ∼ Group.identity additiveGroup) → False
a!=0 pr = SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder reflexive (symmetric pr) x)
invA : A
invA = underlying (Field.allInvertible F a a!=0)
q : 1R ∼ (invA * a)
q with Field.allInvertible F a a!=0
... | invA , pr = symmetric pr
p : invA * (a * b) ∼ invA * Group.identity additiveGroup
p = multWellDefined reflexive ab=0
p' : (invA * a) * b ∼ Group.identity additiveGroup
p' = transitive (symmetric multAssoc) (transitive p (ringTimesZero R))
IntegralDomain.intDom (orderedFieldIsIntDom {S = S} {_*_ = _*_} {R = R} {tOrder = tOrder} O F) {a} {b} ab=0 | inr x = inl (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) x)
IntegralDomain.nontrivial (orderedFieldIsIntDom {S = S} O F) pr = Field.nontrivial F (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) pr)
record Field' {m n : _} : Set (lsuc m ⊔ lsuc n) where record Field' {m n : _} : Set (lsuc m ⊔ lsuc n) where
field field
A : Set m A : Set m

22
Groups/GroupDefinition.agda Normal file
View File

@@ -0,0 +1,22 @@
{-# OPTIONS --safe --warning=error #-}
open import LogicalFormulae
open import Setoids.Setoids
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals
open import Sets.FinSet
module Groups.GroupDefinition where
record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where
open Setoid S
field
wellDefined : {m n x y : A} → (m ∼ x) → (n ∼ y) → (m · n) ∼ (x · y)
identity : A
inverse : A → A
multAssoc : {a b c : A} → (a · (b · c)) ∼ (a · b) · c
multIdentRight : {a : A} → (a · identity) ∼ a
multIdentLeft : {a : A} → (identity · a) ∼ a
invLeft : {a : A} → (inverse a) · a ∼ identity
invRight : {a : A} → a · (inverse a) ∼ identity

20
Groups/Groups.agda
View File

@@ -6,19 +6,9 @@ open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals open import Numbers.Naturals
open import Sets.FinSet open import Sets.FinSet
open import Groups.GroupDefinition
module Groups.Groups where module Groups.Groups where
record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where
open Setoid S
field
wellDefined : {m n x y : A} → (m ∼ x) → (n ∼ y) → (m · n) ∼ (x · y)
identity : A
inverse : A → A
multAssoc : {a b c : A} → (a · (b · c)) ∼ (a · b) · c
multIdentRight : {a : A} → (a · identity) ∼ a
multIdentLeft : {a : A} → (identity · a) ∼ a
invLeft : {a : A} → (inverse a) · a ∼ identity
invRight : {a : A} → a · (inverse a) ∼ identity
reflGroupWellDefined : {lvl : _} {A : Set lvl} {m n x y : A} {op : A → A → A} → m ≡ x → n ≡ y → (op m n) ≡ (op x y) reflGroupWellDefined : {lvl : _} {A : Set lvl} {m n x y : A} {op : A → A → A} → m ≡ x → n ≡ y → (op m n) ≡ (op x y)
reflGroupWellDefined {lvl} {A} {m} {n} {.m} {.n} {op} refl refl = refl reflGroupWellDefined {lvl} {A} {m} {n} {.m} {.n} {op} refl refl = refl
@@ -185,8 +175,8 @@ module Groups.Groups where
open Transitive transitiveEq open Transitive transitiveEq
open Symmetric symmetricEq open Symmetric symmetricEq
invContravariant : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → (x y : A) → (Setoid._∼_ S (Group.inverse G (x · y)) ((Group.inverse G y) · (Group.inverse G x))) invContravariant : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → {x y : A} → (Setoid._∼_ S (Group.inverse G (x · y)) ((Group.inverse G y) · (Group.inverse G x)))
invContravariant {S = S} {_·_} G x y = ans invContravariant {S = S} {_·_} G {x} {y} = ans
where where
open Group G renaming (inverse to _^-1) renaming (identity to e) open Group G renaming (inverse to _^-1) renaming (identity to e)
open Setoid S open Setoid S
@@ -361,7 +351,7 @@ module Groups.Groups where
g : f (Group.inverse G (m ·A Group.inverse G n)) ∼ identity g : f (Group.inverse G (m ·A Group.inverse G n)) ∼ identity
g = transitive (homRespectsInverse fHom {m ·A Group.inverse G n}) (transitive (inverseWellDefined H pr) (invIdentity H)) g = transitive (homRespectsInverse fHom {m ·A Group.inverse G n}) (transitive (inverseWellDefined H pr) (invIdentity H))
h : f (Group.inverse G (Group.inverse G n) ·A Group.inverse G m) ∼ identity h : f (Group.inverse G (Group.inverse G n) ·A Group.inverse G m) ∼ identity
h = transitive (GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invContravariant G m (Group.inverse G n)))) g h = transitive (GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invContravariant G))) g
i : f (n ·A Group.inverse G m) ∼ identity i : f (n ·A Group.inverse G m) ∼ identity
i = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invTwice G n)) (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))))) h i = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (invTwice G n)) (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))))) h
Transitive.transitive (Equivalence.transitiveEq (Setoid.eq ansSetoid)) {m} {n} {o} prmn prno = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Group.multIdentLeft G)))) k Transitive.transitive (Equivalence.transitiveEq (Setoid.eq ansSetoid)) {m} {n} {o} prmn prno = transitive (GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Group.multIdentLeft G)))) k
@@ -392,7 +382,7 @@ module Groups.Groups where
p6 : (f x) ·B (Group.identity H ·B f (Group.inverse G m)) ∼ (f x) ·B f (Group.inverse G m) p6 : (f x) ·B (Group.identity H ·B f (Group.inverse G m)) ∼ (f x) ·B f (Group.inverse G m)
p7 : (f x) ·B f (Group.inverse G m) ∼ f (x ·A (Group.inverse G m)) p7 : (f x) ·B f (Group.inverse G m) ∼ f (x ·A (Group.inverse G m))
p8 : f (x ·A (Group.inverse G m)) ∼ Group.identity H p8 : f (x ·A (Group.inverse G m)) ∼ Group.identity H
p1 = GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (invContravariant G m n)) p1 = GroupHom.wellDefined fHom (Group.wellDefined G (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (invContravariant G))
p2 = GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (fourWayAssoc G)) p2 = GroupHom.wellDefined fHom (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (fourWayAssoc G))
p3 = GroupHom.groupHom fHom p3 = GroupHom.groupHom fHom
p4 = Group.wellDefined H (Reflexive.reflexive reflexiveEq) (GroupHom.groupHom fHom) p4 = Group.wellDefined H (Reflexive.reflexive reflexiveEq) (GroupHom.groupHom fHom)

1
Groups/GroupsLemmas.agda
View File

@@ -6,6 +6,7 @@ open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals open import Numbers.Naturals
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
module Groups.GroupsLemmas where module Groups.GroupsLemmas where
invInv : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S (Group.inverse G (Group.inverse G x)) x invInv : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S (Group.inverse G (Group.inverse G x)) x

1
Rings/IntegralDomains.agda
View File

@@ -2,6 +2,7 @@
open import LogicalFormulae open import LogicalFormulae
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
open import Numbers.Naturals open import Numbers.Naturals
open import Orders open import Orders
open import Setoids.Setoids open import Setoids.Setoids

1
Rings/RingDefinition.agda
View File

@@ -2,6 +2,7 @@
open import LogicalFormulae open import LogicalFormulae
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
open import Numbers.Naturals open import Numbers.Naturals
open import Setoids.Orders open import Setoids.Orders
open import Setoids.Setoids open import Setoids.Setoids

124
Rings/RingLemmas.agda
View File

@@ -3,6 +3,7 @@
open import LogicalFormulae open import LogicalFormulae
open import Functions open import Functions
open import Groups.Groups open import Groups.Groups
open import Groups.GroupDefinition
open import Groups.GroupsLemmas open import Groups.GroupsLemmas
open import Rings.RingDefinition open import Rings.RingDefinition
open import Setoids.Setoids open import Setoids.Setoids
@@ -86,3 +87,126 @@ module Rings.RingLemmas where
open Transitive (Equivalence.transitiveEq (Setoid.eq S)) open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S)) open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S)) open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
ringCanMultiplyByPositive : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
ringCanMultiplyByPositive {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} 0<c x<y = SetoidPartialOrder.wellDefined pOrder reflexive (Group.multIdentRight additiveGroup) q'
where
open Ring R
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
have : 0R < (y + Group.inverse additiveGroup x)
have = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition oRing x<y (Group.inverse additiveGroup x))
p : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p = SetoidPartialOrder.wellDefined pOrder reflexive (transitive multCommutative (transitive multDistributes ((Group.wellDefined additiveGroup) multCommutative multCommutative))) (OrderedRing.orderRespectsMultiplication oRing have 0<c)
p' : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
p' = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (transitive (transitive multCommutative (ringMinusExtracts R)) (inverseWellDefined additiveGroup multCommutative))) p
q : (0R + (x * c)) < (((y * c) + (Group.inverse additiveGroup (x * c))) + (x * c))
q = OrderedRing.orderRespectsAddition oRing p' (x * c)
q' : (x * c) < ((y * c) + 0R)
q' = SetoidPartialOrder.wellDefined pOrder (Group.multIdentLeft additiveGroup) (transitive (symmetric (Group.multAssoc additiveGroup)) (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
ringCanCancelPositive : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
ringCanCancelPositive {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.wellDefined pOrder (Group.multIdentLeft additiveGroup) (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.multIdentRight additiveGroup))) q''
where
open Ring R
open Setoid S
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
have : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
have = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition oRing xc<yc (Group.inverse additiveGroup _))
p : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (symmetric (transitive (multCommutative) (transitive (ringMinusExtracts R) (inverseWellDefined additiveGroup multCommutative))))) have
q : 0R < ((y + Group.inverse additiveGroup x) * c)
q = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (transitive (Group.wellDefined additiveGroup multCommutative multCommutative) (symmetric multDistributes)) multCommutative) p
q' : 0R < (y + Group.inverse additiveGroup x)
q' with SetoidTotalOrder.totality tOrder 0R (y + Group.inverse additiveGroup x)
q' | inl (inl pr) = pr
q' | inl (inr y-x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder reflexive (transitive multCommutative (ringTimesZero R)) k))
where
open Group additiveGroup
f : ((y + inverse x) + (inverse (y + inverse x))) < (identity + inverse (y + inverse x))
f = OrderedRing.orderRespectsAddition oRing y-x<0 _
g : identity < inverse (y + inverse x)
g = SetoidPartialOrder.wellDefined pOrder invRight multIdentLeft f
h : (identity * c) < ((inverse (y + inverse x)) * c)
h = ringCanMultiplyByPositive oRing 0<c g
i : (0R + (identity * c)) < (((y + inverse x) * c) + ((inverse (y + inverse x)) * c))
i = ringAddInequalities oRing q h
j : 0R < (((y + inverse x) + (inverse (y + inverse x))) * c)
j = SetoidPartialOrder.wellDefined pOrder (transitive multIdentLeft (transitive multCommutative (ringTimesZero R))) (symmetric (transitive multCommutative (transitive multDistributes (Group.wellDefined additiveGroup multCommutative multCommutative)))) i
k : 0R < (0R * c)
k = SetoidPartialOrder.wellDefined pOrder reflexive (multWellDefined invRight reflexive) j
q' | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (multWellDefined x=y reflexive) reflexive xc<yc))
where
open Group additiveGroup
f : inverse identity ∼ inverse (y + inverse x)
f = inverseWellDefined additiveGroup 0=y-x
g : identity ∼ (inverse y) + x
g = transitive (symmetric (invIdentity additiveGroup)) (transitive f (transitive (transitive (invContravariant additiveGroup) groupIsAbelian) (wellDefined reflexive (invInv additiveGroup))))
x=y : x ∼ y
x=y = transferToRight additiveGroup (symmetric (transitive g groupIsAbelian))
q'' : (0R + x) < ((y + Group.inverse additiveGroup x) + x)
q'' = OrderedRing.orderRespectsAddition oRing q' x
ringSwapNegatives : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
ringSwapNegatives {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} oRing {x} {y} -x<-y = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.multIdentRight additiveGroup))) (Group.multIdentLeft additiveGroup) v
where
open Ring R
open Setoid S
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
t : ((Group.inverse additiveGroup x) + y) < ((Group.inverse additiveGroup y) + y)
t = OrderedRing.orderRespectsAddition oRing -x<-y y
u : (y + (Group.inverse additiveGroup x)) < 0R
u = SetoidPartialOrder.wellDefined pOrder (groupIsAbelian) (Group.invLeft additiveGroup) t
v : ((y + (Group.inverse additiveGroup x)) + x) < (0R + x)
v = OrderedRing.orderRespectsAddition oRing u x
ringCanMultiplyByNegative : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → c < (Ring.0R R) → x < y → (y * c) < (x * c)
ringCanMultiplyByNegative {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} c<0 x<y = ringSwapNegatives oRing u
where
open Ring R
open Setoid S
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
p : (c + Group.inverse additiveGroup c) < (0R + Group.inverse additiveGroup c)
p = OrderedRing.orderRespectsAddition oRing c<0 _
0<-c : 0R < (Group.inverse additiveGroup c)
0<-c = SetoidPartialOrder.wellDefined pOrder (Group.invRight additiveGroup) (Group.multIdentLeft additiveGroup) p
t : (x * Group.inverse additiveGroup c) < (y * Group.inverse additiveGroup c)
t = ringCanMultiplyByPositive oRing 0<-c x<y
u : (Group.inverse additiveGroup (x * c)) < Group.inverse additiveGroup (y * c)
u = SetoidPartialOrder.wellDefined pOrder (ringMinusExtracts R) (ringMinusExtracts R) t
ringCanCancelNegative : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (oRing : OrderedRing R tOrder) → {x y c : A} → c < (Ring.0R R) → (x * c) < (y * c) → y < x
ringCanCancelNegative {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {_<_ = _<_} {pOrder = pOrder} {tOrder = tOrder} oRing {x} {y} {c} c<0 xc<yc = r
where
open Ring R
open Setoid S
open Group additiveGroup
open Transitive (Equivalence.transitiveEq (Setoid.eq S))
open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
p : 0R < ((y * c) + inverse (x * c))
p = SetoidPartialOrder.wellDefined pOrder invRight reflexive (OrderedRing.orderRespectsAddition oRing xc<yc (inverse (x * c)))
p1 : 0R < ((y * c) + ((inverse x) * c))
p1 = SetoidPartialOrder.wellDefined pOrder reflexive (Group.wellDefined additiveGroup reflexive (transitive (inverseWellDefined additiveGroup multCommutative) (transitive (symmetric (ringMinusExtracts R)) multCommutative))) p
p2 : 0R < ((y + inverse x) * c)
p2 = SetoidPartialOrder.wellDefined pOrder reflexive (transitive (Group.wellDefined additiveGroup multCommutative multCommutative) (transitive (symmetric multDistributes) multCommutative)) p1
q : (y + inverse x) < 0R
q with SetoidTotalOrder.totality tOrder 0R (y + inverse x)
q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bad c<0))
where
bad : 0R < c
bad = ringCanCancelPositive oRing pr (SetoidPartialOrder.wellDefined pOrder (symmetric (transitive multCommutative (ringTimesZero R))) multCommutative p2)
q | inl (inr pr) = pr
q | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.wellDefined pOrder (multWellDefined x=y reflexive) reflexive xc<yc))
where
x=y : x ∼ y
x=y = transitive (symmetric multIdentLeft) (transitive (Group.wellDefined additiveGroup 0=y-x reflexive) (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive invLeft) multIdentRight)))
r : y < x
r = SetoidPartialOrder.wellDefined pOrder (transitive (symmetric (Group.multAssoc additiveGroup)) (transitive (Group.wellDefined additiveGroup reflexive (invLeft)) multIdentRight)) (Group.multIdentLeft additiveGroup) (OrderedRing.orderRespectsAddition oRing q x)