From 99c38495cec28f65db1ac421b629015e76caacc4 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Sat, 7 Dec 2019 18:53:08 +0000
Subject: [PATCH] Irreducible and maximal (#87)

---
 Everything/Safe.agda                        |  2 +-
 Rings/Associates/Lemmas.agda                |  7 +++
 Rings/Ideals/Lemmas.agda                    |  5 ++
 Rings/Ideals/Principal/Definition.agda      |  8 +++-
 Rings/Irreducibles/Lemmas.agda              | 27 +++++++++++
 Rings/PrincipalIdealDomains/Definition.agda | 12 +----
 Rings/PrincipalIdealDomains/Lemmas.agda     | 53 +++++++++++++++++++++
 Rings/Units/Definition.agda                 |  6 ---
 Rings/Units/Lemmas.agda                     | 22 +++++++++
 9 files changed, 123 insertions(+), 19 deletions(-)
 create mode 100644 Rings/Irreducibles/Lemmas.agda
 create mode 100644 Rings/PrincipalIdealDomains/Lemmas.agda
 create mode 100644 Rings/Units/Lemmas.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 91d8159..e62f9f5 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -67,7 +67,7 @@ open import Rings.Ideals.Prime.Definition
 open import Rings.Ideals.Prime.Lemmas
 open import Rings.Ideals.Principal.Definition
 open import Rings.IntegralDomains.Examples
-open import Rings.PrincipalIdealDomains.Definition
+open import Rings.PrincipalIdealDomains.Lemmas
 open import Rings.Subrings.Definition
 open import Rings.Ideals.Maximal.Lemmas
 open import Rings.Primes.Lemmas
diff --git a/Rings/Associates/Lemmas.agda b/Rings/Associates/Lemmas.agda
index 9f0b2b3..0f46171 100644
--- a/Rings/Associates/Lemmas.agda
+++ b/Rings/Associates/Lemmas.agda
@@ -22,6 +22,7 @@ open import Rings.Divisible.Definition R
 open import Rings.IntegralDomains.Lemmas intDom
 open import Rings.Associates.Definition intDom
 open import Rings.Units.Definition R
+open import Rings.Ideals.Definition R
 open Setoid S
 open Ring R
 open Equivalence eq
@@ -42,3 +43,9 @@ mutualDivisionImpliesAssociate' {a} {b} (r , ar=b) (s , bs=a) a=0 = 1R , ((1R ,
   where
     b=0 : b ∼ 0R
     b=0 = transitive (symmetric ar=b) (transitive (transitive *Commutative (*WellDefined reflexive a=0)) (timesZero {r}))
+
+associateImpliesGeneratedIdealsEqual : {a b : A} → Associates a b → {x : A} → generatedIdealPred a x → generatedIdealPred b x
+associateImpliesGeneratedIdealsEqual {a} {b} (r , ((s , rs=1) ,, a=br)) {x} (c , ac=x) = (r * c) , transitive *Associative (transitive (*WellDefined (symmetric a=br) reflexive) ac=x)
+
+associateImpliesGeneratedIdealsEqual' : {a b : A} → Associates a b → {x : A} → generatedIdealPred b x → generatedIdealPred a x
+associateImpliesGeneratedIdealsEqual' assoc = associateImpliesGeneratedIdealsEqual (Equivalence.symmetric associatesEquiv assoc)
diff --git a/Rings/Ideals/Lemmas.agda b/Rings/Ideals/Lemmas.agda
index c5854fb..8a4d162 100644
--- a/Rings/Ideals/Lemmas.agda
+++ b/Rings/Ideals/Lemmas.agda
@@ -23,6 +23,8 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Rings.Ideals.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
 
+open import Rings.Divisible.Definition R
+
 idealPredForKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → A → Set d
 idealPredForKernel {T = T} R2 {f} fHom a = Setoid._∼_ T (f a) (Ring.0R R2)
 
@@ -65,3 +67,6 @@ Subgroup.closedUnderPlus (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) {g} {h}
 Subgroup.containsIdentity (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) = 0G , (Ideal.containsIdentity i ,, imageOfIdentityIsIdentity (RingHom.groupHom fHom))
 Subgroup.closedUnderInverse (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) (a , (prA ,, fg=a)) = inverse a , (Ideal.closedUnderInverse i prA ,, transitive (homRespectsInverse (RingHom.groupHom fHom)) (inverseWellDefined additiveGroup fg=a))
 Ideal.accumulatesTimes (inverseImageIsIdeal {_*2_ = _*2_} {f = f} fHom i) {g} {h} (a , (prA ,, fg=a)) = (a * f h) , (Ideal.accumulatesTimes i prA ,, transitive (RingHom.ringHom fHom) (*WellDefined fg=a reflexive))
+
+memberDividesImpliesMember : {a b : A} → {c : _} → {pred : A → Set c} → (i : Ideal R pred) → pred a → a ∣ b → pred b
+memberDividesImpliesMember {a} {b} i pA (s , as=b) = Ideal.isSubset i as=b (Ideal.accumulatesTimes i pA)
diff --git a/Rings/Ideals/Principal/Definition.agda b/Rings/Ideals/Principal/Definition.agda
index d45d4bc..6cccfda 100644
--- a/Rings/Ideals/Principal/Definition.agda
+++ b/Rings/Ideals/Principal/Definition.agda
@@ -18,7 +18,11 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 module Rings.Ideals.Principal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
 
 open import Rings.Ideals.Definition R
+open import Rings.Divisible.Definition R
 open Setoid S
 
-PrincipalIdeal : {c : _} {pred : A → Set c} (ideal : Ideal pred) → Set (a ⊔ b ⊔ c)
-PrincipalIdeal {pred = pred} ideal = Sg A (λ a → {x : A} → (pred x) → Sg A (λ c → (a * c) ∼ x))
+record PrincipalIdeal {c : _} {pred : A → Set c} (ideal : Ideal pred) : Set (a ⊔ b ⊔ c) where
+  field
+    generator : A
+    genIsInIdeal : pred generator
+    genGenerates : {x : A} → pred x → generator ∣ x
diff --git a/Rings/Irreducibles/Lemmas.agda b/Rings/Irreducibles/Lemmas.agda
new file mode 100644
index 0000000..54a5376
--- /dev/null
+++ b/Rings/Irreducibles/Lemmas.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Sets.EquivalenceRelations
+open import Rings.IntegralDomains.Definition
+open import Rings.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Irreducibles.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
+
+open import Rings.Irreducibles.Definition intDom
+open import Rings.Divisible.Definition R
+open import Rings.Units.Definition R
+open import Rings.Associates.Definition intDom
+
+open Setoid S
+open Equivalence eq
+open Ring R
+
+dividesIrreducibleImpliesUnit : {r c : A} → Irreducible r → c ∣ r → (r ∣ c → False) → Unit c
+dividesIrreducibleImpliesUnit {r} {c} irred (x , cx=r) notAssoc = Irreducible.irreducible irred x c (transitive *Commutative cx=r) nonunit
+  where
+    nonunit : Unit x → False
+    nonunit (a , xa=1) = notAssoc (a , transitive (transitive (transitive (transitive (*WellDefined (symmetric cx=r) reflexive) (symmetric *Associative)) *Commutative) (*WellDefined xa=1 reflexive)) identIsIdent)
diff --git a/Rings/PrincipalIdealDomains/Definition.agda b/Rings/PrincipalIdealDomains/Definition.agda
index 5353637..70ddfcd 100644
--- a/Rings/PrincipalIdealDomains/Definition.agda
+++ b/Rings/PrincipalIdealDomains/Definition.agda
@@ -1,21 +1,13 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
 open import LogicalFormulae
-open import Groups.Groups
-open import Groups.Homomorphisms.Definition
-open import Groups.Definition
-open import Numbers.Naturals.Naturals
-open import Setoids.Orders
 open import Setoids.Setoids
-open import Functions
-open import Sets.EquivalenceRelations
 open import Rings.Definition
-open import Rings.Homomorphisms.Definition
-open import Groups.Homomorphisms.Lemmas
+open import Rings.IntegralDomains.Definition
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
-module Rings.PrincipalIdealDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+module Rings.PrincipalIdealDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
 
 open import Rings.Ideals.Principal.Definition R
 open import Rings.Ideals.Definition R
diff --git a/Rings/PrincipalIdealDomains/Lemmas.agda b/Rings/PrincipalIdealDomains/Lemmas.agda
new file mode 100644
index 0000000..f8f6103
--- /dev/null
+++ b/Rings/PrincipalIdealDomains/Lemmas.agda
@@ -0,0 +1,53 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Sets.EquivalenceRelations
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.PrincipalIdealDomains.Definition
+open import Rings.IntegralDomains.Definition
+open import Rings.Ideals.Maximal.Definition
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.PrincipalIdealDomains.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) (pid : {c : _} → PrincipalIdealDomain intDom {c}) where
+
+open import Rings.Ideals.Definition R
+open import Rings.Irreducibles.Definition intDom
+open import Rings.Ideals.Principal.Definition R
+open import Rings.Divisible.Definition R
+open import Rings.Associates.Lemmas intDom
+open import Rings.Ideals.Lemmas R
+open import Rings.Units.Definition R
+open import Rings.Irreducibles.Lemmas intDom
+open import Rings.Units.Lemmas R
+
+open Ring R
+open Setoid S
+open Equivalence eq
+
+irreducibleImpliesMaximalIdeal : (r : A) → Irreducible r → {d : _} → MaximalIdeal (generatedIdeal r) {d}
+MaximalIdeal.notContained (irreducibleImpliesMaximalIdeal r irred {d}) = 1R
+MaximalIdeal.notContainedIsNotContained (irreducibleImpliesMaximalIdeal r irred {d}) = Irreducible.nonunit irred
+MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal r irred {d}) {biggerPred} bigger biggerContains (outsideR , (biggerContainsOutside ,, notInR)) {x} = biggerPrincipal' (unitImpliesGeneratedIdealEverything w {x})
+  where
+    biggerGen : A
+    biggerGen = PrincipalIdeal.generator (pid bigger)
+    biggerPrincipal : {x : A} → biggerPred x → biggerGen ∣ x
+    biggerPrincipal = PrincipalIdeal.genGenerates (pid bigger)
+    bp : biggerPred biggerGen
+    bp = PrincipalIdeal.genIsInIdeal (pid bigger)
+    biggerPrincipal' : {x : A} → biggerGen ∣ x → biggerPred x
+    biggerPrincipal' {y} bg|y = memberDividesImpliesMember bigger bp bg|y
+    u : biggerGen ∣ r
+    u = biggerPrincipal (biggerContains (1R , transitive *Commutative identIsIdent))
+    biggerGenNonzero : biggerGen ∼ 0R → False
+    biggerGenNonzero bg=0 = notInR (Ideal.isSubset (generatedIdeal r) (symmetric t) (Ideal.containsIdentity (generatedIdeal r)))
+      where
+        t : outsideR ∼ 0R
+        t with biggerPrincipal {outsideR} biggerContainsOutside
+        ... | mult , pr = transitive (symmetric pr) (transitive (*WellDefined bg=0 reflexive) (transitive *Commutative timesZero))
+    v : (r ∣ biggerGen) → False
+    v r|bg with mutualDivisionImpliesAssociate r|bg u (Irreducible.nonzero irred)
+    v r|bg | assoc = notInR (associateImpliesGeneratedIdealsEqual' assoc (PrincipalIdeal.genGenerates (pid bigger) biggerContainsOutside))
+    w : Unit biggerGen
+    w = dividesIrreducibleImpliesUnit irred u v
diff --git a/Rings/Units/Definition.agda b/Rings/Units/Definition.agda
index d7ab33f..a18b095 100644
--- a/Rings/Units/Definition.agda
+++ b/Rings/Units/Definition.agda
@@ -1,17 +1,11 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
 open import LogicalFormulae
-open import Groups.Groups
-open import Groups.Homomorphisms.Definition
-open import Groups.Definition
-open import Numbers.Naturals.Naturals
-open import Setoids.Orders
 open import Setoids.Setoids
 open import Functions
 open import Sets.EquivalenceRelations
 open import Rings.Definition
 open import Rings.Homomorphisms.Definition
-open import Groups.Homomorphisms.Lemmas
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
diff --git a/Rings/Units/Lemmas.agda b/Rings/Units/Lemmas.agda
new file mode 100644
index 0000000..67a9564
--- /dev/null
+++ b/Rings/Units/Lemmas.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Units.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open import Rings.Units.Definition R
+open import Rings.Ideals.Definition R
+
+open Ring R
+open Setoid S
+open Equivalence eq
+
+unitImpliesGeneratedIdealEverything : {x : A} → Unit x → {y : A} → generatedIdealPred x y
+unitImpliesGeneratedIdealEverything {x} (a , xa=1) {y} = (a * y) , transitive *Associative (transitive (*WellDefined xa=1 reflexive) identIsIdent)