mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-11 06:38:39 +00:00
Quotient ring (#81)
This commit is contained in:
Patrick Stevens
GitHub
49
Rings/Cosets.agda
Normal file
49
Rings/Cosets.agda
Normal file
@@ -0,0 +1,49 @@
|
||||
{-# OPTIONS --warning=error --safe --without-K #-}
|
||||
|
||||
open import Functions
|
||||
open import Sets.FinSet
|
||||
open import LogicalFormulae
|
||||
open import Groups.Definition
|
||||
open import Groups.Groups
|
||||
open import Groups.FiniteGroups.Definition
|
||||
open import Rings.Homomorphisms.Definition
|
||||
open import Groups.Homomorphisms.Definition
|
||||
open import Groups.Abelian.Definition
|
||||
open import Setoids.Setoids
|
||||
open import Rings.Definition
|
||||
open import Fields.FieldOfFractions.Setoid
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Groups.Lemmas
|
||||
open import Groups.Subgroups.Definition
|
||||
open import Groups.QuotientGroup.Definition
|
||||
open import Rings.Ideals.Definition
|
||||
|
||||
module Rings.Cosets {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) {pred : A → Set c} (ideal : Ideal R pred) where
|
||||
|
||||
open Ring R
|
||||
open import Rings.Lemmas R
|
||||
open import Groups.Subgroups.Normal.Lemmas
|
||||
|
||||
open import Groups.Cosets additiveGroup (Ideal.isSubgroup ideal)
|
||||
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
open Ideal ideal
|
||||
open Group additiveGroup
|
||||
|
||||
cosetRing : Ring cosetSetoid _+_ _*_
|
||||
Ring.additiveGroup cosetRing = cosetGroup (abelianGroupSubgroupIsNormal (Ideal.isSubgroup ideal) abelianUnderlyingGroup)
|
||||
Ring.*WellDefined cosetRing {r} {s} {t} {u} r=t s=u = need
|
||||
where
|
||||
r=t' : pred ((inverse t + r) * u)
|
||||
r=t' = accumulatesTimes r=t
|
||||
s=u' : pred ((inverse u + s) * r)
|
||||
s=u' = accumulatesTimes s=u
|
||||
need : pred (inverse (t * u) + (r * s))
|
||||
need = isSubset (transitive (+WellDefined (*DistributesOver+') *DistributesOver+') (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined ringMinusExtracts' (transitive (+WellDefined reflexive (transitive ringMinusExtracts' (inverseWellDefined additiveGroup *Commutative))) invRight)) identRight)) *Commutative))) (closedUnderPlus r=t' s=u')
|
||||
Ring.1R cosetRing = 1R
|
||||
Ring.groupIsAbelian cosetRing = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup groupIsAbelian) reflexive)) containsIdentity
|
||||
Ring.*Associative cosetRing = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup *Associative) reflexive)) containsIdentity
|
||||
Ring.*Commutative cosetRing {a} {b} = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup *Commutative) reflexive)) containsIdentity
|
||||
Ring.*DistributesOver+ cosetRing = isSubset (symmetric (transitive (+WellDefined (inverseWellDefined additiveGroup (symmetric *DistributesOver+)) reflexive) invLeft)) containsIdentity
|
||||
Ring.identIsIdent cosetRing = isSubset (symmetric (transitive (Group.+WellDefined additiveGroup reflexive identIsIdent) invLeft)) containsIdentity
|
||||
@@ -22,8 +22,14 @@ open import Groups.Subgroups.Definition (Ring.additiveGroup R)
|
||||
ringKernel : {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) → Set (a ⊔ d)
|
||||
ringKernel {T = T} R2 {f} fHom = Sg A (λ a → Setoid._∼_ T (f a) (Ring.0R R2))
|
||||
|
||||
ideal : {c : _} (pred : A → Set c) → Set (a ⊔ b ⊔ c)
|
||||
ideal pred = subgroup pred && ({x : A} → {y : A} → pred x → pred (x * y))
|
||||
record Ideal {c : _} (pred : A → Set c) : Set (a ⊔ b ⊔ c) where
|
||||
field
|
||||
isSubgroup : Subgroup pred
|
||||
accumulatesTimes : {x : A} → {y : A} → pred x → pred (x * y)
|
||||
closedUnderPlus = Subgroup.closedUnderPlus isSubgroup
|
||||
closedUnderInverse = Subgroup.closedUnderInverse isSubgroup
|
||||
containsIdentity = Subgroup.containsIdentity isSubgroup
|
||||
isSubset = Subgroup.isSubset isSubgroup
|
||||
|
||||
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)
|
||||
@@ -31,22 +37,22 @@ idealPredForKernel {T = T} R2 {f} fHom a = Setoid._∼_ T (f a) (Ring.0R R2)
|
||||
idealPredForKernelWellDefined : {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) → {x y : A} → (Setoid._∼_ S x y) → (idealPredForKernel R2 fHom x → idealPredForKernel R2 fHom y)
|
||||
idealPredForKernelWellDefined {T = T} R2 {f} fHom a x=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined (RingHom.groupHom fHom) (Equivalence.symmetric (Setoid.eq S) a)) x=0
|
||||
|
||||
kernelIdealIsIdeal : {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) → ideal (idealPredForKernel R2 fHom)
|
||||
_&&_.fst (_&&_.fst (kernelIdealIsIdeal {R2 = R2} fHom)) = idealPredForKernelWellDefined R2 fHom
|
||||
_&_&_.one (_&&_.snd (_&&_.fst (kernelIdealIsIdeal {T = T} {R2 = R2} fHom))) {x} {y} fx=0 fy=0 = transitive (transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fx=0 fy=0)) identLeft
|
||||
kernelIdealIsIdeal : {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) → Ideal (idealPredForKernel R2 fHom)
|
||||
Subgroup.isSubset (Ideal.isSubgroup (kernelIdealIsIdeal {R2 = R2} fHom)) = idealPredForKernelWellDefined R2 fHom
|
||||
Subgroup.closedUnderPlus (Ideal.isSubgroup (kernelIdealIsIdeal {T = T} {R2 = R2} fHom)) {x} {y} fx=0 fy=0 = transitive (transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fx=0 fy=0)) identLeft
|
||||
where
|
||||
open Ring R2
|
||||
open Group (Ring.additiveGroup R2)
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
_&_&_.two (_&&_.snd (_&&_.fst (kernelIdealIsIdeal fHom))) = imageOfIdentityIsIdentity (RingHom.groupHom fHom)
|
||||
_&_&_.three (_&&_.snd (_&&_.fst (kernelIdealIsIdeal {T = T} {R2 = R2} fHom))) {x} fx=0 = zeroImpliesInverseZero (RingHom.groupHom fHom) fx=0
|
||||
Subgroup.containsIdentity (Ideal.isSubgroup (kernelIdealIsIdeal fHom)) = imageOfIdentityIsIdentity (RingHom.groupHom fHom)
|
||||
Subgroup.closedUnderInverse (Ideal.isSubgroup (kernelIdealIsIdeal {T = T} {R2 = R2} fHom)) {x} fx=0 = zeroImpliesInverseZero (RingHom.groupHom fHom) fx=0
|
||||
where
|
||||
open Ring R2
|
||||
open Group (Ring.additiveGroup R2)
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
_&&_.snd (kernelIdealIsIdeal {T = T} {R2 = R2} {f = f} fHom) {x} {y} fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2 {f y})))
|
||||
Ideal.accumulatesTimes (kernelIdealIsIdeal {T = T} {R2 = R2} {f = f} fHom) {x} {y} fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2 {f y})))
|
||||
where
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
|
||||
@@ -3,6 +3,7 @@
|
||||
open import LogicalFormulae
|
||||
open import Functions
|
||||
open import Groups.Groups
|
||||
open import Groups.Abelian.Definition
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
@@ -54,3 +55,6 @@ abstract
|
||||
|
||||
charNot2ImpliesNontrivial : ((1R + 1R) ∼ 0R → False) → (0R ∼ 1R) → False
|
||||
charNot2ImpliesNontrivial charNot2 0=1 = charNot2 (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.symmetric eq 0=1)) identRight)
|
||||
|
||||
abelianUnderlyingGroup : AbelianGroup additiveGroup
|
||||
abelianUnderlyingGroup = record { commutative = groupIsAbelian }
|
||||
|
||||
@@ -20,20 +20,20 @@ module Rings.Quotients.Definition {a b c d : _} {A : Set a} {B : Set b} {S : Set
|
||||
|
||||
open import Groups.QuotientGroup.Lemmas (Ring.additiveGroup R) (Ring.additiveGroup R2) (RingHom.groupHom f)
|
||||
|
||||
quotientRing : Ring (quotientGroupSetoid (Ring.additiveGroup R) (RingHom.groupHom f)) _+A_ _*A_
|
||||
Ring.additiveGroup quotientRing = quotientGroupByHom (Ring.additiveGroup R) (RingHom.groupHom f)
|
||||
Ring.*WellDefined quotientRing fr=ft fs=fu = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (transitive (RingHom.ringHom f) (transitive (Ring.*WellDefined R2 (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fr=ft) (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fs=fu)) (symmetric (RingHom.ringHom f))))
|
||||
quotientByRingHom : Ring (quotientGroupSetoid (Ring.additiveGroup R) (RingHom.groupHom f)) _+A_ _*A_
|
||||
Ring.additiveGroup quotientByRingHom = quotientGroupByHom (Ring.additiveGroup R) (RingHom.groupHom f)
|
||||
Ring.*WellDefined quotientByRingHom fr=ft fs=fu = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (transitive (RingHom.ringHom f) (transitive (Ring.*WellDefined R2 (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fr=ft) (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fs=fu)) (symmetric (RingHom.ringHom f))))
|
||||
where
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
Ring.1R quotientRing = Ring.1R R
|
||||
Ring.groupIsAbelian quotientRing = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.groupIsAbelian R))
|
||||
Ring.*Associative quotientRing = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Associative R))
|
||||
Ring.*Commutative quotientRing = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Commutative R))
|
||||
Ring.*DistributesOver+ quotientRing = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*DistributesOver+ R))
|
||||
Ring.identIsIdent quotientRing = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.identIsIdent R))
|
||||
Ring.1R quotientByRingHom = Ring.1R R
|
||||
Ring.groupIsAbelian quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.groupIsAbelian R))
|
||||
Ring.*Associative quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Associative R))
|
||||
Ring.*Commutative quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Commutative R))
|
||||
Ring.*DistributesOver+ quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*DistributesOver+ R))
|
||||
Ring.identIsIdent quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.identIsIdent R))
|
||||
|
||||
projectionMapIsHom : RingHom R quotientRing id
|
||||
projectionMapIsHom : RingHom R quotientByRingHom id
|
||||
RingHom.preserves1 projectionMapIsHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (Equivalence.reflexive (Setoid.eq T))
|
||||
RingHom.ringHom projectionMapIsHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (Equivalence.reflexive (Setoid.eq T))
|
||||
RingHom.groupHom projectionMapIsHom = projectionMapIsGroupHom
|
||||
|
||||
Reference in New Issue
Block a user