patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-13 07:38:40 +00:00
Code Issues Packages Projects Releases Wiki Activity

Progress towards UFDs (#88)

Browse Source
This commit is contained in:
Patrick Stevens
2019-12-08 11:18:39 +00:00
committed by GitHub
parent 99c38495ce
commit 33098e94b0
20 changed files with 462 additions and 253 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
Rings/Ideals/Lemmas.agda
View File

@@ -70,3 +70,6 @@ Ideal.accumulatesTimes (inverseImageIsIdeal {_*2_ = _*2_} {f = f} fHom i) {g} {h
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)
generatorZeroImpliesMembersZero : {x : A} → generatedIdealPred R 0R x → x ∼ 0R
generatorZeroImpliesMembersZero {x} (a , b) = transitive (symmetric b) (transitive *Commutative timesZero)

15
Rings/Ideals/Maximal/Lemmas.agda
View File

@@ -26,7 +26,9 @@ open import Rings.Ideals.Prime.Lemmas
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) (proper : A) (isProper : pred proper → False) where
module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where
open import Rings.Divisible.Definition R
open Ring R
open Group additiveGroup
@@ -56,7 +58,7 @@ Field.allInvertible (idealMaximalImpliesQuotientField max) cosetA cosetA!=0 = an
ans'' : pred (inverse (Ring.1R (cosetRing R i)) + (ans' * cosetA))
ans'' with ans {1R}
ans'' | a , ((b , predCAb-a) ,, pred1-a) = Ideal.isSubset i (transitive (+WellDefined (invContravariant additiveGroup) reflexive) (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) *Commutative))) (Ideal.closedUnderPlus i (Ideal.closedUnderInverse i pred1-a) predCAb-a)
Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = isProper (Ideal.isSubset i (identIsIdent {proper}) (Ideal.accumulatesTimes i p))
Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = MaximalIdeal.notContainedIsNotContained max (Ideal.isSubset i (identIsIdent {MaximalIdeal.notContained (max {lzero})}) (Ideal.accumulatesTimes i p))
where
have : pred (inverse 1R)
have = Ideal.isSubset i identRight 1=0
@@ -64,8 +66,8 @@ Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = isProper (Ideal.is
p = Ideal.isSubset i (invTwice additiveGroup 1R) (Ideal.closedUnderInverse i have)
quotientFieldImpliesIdealMaximal : Field (cosetRing R i) → ({d : _} → MaximalIdeal i {d})
MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = proper
MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) = isProper
MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = Ring.1R (cosetRing R i)
MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) p1R = Field.nontrivial f (memberDividesImpliesMember R i p1R ((inverse 1R + 0R) , identIsIdent))
MaximalIdeal.isMaximal (quotientFieldImpliesIdealMaximal f) {bigger} biggerIdeal contained (a , (biggerA ,, notPredA)) = Ideal.isSubset biggerIdeal identIsIdent (Ideal.accumulatesTimes biggerIdeal v)
where
inv : Sg A (λ t → pred (inverse 1R + (t * a)))
@@ -89,3 +91,8 @@ idealMaximalImpliesIdealPrime max = quotientIntDomImpliesIdealPrime i f'
f = idealMaximalImpliesQuotientField max
f' : IntegralDomain (cosetRing R i)
f' = fieldIsIntDom f (λ p → Field.nontrivial f (Equivalence.symmetric (Setoid.eq (cosetSetoid additiveGroup (Ideal.isSubgroup i))) p))
maximalIdealWellDefined : {d : _} {pred2 : A → Set d} (i2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → {e : _} → MaximalIdeal i {e} → MaximalIdeal i2 {e}
MaximalIdeal.notContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) = notContained
MaximalIdeal.notContainedIsNotContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) p2Not = notContainedIsNotContained (p2ToP p2Not)
MaximalIdeal.isMaximal (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) {biggerPred} bigger pred2InBigger (r , (biggerPredR ,, notP2r)) {x} = isMaximal bigger (λ p → pred2InBigger (pToP2 p)) (r , (biggerPredR ,, λ p → notP2r (pToP2 p)))

5
Rings/Ideals/Prime/Lemmas.agda
View File

@@ -64,3 +64,8 @@ PrimeIdeal.isPrime (intDomImpliesZeroIdealPrime intDom) (c , 0=ab) 0not|a with I
... | b=0 = 0R , transitive timesZero (symmetric b=0)
PrimeIdeal.notContained (intDomImpliesZeroIdealPrime intDom) = 1R
PrimeIdeal.notContainedIsNotContained (intDomImpliesZeroIdealPrime intDom) (c , 0c=1) = IntegralDomain.nontrivial intDom (symmetric (transitive (symmetric (transitive *Commutative timesZero)) 0c=1))
primeIdealWellDefined : {c : _} {pred2 : A → Set c} (ideal2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → PrimeIdeal i → PrimeIdeal ideal2
PrimeIdeal.isPrime (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) p2ab notP2a = predToPred2 (isPrime (pred2ToPred p2ab) λ p → notP2a (predToPred2 p))
PrimeIdeal.notContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) = notContained
PrimeIdeal.notContainedIsNotContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) pred2Not = notContainedIsNotContained (pred2ToPred pred2Not)

