From 660d7aa27c6dd5c90118a2fea19525f9c5622879 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Fri, 22 Nov 2019 19:52:57 +0000 Subject: [PATCH] Lots of rings (#82) --- Everything/Safe.agda | 13 +- Fields/FieldOfFractions/Addition.agda | 5 +- Fields/FieldOfFractions/Field.agda | 2 +- Fields/FieldOfFractions/Group.agda | 2 +- Fields/FieldOfFractions/Lemmas.agda | 2 +- Fields/FieldOfFractions/Multiplication.agda | 5 +- Fields/FieldOfFractions/Order.agda | 1362 ++++++++--------- Fields/FieldOfFractions/Ring.agda | 2 +- Fields/FieldOfFractions/Setoid.agda | 11 +- Fields/Fields.agda | 4 +- Fields/Orders/Lemmas.agda | 66 +- Fields/Orders/Partial/Definition.agda | 1 - Fields/Orders/Total/Definition.agda | 1 - Groups/Cosets.agda | 5 + Groups/FirstIsomorphismTheorem.agda | 16 +- Groups/Groups.agda | 44 - Groups/QuotientGroup/Definition.agda | 54 +- Groups/QuotientGroup/Lemmas.agda | 17 +- Groups/Subgroups/Definition.agda | 18 +- Groups/SymmetricGroups/Lemmas.agda | 1 + Numbers/Integers/Multiplication.agda | 1 - .../RingStructure/IntegralDomain.agda | 12 +- Numbers/Integers/RingStructure/Ring.agda | 1 - Rings/Cosets.agda | 5 + Rings/EuclideanDomains/Definition.agda | 37 + Rings/EuclideanDomains/Examples.agda | 39 + Rings/Homomorphisms/Definition.agda | 1 - Rings/Homomorphisms/Image.agda | 29 + Rings/Homomorphisms/Kernel.agda | 21 + Rings/Ideals/Definition.agda | 31 - Rings/Ideals/FirstIsomorphismTheorem.agda | 34 + Rings/Ideals/Lemmas.agda | 58 + Rings/Ideals/Prime/Definition.agda | 22 + Rings/Ideals/Principal/Definition.agda | 24 + Rings/IntegralDomains.agda | 37 - Rings/IntegralDomains/Definition.agda | 41 + Rings/IntegralDomains/Examples.agda | 28 + Rings/Isomorphisms/Definition.agda | 7 +- Rings/PrincipalIdealDomain.agda | 24 + Rings/Subrings/Definition.agda | 44 + 40 files changed, 1246 insertions(+), 881 deletions(-) create mode 100644 Rings/EuclideanDomains/Definition.agda create mode 100644 Rings/EuclideanDomains/Examples.agda create mode 100644 Rings/Homomorphisms/Image.agda create mode 100644 Rings/Homomorphisms/Kernel.agda create mode 100644 Rings/Ideals/FirstIsomorphismTheorem.agda create mode 100644 Rings/Ideals/Lemmas.agda create mode 100644 Rings/Ideals/Prime/Definition.agda create mode 100644 Rings/Ideals/Principal/Definition.agda delete mode 100644 Rings/IntegralDomains.agda create mode 100644 Rings/IntegralDomains/Definition.agda create mode 100644 Rings/IntegralDomains/Examples.agda create mode 100644 Rings/PrincipalIdealDomain.agda create mode 100644 Rings/Subrings/Definition.agda diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 027c39d..44d80c4 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -47,7 +47,7 @@ open import Rings.Lemmas open import Rings.Orders.Partial.Definition open import Rings.Orders.Total.Lemmas open import Rings.Orders.Partial.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Rings.DirectSum open import Rings.Polynomial.Ring open import Rings.Polynomial.Evaluation @@ -55,6 +55,17 @@ open import Rings.Ideals.Definition open import Rings.Isomorphisms.Definition open import Rings.Quotients.Definition open import Rings.Cosets +open import Rings.EuclideanDomains.Definition +open import Rings.EuclideanDomains.Examples +open import Rings.Homomorphisms.Image +open import Rings.Homomorphisms.Kernel +open import Rings.Ideals.FirstIsomorphismTheorem +open import Rings.Ideals.Lemmas +open import Rings.Ideals.Prime.Definition +open import Rings.Ideals.Principal.Definition +open import Rings.IntegralDomains.Examples +open import Rings.PrincipalIdealDomain +open import Rings.Subrings.Definition open import Setoids.Setoids open import Setoids.DirectSum diff --git a/Fields/FieldOfFractions/Addition.agda b/Fields/FieldOfFractions/Addition.agda index 3f91267..04a0b5e 100644 --- a/Fields/FieldOfFractions/Addition.agda +++ b/Fields/FieldOfFractions/Addition.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -25,8 +25,7 @@ fieldOfFractionsPlus (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (((a * d) + (b * c)) 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 + ans pr | f = exFalso (d!=0 (f b!=0)) 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 diff --git a/Fields/FieldOfFractions/Field.agda b/Fields/FieldOfFractions/Field.agda index b5b5ec6..441be2a 100644 --- a/Fields/FieldOfFractions/Field.agda +++ b/Fields/FieldOfFractions/Field.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Group.agda b/Fields/FieldOfFractions/Group.agda index c73d7d7..1fee587 100644 --- a/Fields/FieldOfFractions/Group.agda +++ b/Fields/FieldOfFractions/Group.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Lemmas.agda b/Fields/FieldOfFractions/Lemmas.agda index 979d4e0..f352b4c 100644 --- a/Fields/FieldOfFractions/Lemmas.agda +++ b/Fields/FieldOfFractions/Lemmas.agda @@ -8,7 +8,7 @@ open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas open import Rings.Homomorphisms.Definition -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Multiplication.agda b/Fields/FieldOfFractions/Multiplication.agda index 14911d5..1c075df 100644 --- a/Fields/FieldOfFractions/Multiplication.agda +++ b/Fields/FieldOfFractions/Multiplication.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -25,8 +25,7 @@ fieldOfFractionsTimes (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (a * c) ,, ((b * d) 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 + ans pr | f = exFalso (d!=0 (f b!=0)) 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 diff --git a/Fields/FieldOfFractions/Order.agda b/Fields/FieldOfFractions/Order.agda index 22b37eb..c1c9cad 100644 --- a/Fields/FieldOfFractions/Order.agda +++ b/Fields/FieldOfFractions/Order.agda @@ -9,7 +9,7 @@ open import Rings.Orders.Partial.Definition open import Rings.Orders.Total.Definition open import Rings.Orders.Total.Lemmas open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -20,698 +20,694 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) 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 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 +open SetoidTotalOrder (TotallyOrderedRing.total order) +open import Rings.Orders.Partial.Lemmas +open PartiallyOrderedRing pRing - 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