mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-12 23:28:39 +00:00
Split out parts of Field of Fractions (#63)
This commit is contained in:
Patrick Stevens
GitHub
@@ -1,194 +0,0 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions where
|
||||
|
||||
fieldOfFractionsSet : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} → {R : Ring S _+_ _*_} → IntegralDomain R → Set (a ⊔ b)
|
||||
fieldOfFractionsSet {A = A} {S = S} {R = R} I = (A && (Sg A (λ a → (Setoid._∼_ S a (Ring.0R R) → False))))
|
||||
|
||||
fieldOfFractionsSetoid : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} → {R : Ring S _+_ _*_} → (I : IntegralDomain R) → Setoid (fieldOfFractionsSet I)
|
||||
Setoid._∼_ (fieldOfFractionsSetoid {S = S} {_*_ = _*_} I) (a ,, (b , b!=0)) (c ,, (d , d!=0)) = Setoid._∼_ S (a * d) (b * c)
|
||||
Equivalence.reflexive (Setoid.eq (fieldOfFractionsSetoid {R = R} I)) {a ,, (b , b!=0)} = Ring.*Commutative R
|
||||
Equivalence.symmetric (Setoid.eq (fieldOfFractionsSetoid {S = S} {R = R} I)) {a ,, (b , b!=0)} {c ,, (d , d!=0)} ad=bc = transitive (Ring.*Commutative R) (transitive (symmetric ad=bc) (Ring.*Commutative R))
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
Equivalence.transitive (Setoid.eq (fieldOfFractionsSetoid {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} ad=bc cf=de = p5
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
p : (a * d) * f ∼ (b * c) * f
|
||||
p = Ring.*WellDefined R ad=bc reflexive
|
||||
p2 : (a * f) * d ∼ b * (d * e)
|
||||
p2 = transitive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive p (transitive (symmetric *Associative) (*WellDefined reflexive cf=de)))
|
||||
p3 : (a * f) * d ∼ (b * e) * d
|
||||
p3 = transitive p2 (transitive (*WellDefined reflexive *Commutative) *Associative)
|
||||
p4 : (d ∼ 0R) || ((a * f) ∼ (b * e))
|
||||
p4 = cancelIntDom I (transitive *Commutative (transitive p3 *Commutative))
|
||||
p5 : (a * f) ∼ (b * e)
|
||||
p5 with p4
|
||||
p5 | inl d=0 = exFalso (d!=0 d=0)
|
||||
p5 | inr x = x
|
||||
|
||||
fieldOfFractionsPlus : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} → (I : IntegralDomain R) → fieldOfFractionsSet I → fieldOfFractionsSet I → fieldOfFractionsSet I
|
||||
fieldOfFractionsPlus {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (((a * d) + (b * c)) ,, ((b * d) , ans))
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
ans : ((b * d) ∼ Ring.0R R) → False
|
||||
ans pr with IntegralDomain.intDom I pr
|
||||
ans pr | inl x = b!=0 x
|
||||
ans pr | inr x = d!=0 x
|
||||
|
||||
fieldOfFractionsTimes : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} → (I : IntegralDomain R) → fieldOfFractionsSet I → fieldOfFractionsSet I → fieldOfFractionsSet I
|
||||
fieldOfFractionsTimes {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (a * c) ,, ((b * d) , ans)
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
ans : ((b * d) ∼ Ring.0R R) → False
|
||||
ans pr with IntegralDomain.intDom I pr
|
||||
ans pr | inl x = b!=0 x
|
||||
ans pr | inr x = d!=0 x
|
||||
|
||||
fieldOfFractionsRing : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} → (I : IntegralDomain R) → Ring (fieldOfFractionsSetoid I) (fieldOfFractionsPlus I) (fieldOfFractionsTimes I)
|
||||
Group.+WellDefined (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} {g ,, (h , h!=0)} af=be ch=dg = need
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
have1 : (c * h) ∼ (d * g)
|
||||
have1 = ch=dg
|
||||
have2 : (a * f) ∼ (b * e)
|
||||
have2 = af=be
|
||||
need : (((a * d) + (b * c)) * (f * h)) ∼ ((b * d) * (((e * h) + (f * g))))
|
||||
need = transitive (transitive (Ring.*Commutative R) (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) (transitive *Associative (transitive (*WellDefined (*Commutative) reflexive) (transitive (*WellDefined *Associative reflexive) (transitive (*WellDefined (*WellDefined have2 reflexive) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) reflexive) (symmetric *Associative))))))))) (transitive *Commutative (transitive (transitive (symmetric *Associative) (*WellDefined reflexive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined have1 reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))))) *Associative))))) (symmetric (Ring.*DistributesOver+ R))
|
||||
Group.0G (Ring.additiveGroup (fieldOfFractionsRing {R = R} I)) = Ring.0R R ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
Group.inverse (Ring.additiveGroup (fieldOfFractionsRing {R = R} I)) (a ,, b) = Group.inverse (Ring.additiveGroup R) a ,, b
|
||||
Group.+Associative (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * (d * f)) + (b * ((c * f) + (d * e)))) * ((b * d) * f)) ∼ ((b * (d * f)) * ((((a * d) + (b * c)) * f) + ((b * d) * e)))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.*Associative R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.*DistributesOver+ R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Associative R) (Ring.*Associative R))) (transitive (Group.+Associative (Ring.additiveGroup R)) (Group.+WellDefined (Ring.additiveGroup R) (transitive (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Associative R) (Ring.*Commutative R)) (Ring.*Commutative R)) (symmetric (Ring.*DistributesOver+ R))) (Ring.*Commutative R)) reflexive)))))
|
||||
Group.identRight (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , b!=0)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * Ring.1R R) + (b * Group.0G (Ring.additiveGroup R))) * b) ∼ ((b * Ring.1R R) * a)
|
||||
need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.timesZero R)) (Group.identRight (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (symmetric (Ring.*WellDefined R (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive))
|
||||
Group.identLeft (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Group.0G (Ring.additiveGroup R) * b) + (Ring.1R R * a)) * b) ∼ ((Ring.1R R * b) * a)
|
||||
need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.timesZero R)) reflexive) (Group.identLeft (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive)
|
||||
Group.invLeft (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Group.inverse (Ring.additiveGroup R) a * b) + (b * a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
|
||||
need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invLeft (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))
|
||||
Group.invRight (Ring.additiveGroup (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * b) + (b * Group.inverse (Ring.additiveGroup R) a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
|
||||
need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invRight (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))
|
||||
Ring.*WellDefined (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} {g ,, (h , _)} af=be ch=dg = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * c) * (f * h)) ∼ ((b * d) * (e * g))
|
||||
need = transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) (transitive (Ring.*WellDefined R (Ring.*WellDefined R reflexive ch=dg) reflexive) (transitive (Ring.*Commutative R) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (Ring.*Commutative R) reflexive) (transitive (Ring.*WellDefined R af=be reflexive) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (transitive (symmetric (Ring.*Associative R)) (transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (Ring.*Associative R))) reflexive) (symmetric (Ring.*Associative R)))))))))))
|
||||
Ring.1R (fieldOfFractionsRing {R = R} I) = Ring.1R R ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
Ring.groupIsAbelian (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} {c ,, (d , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * d) + (b * c)) * (d * b)) ∼ ((b * d) * ((c * b) + (d * a)))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) (Ring.*Commutative R)) (Ring.groupIsAbelian R)))
|
||||
Ring.*Associative (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * (c * e)) * ((b * d) * f)) ∼ ((b * (d * f)) * ((a * c) * e))
|
||||
need = transitive (Ring.*WellDefined R (Ring.*Associative R) (symmetric (Ring.*Associative R))) (Ring.*Commutative R)
|
||||
Ring.*Commutative (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} {c ,, (d , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * c) * (d * b)) ∼ ((b * d) * (c * a))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (Ring.*Commutative R))
|
||||
Ring.*DistributesOver+ (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
inter : b * (a * ((c * f) + (d * e))) ∼ (((a * c) * (b * f)) + ((b * d) * (a * e)))
|
||||
inter = transitive *Associative (transitive *DistributesOver+ (Group.+WellDefined additiveGroup (transitive *Associative (transitive (*WellDefined (transitive (*WellDefined (*Commutative) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative))) reflexive) (symmetric *Associative))) (transitive *Associative (transitive (*WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive) (symmetric *Associative)))))
|
||||
need : ((a * ((c * f) + (d * e))) * ((b * d) * (b * f))) ∼ ((b * (d * f)) * (((a * c) * (b * f)) + ((b * d) * (a * e))))
|
||||
need = transitive (Ring.*WellDefined R reflexive (Ring.*WellDefined R reflexive (Ring.*Commutative R))) (transitive (Ring.*WellDefined R reflexive (Ring.*Associative R)) (transitive (Ring.*Commutative R) (transitive (Ring.*WellDefined R (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) reflexive) (transitive (symmetric (Ring.*Associative R)) (Ring.*WellDefined R reflexive inter)))))
|
||||
Ring.identIsIdent (fieldOfFractionsRing {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Ring.1R R) * a) * b) ∼ (((Ring.1R R * b)) * a)
|
||||
need = transitive (Ring.*WellDefined R (Ring.identIsIdent R) reflexive) (transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive))
|
||||
|
||||
fieldOfFractions : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} → (I : IntegralDomain R) → Field (fieldOfFractionsRing I)
|
||||
Field.allInvertible (fieldOfFractions {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) (fst ,, (b , _)) prA = (b ,, (fst , ans)) , need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((b * fst) * Ring.1R R) ∼ ((fst * b) * Ring.1R R)
|
||||
need = Ring.*WellDefined R (Ring.*Commutative R) reflexive
|
||||
ans : fst ∼ Ring.0R R → False
|
||||
ans pr = prA need'
|
||||
where
|
||||
need' : (fst * Ring.1R R) ∼ (b * Ring.0R R)
|
||||
need' = transitive (Ring.*WellDefined R pr reflexive) (transitive (transitive (Ring.*Commutative R) (Ring.timesZero R)) (symmetric (Ring.timesZero R)))
|
||||
Field.nontrivial (fieldOfFractions {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I) pr = IntegralDomain.nontrivial I (symmetric (transitive (symmetric (Ring.timesZero R)) (transitive (Ring.*Commutative R) (transitive pr (Ring.identIsIdent R)))))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
pr' : (Ring.0R R) * (Ring.1R R) ∼ (Ring.1R R) * (Ring.1R R)
|
||||
pr' = pr
|
||||
|
||||
embedIntoFieldOfFractions : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) → A → fieldOfFractionsSet I
|
||||
embedIntoFieldOfFractions {R = R} I a = a ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
|
||||
homIntoFieldOfFractions : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) → RingHom R (fieldOfFractionsRing I) (embedIntoFieldOfFractions I)
|
||||
RingHom.preserves1 (homIntoFieldOfFractions {S = S} I) = Equivalence.reflexive (Setoid.eq S)
|
||||
RingHom.ringHom (homIntoFieldOfFractions {S = S} {R = R} I) {a} {b} = Equivalence.transitive (Setoid.eq S) (Ring.*WellDefined R (Equivalence.reflexive (Setoid.eq S)) (Ring.identIsIdent R)) (Ring.*Commutative R)
|
||||
GroupHom.groupHom (RingHom.groupHom (homIntoFieldOfFractions {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} I)) {x} {y} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((x + y) * (Ring.1R R * Ring.1R R)) ∼ (Ring.1R R * ((x * Ring.1R R) + (Ring.1R R * y)))
|
||||
need = transitive (transitive (Ring.*WellDefined R reflexive (Ring.identIsIdent R)) (transitive (Ring.*Commutative R) (transitive (Ring.identIsIdent R) (Group.+WellDefined (Ring.additiveGroup R) (symmetric (transitive (Ring.*Commutative R) (Ring.identIsIdent R))) (symmetric (Ring.identIsIdent R)))))) (symmetric (Ring.identIsIdent R))
|
||||
GroupHom.wellDefined (RingHom.groupHom (homIntoFieldOfFractions {S = S} {R = R} I)) x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
homIntoFieldOfFractionsIsInj : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) → SetoidInjection S (fieldOfFractionsSetoid I) (embedIntoFieldOfFractions I)
|
||||
SetoidInjection.wellDefined (homIntoFieldOfFractionsIsInj {S = S} {R = R} I) x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
SetoidInjection.injective (homIntoFieldOfFractionsIsInj {S = S} {R = R} I) x~y = transitive (symmetric identIsIdent) (transitive *Commutative (transitive x~y identIsIdent))
|
||||
where
|
||||
open Ring R
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
42
Fields/FieldOfFractions/Addition.agda
Normal file
42
Fields/FieldOfFractions/Addition.agda
Normal file
@@ -0,0 +1,42 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Addition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
|
||||
fieldOfFractionsPlus : fieldOfFractionsSet → fieldOfFractionsSet → fieldOfFractionsSet
|
||||
fieldOfFractionsPlus (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (((a * d) + (b * c)) ,, ((b * d) , ans))
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
ans : ((b * d) ∼ Ring.0R R) → False
|
||||
ans pr with IntegralDomain.intDom I pr
|
||||
ans pr | inl x = b!=0 x
|
||||
ans pr | inr x = d!=0 x
|
||||
|
||||
plusWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsPlus a b) (fieldOfFractionsPlus c d)
|
||||
plusWellDefined {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} {g ,, (h , h!=0)} af=be ch=dg = need
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
have1 : (c * h) ∼ (d * g)
|
||||
have1 = ch=dg
|
||||
have2 : (a * f) ∼ (b * e)
|
||||
have2 = af=be
|
||||
need : (((a * d) + (b * c)) * (f * h)) ∼ ((b * d) * (((e * h) + (f * g))))
|
||||
need = transitive (transitive (Ring.*Commutative R) (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) (transitive *Associative (transitive (*WellDefined (*Commutative) reflexive) (transitive (*WellDefined *Associative reflexive) (transitive (*WellDefined (*WellDefined have2 reflexive) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) reflexive) (symmetric *Associative))))))))) (transitive *Commutative (transitive (transitive (symmetric *Associative) (*WellDefined reflexive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined have1 reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))))) *Associative))))) (symmetric (Ring.*DistributesOver+ R))
|
||||
41
Fields/FieldOfFractions/Field.agda
Normal file
41
Fields/FieldOfFractions/Field.agda
Normal file
@@ -0,0 +1,41 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Field {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
open import Fields.FieldOfFractions.Addition I
|
||||
open import Fields.FieldOfFractions.Multiplication I
|
||||
open import Fields.FieldOfFractions.Ring I
|
||||
|
||||
fieldOfFractions : Field fieldOfFractionsRing
|
||||
Field.allInvertible fieldOfFractions (fst ,, (b , _)) prA = (b ,, (fst , ans)) , need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((b * fst) * Ring.1R R) ∼ ((fst * b) * Ring.1R R)
|
||||
need = Ring.*WellDefined R (Ring.*Commutative R) reflexive
|
||||
ans : fst ∼ Ring.0R R → False
|
||||
ans pr = prA need'
|
||||
where
|
||||
need' : (fst * Ring.1R R) ∼ (b * Ring.0R R)
|
||||
need' = transitive (Ring.*WellDefined R pr reflexive) (transitive (transitive (Ring.*Commutative R) (Ring.timesZero R)) (symmetric (Ring.timesZero R)))
|
||||
Field.nontrivial fieldOfFractions pr = IntegralDomain.nontrivial I (symmetric (transitive (symmetric (Ring.timesZero R)) (transitive (Ring.*Commutative R) (transitive pr (Ring.identIsIdent R)))))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
pr' : (Ring.0R R) * (Ring.1R R) ∼ (Ring.1R R) * (Ring.1R R)
|
||||
pr' = pr
|
||||
65
Fields/FieldOfFractions/Group.agda
Normal file
65
Fields/FieldOfFractions/Group.agda
Normal file
@@ -0,0 +1,65 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Group {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
open import Fields.FieldOfFractions.Addition I
|
||||
|
||||
fieldOfFractionsGroup : Group fieldOfFractionsSetoid fieldOfFractionsPlus
|
||||
Group.+WellDefined fieldOfFractionsGroup {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} {g ,, (h , h!=0)} af=be ch=dg = need
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
have1 : (c * h) ∼ (d * g)
|
||||
have1 = ch=dg
|
||||
have2 : (a * f) ∼ (b * e)
|
||||
have2 = af=be
|
||||
need : (((a * d) + (b * c)) * (f * h)) ∼ ((b * d) * (((e * h) + (f * g))))
|
||||
need = transitive (transitive (Ring.*Commutative R) (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) (transitive *Associative (transitive (*WellDefined (*Commutative) reflexive) (transitive (*WellDefined *Associative reflexive) (transitive (*WellDefined (*WellDefined have2 reflexive) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) reflexive) (symmetric *Associative))))))))) (transitive *Commutative (transitive (transitive (symmetric *Associative) (*WellDefined reflexive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined have1 reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))))) *Associative))))) (symmetric (Ring.*DistributesOver+ R))
|
||||
Group.0G fieldOfFractionsGroup = Ring.0R R ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
Group.inverse fieldOfFractionsGroup (a ,, b) = Group.inverse (Ring.additiveGroup R) a ,, b
|
||||
Group.+Associative fieldOfFractionsGroup {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * (d * f)) + (b * ((c * f) + (d * e)))) * ((b * d) * f)) ∼ ((b * (d * f)) * ((((a * d) + (b * c)) * f) + ((b * d) * e)))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.*Associative R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.*DistributesOver+ R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Associative R) (Ring.*Associative R))) (transitive (Group.+Associative (Ring.additiveGroup R)) (Group.+WellDefined (Ring.additiveGroup R) (transitive (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Associative R) (Ring.*Commutative R)) (Ring.*Commutative R)) (symmetric (Ring.*DistributesOver+ R))) (Ring.*Commutative R)) reflexive)))))
|
||||
Group.identRight fieldOfFractionsGroup {a ,, (b , b!=0)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * Ring.1R R) + (b * Group.0G (Ring.additiveGroup R))) * b) ∼ ((b * Ring.1R R) * a)
|
||||
need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive) (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.timesZero R)) (Group.identRight (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (symmetric (Ring.*WellDefined R (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) reflexive))
|
||||
Group.identLeft fieldOfFractionsGroup {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Group.0G (Ring.additiveGroup R) * b) + (Ring.1R R * a)) * b) ∼ ((Ring.1R R * b) * a)
|
||||
need = transitive (transitive (Ring.*WellDefined R (transitive (Group.+WellDefined (Ring.additiveGroup R) reflexive (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (transitive (Ring.*Commutative R) (Ring.timesZero R)) reflexive) (Group.identLeft (Ring.additiveGroup R)))) reflexive) (Ring.*Commutative R)) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive)
|
||||
Group.invLeft fieldOfFractionsGroup {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Group.inverse (Ring.additiveGroup R) a * b) + (b * a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
|
||||
need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invLeft (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))
|
||||
Group.invRight fieldOfFractionsGroup {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * b) + (b * Group.inverse (Ring.additiveGroup R) a)) * Ring.1R R) ∼ ((b * b) * Group.0G (Ring.additiveGroup R))
|
||||
need = transitive (transitive (transitive (Ring.*Commutative R) (Ring.identIsIdent R)) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) reflexive) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invRight (Ring.additiveGroup R))) (Ring.timesZero R))))) (symmetric (Ring.timesZero R))
|
||||
49
Fields/FieldOfFractions/Lemmas.agda
Normal file
49
Fields/FieldOfFractions/Lemmas.agda
Normal file
@@ -0,0 +1,49 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
open import Fields.FieldOfFractions.Addition I
|
||||
open import Fields.FieldOfFractions.Multiplication I
|
||||
open import Fields.FieldOfFractions.Ring I
|
||||
open import Fields.FieldOfFractions.Field I
|
||||
|
||||
embedIntoFieldOfFractions : A → fieldOfFractionsSet
|
||||
embedIntoFieldOfFractions a = a ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
|
||||
homIntoFieldOfFractions : RingHom R fieldOfFractionsRing embedIntoFieldOfFractions
|
||||
RingHom.preserves1 homIntoFieldOfFractions = Equivalence.reflexive (Setoid.eq S)
|
||||
RingHom.ringHom homIntoFieldOfFractions {a} {b} = Equivalence.transitive (Setoid.eq S) (Ring.*WellDefined R (Equivalence.reflexive (Setoid.eq S)) (Ring.identIsIdent R)) (Ring.*Commutative R)
|
||||
GroupHom.groupHom (RingHom.groupHom homIntoFieldOfFractions) {x} {y} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((x + y) * (Ring.1R R * Ring.1R R)) ∼ (Ring.1R R * ((x * Ring.1R R) + (Ring.1R R * y)))
|
||||
need = transitive (transitive (Ring.*WellDefined R reflexive (Ring.identIsIdent R)) (transitive (Ring.*Commutative R) (transitive (Ring.identIsIdent R) (Group.+WellDefined (Ring.additiveGroup R) (symmetric (transitive (Ring.*Commutative R) (Ring.identIsIdent R))) (symmetric (Ring.identIsIdent R)))))) (symmetric (Ring.identIsIdent R))
|
||||
GroupHom.wellDefined (RingHom.groupHom homIntoFieldOfFractions) x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
homIntoFieldOfFractionsIsInj : SetoidInjection S fieldOfFractionsSetoid embedIntoFieldOfFractions
|
||||
SetoidInjection.wellDefined homIntoFieldOfFractionsIsInj x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
SetoidInjection.injective homIntoFieldOfFractionsIsInj x~y = transitive (symmetric identIsIdent) (transitive *Commutative (transitive x~y identIsIdent))
|
||||
where
|
||||
open Ring R
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
37
Fields/FieldOfFractions/Multiplication.agda
Normal file
37
Fields/FieldOfFractions/Multiplication.agda
Normal file
@@ -0,0 +1,37 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Multiplication {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
|
||||
fieldOfFractionsTimes : fieldOfFractionsSet → fieldOfFractionsSet → fieldOfFractionsSet
|
||||
fieldOfFractionsTimes (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (a * c) ,, ((b * d) , ans)
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
ans : ((b * d) ∼ Ring.0R R) → False
|
||||
ans pr with IntegralDomain.intDom I pr
|
||||
ans pr | inl x = b!=0 x
|
||||
ans pr | inr x = d!=0 x
|
||||
|
||||
fieldOfFractionsTimesWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → (Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsTimes a b) (fieldOfFractionsTimes c d))
|
||||
fieldOfFractionsTimesWellDefined {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} {g ,, (h , _)} af=be ch=dg = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * c) * (f * h)) ∼ ((b * d) * (e * g))
|
||||
need = transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) (transitive (Ring.*WellDefined R (Ring.*WellDefined R reflexive ch=dg) reflexive) (transitive (Ring.*Commutative R) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (Ring.*Commutative R) reflexive) (transitive (Ring.*WellDefined R af=be reflexive) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (transitive (symmetric (Ring.*Associative R)) (transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (Ring.*Associative R))) reflexive) (symmetric (Ring.*Associative R)))))))))))
|
||||
@@ -14,18 +14,20 @@ open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Orders
|
||||
open import Fields.FieldOfFractions
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.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 _<_} {pRing : PartiallyOrderedRing R pOrder} (I : IntegralDomain R) (order : TotallyOrderedRing pRing) where
|
||||
module Fields.FieldOfFractions.Order {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 _<_} {pRing : PartiallyOrderedRing R pOrder} (I : IntegralDomain R) (order : TotallyOrderedRing pRing) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
open import Fields.FieldOfFractions.Ring I
|
||||
|
||||
open SetoidTotalOrder (TotallyOrderedRing.total order)
|
||||
open import Rings.Orders.Partial.Lemmas
|
||||
open PartiallyOrderedRing pRing
|
||||
|
||||
fieldOfFractionsComparison : Rel (fieldOfFractionsSet I)
|
||||
fieldOfFractionsComparison : Rel fieldOfFractionsSet
|
||||
fieldOfFractionsComparison (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with totality (Ring.0R R) denomA
|
||||
fieldOfFractionsComparison (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) with totality (Ring.0R R) denomB
|
||||
fieldOfFractionsComparison (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0<denomA) | inl (inl 0<denomB) = (numA * denomB) < (numB * denomA)
|
||||
@@ -43,7 +45,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
fieldOfFractionsOrderWellDefinedLeft : {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison x y → Setoid._∼_ (fieldOfFractionsSetoid I) x z → fieldOfFractionsComparison z y
|
||||
fieldOfFractionsOrderWellDefinedLeft : {x y z : fieldOfFractionsSet} → fieldOfFractionsComparison x y → Setoid._∼_ fieldOfFractionsSetoid x z → fieldOfFractionsComparison z y
|
||||
fieldOfFractionsOrderWellDefinedLeft {(numX ,, (denomX , denomX!=0))} {(numY ,, (denomY , denomY!=0))} {(numZ ,, (denomZ , denomZ!=0))} x<y x=z with totality (Ring.0R R) denomZ
|
||||
fieldOfFractionsOrderWellDefinedLeft {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y x=z | inl (inl 0<denomZ) with totality (Ring.0R R) denomY
|
||||
fieldOfFractionsOrderWellDefinedLeft {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 totality (Ring.0R R) denomX
|
||||
@@ -153,7 +155,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
fieldOfFractionsOrderWellDefinedRight : {x y z : fieldOfFractionsSet I} → fieldOfFractionsComparison x y → Setoid._∼_ (fieldOfFractionsSetoid I) y z → fieldOfFractionsComparison x z
|
||||
fieldOfFractionsOrderWellDefinedRight : {x y z : fieldOfFractionsSet} → fieldOfFractionsComparison x y → Setoid._∼_ (fieldOfFractionsSetoid) y z → fieldOfFractionsComparison x z
|
||||
fieldOfFractionsOrderWellDefinedRight {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z with totality (Ring.0R R) denomX
|
||||
fieldOfFractionsOrderWellDefinedRight {numX ,, (denomX , denomX!=0)} {numY ,, (denomY , denomY!=0)} {numZ ,, (denomZ , denomZ!=0)} x<y y=z | inl (inl 0<denomX) with totality (Ring.0R R) denomZ
|
||||
fieldOfFractionsOrderWellDefinedRight {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 totality (Ring.0R R) denomY
|
||||
@@ -208,7 +210,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
|
||||
open Ring R
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
fieldOfFractionsOrder : SetoidPartialOrder (fieldOfFractionsSetoid I) fieldOfFractionsComparison
|
||||
fieldOfFractionsOrder : SetoidPartialOrder fieldOfFractionsSetoid fieldOfFractionsComparison
|
||||
SetoidPartialOrder.<WellDefined (fieldOfFractionsOrder) {a} {b} {c} {d} a=b c=d a<c = fieldOfFractionsOrderWellDefinedRight {b} {c} {d} (fieldOfFractionsOrderWellDefinedLeft {a} {c} {b} a<c a=b) c=d
|
||||
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr with totality (Ring.0R R) aDenom
|
||||
SetoidPartialOrder.irreflexive (fieldOfFractionsOrder) {aNum ,, (aDenom , aDenom!=0)} pr | inl (inl 0<aDenom) with totality (Ring.0R R) aDenom
|
||||
@@ -407,7 +409,7 @@ module Fields.FieldOfFractionsOrder {a b c : _} {A : Set a} {S : Setoid {a} {b}
|
||||
open Ring R
|
||||
open Equivalence (Setoid.eq S)
|
||||
|
||||
fieldOfFractionsPOrderedRing : PartiallyOrderedRing (fieldOfFractionsRing I) (SetoidTotalOrder.partial fieldOfFractionsTotalOrder)
|
||||
fieldOfFractionsPOrderedRing : PartiallyOrderedRing fieldOfFractionsRing (SetoidTotalOrder.partial fieldOfFractionsTotalOrder)
|
||||
PartiallyOrderedRing.orderRespectsAddition fieldOfFractionsPOrderedRing {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) with totality (Ring.0R R) (denomA * denomC)
|
||||
PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) with totality (Ring.0R R) (denomB * denomC)
|
||||
PartiallyOrderedRing.orderRespectsAddition (fieldOfFractionsPOrderedRing) {numA ,, (denomA , denomA!=0)} {numB ,, (denomB , denomB!=0)} a<b (numC ,, (denomC , denomC!=0)) | inl (inl 0<dAdC) | inl (inl 0<dBdC) with totality (Ring.0R R) denomA
|
||||
60
Fields/FieldOfFractions/Ring.agda
Normal file
60
Fields/FieldOfFractions/Ring.agda
Normal file
@@ -0,0 +1,60 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Ring {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid I
|
||||
open import Fields.FieldOfFractions.Addition I
|
||||
open import Fields.FieldOfFractions.Group I
|
||||
open import Fields.FieldOfFractions.Multiplication I
|
||||
|
||||
fieldOfFractionsRing : Ring fieldOfFractionsSetoid fieldOfFractionsPlus fieldOfFractionsTimes
|
||||
Ring.additiveGroup fieldOfFractionsRing = fieldOfFractionsGroup
|
||||
Ring.*WellDefined fieldOfFractionsRing {a} {b} {c} {d} = fieldOfFractionsTimesWellDefined {a} {b} {c} {d}
|
||||
Ring.1R fieldOfFractionsRing = Ring.1R R ,, (Ring.1R R , IntegralDomain.nontrivial I)
|
||||
Ring.groupIsAbelian fieldOfFractionsRing {a ,, (b , _)} {c ,, (d , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((a * d) + (b * c)) * (d * b)) ∼ ((b * d) * ((c * b) + (d * a)))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (transitive (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) (Ring.*Commutative R)) (Ring.groupIsAbelian R)))
|
||||
Ring.*Associative fieldOfFractionsRing {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * (c * e)) * ((b * d) * f)) ∼ ((b * (d * f)) * ((a * c) * e))
|
||||
need = transitive (Ring.*WellDefined R (Ring.*Associative R) (symmetric (Ring.*Associative R))) (Ring.*Commutative R)
|
||||
Ring.*Commutative fieldOfFractionsRing {a ,, (b , _)} {c ,, (d , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : ((a * c) * (d * b)) ∼ ((b * d) * (c * a))
|
||||
need = transitive (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (Ring.*Commutative R))
|
||||
Ring.*DistributesOver+ fieldOfFractionsRing {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
inter : b * (a * ((c * f) + (d * e))) ∼ (((a * c) * (b * f)) + ((b * d) * (a * e)))
|
||||
inter = transitive *Associative (transitive *DistributesOver+ (Group.+WellDefined additiveGroup (transitive *Associative (transitive (*WellDefined (transitive (*WellDefined (*Commutative) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative))) reflexive) (symmetric *Associative))) (transitive *Associative (transitive (*WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive) (symmetric *Associative)))))
|
||||
need : ((a * ((c * f) + (d * e))) * ((b * d) * (b * f))) ∼ ((b * (d * f)) * (((a * c) * (b * f)) + ((b * d) * (a * e))))
|
||||
need = transitive (Ring.*WellDefined R reflexive (Ring.*WellDefined R reflexive (Ring.*Commutative R))) (transitive (Ring.*WellDefined R reflexive (Ring.*Associative R)) (transitive (Ring.*Commutative R) (transitive (Ring.*WellDefined R (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) reflexive) (transitive (symmetric (Ring.*Associative R)) (Ring.*WellDefined R reflexive inter)))))
|
||||
Ring.identIsIdent fieldOfFractionsRing {a ,, (b , _)} = need
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
need : (((Ring.1R R) * a) * b) ∼ (((Ring.1R R * b)) * a)
|
||||
need = transitive (Ring.*WellDefined R (Ring.identIsIdent R) reflexive) (transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive))
|
||||
44
Fields/FieldOfFractions/Setoid.agda
Normal file
44
Fields/FieldOfFractions/Setoid.agda
Normal file
@@ -0,0 +1,44 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Lemmas
|
||||
open import Rings.IntegralDomains
|
||||
open import Fields.Fields
|
||||
open import Functions
|
||||
open import Setoids.Setoids
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Fields.FieldOfFractions.Setoid {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
fieldOfFractionsSet : Set (a ⊔ b)
|
||||
fieldOfFractionsSet = (A && (Sg A (λ a → (Setoid._∼_ S a (Ring.0R R) → False))))
|
||||
|
||||
fieldOfFractionsSetoid : Setoid fieldOfFractionsSet
|
||||
Setoid._∼_ fieldOfFractionsSetoid (a ,, (b , b!=0)) (c ,, (d , d!=0)) = Setoid._∼_ S (a * d) (b * c)
|
||||
Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {a ,, (b , b!=0)} = Ring.*Commutative R
|
||||
Equivalence.symmetric (Setoid.eq fieldOfFractionsSetoid) {a ,, (b , b!=0)} {c ,, (d , d!=0)} ad=bc = transitive (Ring.*Commutative R) (transitive (symmetric ad=bc) (Ring.*Commutative R))
|
||||
where
|
||||
open Equivalence (Setoid.eq S)
|
||||
Equivalence.transitive (Setoid.eq fieldOfFractionsSetoid) {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} ad=bc cf=de = p5
|
||||
where
|
||||
open Setoid S
|
||||
open Ring R
|
||||
open Equivalence eq
|
||||
p : (a * d) * f ∼ (b * c) * f
|
||||
p = Ring.*WellDefined R ad=bc reflexive
|
||||
p2 : (a * f) * d ∼ b * (d * e)
|
||||
p2 = transitive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) (transitive p (transitive (symmetric *Associative) (*WellDefined reflexive cf=de)))
|
||||
p3 : (a * f) * d ∼ (b * e) * d
|
||||
p3 = transitive p2 (transitive (*WellDefined reflexive *Commutative) *Associative)
|
||||
p4 : (d ∼ 0R) || ((a * f) ∼ (b * e))
|
||||
p4 = cancelIntDom I (transitive *Commutative (transitive p3 *Commutative))
|
||||
p5 : (a * f) ∼ (b * e)
|
||||
p5 with p4
|
||||
p5 | inl d=0 = exFalso (d!=0 d=0)
|
||||
p5 | inr x = x
|
||||
Reference in New Issue
Block a user