6
Rings/Ideals/Principal/Definition.agda
View File

@@ -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; _⊔_)

23
Rings/Ideals/Principal/Lemmas.agda Normal file
View File

@@ -0,0 +1,23 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Ideals.Principal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
open Setoid S
open Ring R
open Equivalence eq
open import Rings.Ideals.Principal.Definition R
open import Rings.Ideals.Definition R
open import Rings.Ideals.Lemmas R
open import Rings.Divisible.Definition R
generatorZeroImpliesAllZero : {c : _} {pred : A → Set c} → {i : Ideal pred} → (princ : PrincipalIdeal i) → PrincipalIdeal.generator princ ∼ 0R → {x : A} → pred x → x ∼ 0R
generatorZeroImpliesAllZero record { generator = gen ; genIsInIdeal = genIsInIdeal ; genGenerates = genGenerates } gen=0 {x} predX = generatorZeroImpliesMembersZero {x} (divisibleWellDefined gen=0 reflexive (genGenerates predX))

29
Rings/PrincipalIdealDomains/Lemmas.agda
View File

@@ -20,15 +20,21 @@ 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 import Rings.Ideals.Prime.Definition {R = R}
open import Rings.Ideals.Prime.Lemmas {R = R}
open import Rings.Primes.Definition intDom
open import Rings.Primes.Lemmas intDom
open import Rings.Ideals.Principal.Lemmas R
open import Rings.Ideals.Maximal.Lemmas {R = 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})
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)
@@ -51,3 +57,18 @@ MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal r irred {d}) {biggerPred}
v r|bg | assoc = notInR (associateImpliesGeneratedIdealsEqual' assoc (PrincipalIdeal.genGenerates (pid bigger) biggerContainsOutside))
w : Unit biggerGen
w = dividesIrreducibleImpliesUnit irred u v
primeIdealIsMaximal : {c : _} {pred : A → Set c} → {i : Ideal pred} → (nonzero : Sg A (λ a → ((a ∼ 0R) → False) && pred a)) → PrimeIdeal i → {d : _} → MaximalIdeal i {d}
primeIdealIsMaximal {pred = pred} {i} (m , (m!=0 ,, predM)) prime {d = d} = maximalIdealWellDefined (generatedIdeal (PrincipalIdeal.generator princ)) i (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) (PrincipalIdeal.genGenerates princ) isMaximal
where
princ : PrincipalIdeal i
princ = pid i
isPrime : Prime (PrincipalIdeal.generator princ)
isPrime = primeIdealImpliesPrime (λ gen=0 → PrimeIdeal.notContainedIsNotContained prime (exFalso (m!=0 (generatorZeroImpliesAllZero princ gen=0 predM)))) (primeIdealWellDefined i (generatedIdeal (PrincipalIdeal.generator princ)) (PrincipalIdeal.genGenerates princ) (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) prime)
isIrreducible : Irreducible (PrincipalIdeal.generator princ)
isIrreducible = primeIsIrreducible isPrime
isMaximal : MaximalIdeal (generatedIdeal (PrincipalIdeal.generator princ)) {d}
isMaximal = irreducibleImpliesMaximalIdeal isIrreducible {d}
irreducibleImpliesPrime : {x : A} → Irreducible x → Prime x
irreducibleImpliesPrime {x} irred = primeIdealImpliesPrime (Irreducible.nonzero irred) (idealMaximalImpliesIdealPrime (generatedIdeal x) (irreducibleImpliesMaximalIdeal irred))

27
Rings/UniqueFactorisationDomains/Definition.agda Normal file
View File

@@ -0,0 +1,27 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Lists.Lists
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.UniqueFactorisationDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where
open import Rings.Units.Definition R
open import Rings.Irreducibles.Definition intDom
open Ring R
open Setoid S
record Factorisation {r : A} (nonzero : (r ∼ 0R) → False) (nonunit : (Unit r) → False) : Set (a ⊔ b) where
field
factorise : List A
factoriseIsFactorisation : fold (_*_) 1R factorise ∼ r
factoriseIsIrreducibles : allTrue Irreducible factorise
record UFD : Set (a ⊔ b) where
field
factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
uniqueFactorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → (f1 f2 : Factorisation nonzero nonunit) → {!Sg !}