Skip to content

Commit 441d612

Browse files
TanebTaneb
committed
Chinese remainder theorem
1 parent 851001d commit 441d612

File tree

5 files changed

+177
-50
lines changed

5 files changed

+177
-50
lines changed

‎src/Algebra/Construct/Quotient/Group.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
open import Algebra.Bundles using (Group)
1010
open import Algebra.NormalSubgroup using (NormalSubgroup)
1111

12-
module Algebra.Construct.Quotient.Group {c ℓ c′ ℓ′} (G : Group c ℓ) (N : NormalSubgroup G c′ ℓ′) where
12+
module Algebra.Construct.Quotient.Group {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
1313

1414
open Group G
1515

‎src/Algebra/Construct/Quotient/Ring.agda

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,15 @@
66

77
{-# OPTIONS --safe --cubical-compatible #-}
88

9-
open import Algebra.Bundles using (Ring)
9+
open import Algebra.Bundles using (Ring; RawRing)
1010
open import Algebra.Ideal using (Ideal)
1111

12-
module Algebra.Construct.Quotient.Ring {c ℓ c′ ℓ′} (R : Ring c ℓ) (I : Ideal R c′ ℓ′) where
12+
module Algebra.Construct.Quotient.Ring {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) where
1313

1414
open Ring R
1515
open Ideal I
1616

17-
open import Algebra.Construct.Quotient.Group +-group normalSubgroup
18-
public
17+
open import Algebra.Construct.Quotient.Group +-group normalSubgroup public
1918
using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup)
2019
renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)
2120

@@ -37,6 +36,17 @@ open import Relation.Binary.Reasoning.Setoid setoid
3736
ι (j I.*ᵣ u) + ι (y I.*ₗ k) ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨
3837
ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k) ∎
3938

39+
quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
40+
quotientRawRing = record
41+
{ Carrier = Carrier
42+
; _≈_ = _≋_
43+
; _+_ = _+_
44+
; _*_ = _*_
45+
; -_ = -_
46+
; 0# = 0#
47+
; 1# = 1#
48+
}
49+
4050
quotientIsRing : IsRing _≋_ _+_ _*_ (-_) 0# 1#
4151
quotientIsRing = record
4252
{ +-isAbelianGroup = record

‎src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
------------------------------------------------------------------------
2+
-- The Chinese Remainder Theorem for arbitrary rings
3+
--
4+
-- The Agda standard library
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles
10+
11+
module Algebra.Construct.Quotient.Ring.Properties.ChineseRemainderTheorem {c ℓ} (R : Ring c ℓ) where
12+
13+
open Ring R
14+
15+
import Algebra.Construct.DirectProduct as DP
16+
open import Algebra.Construct.Quotient.Ring as QR using (quotientRawRing)
17+
open import Algebra.Ideal R
18+
open import Algebra.Ideal.Coprimality R using (Coprime)
19+
open import Algebra.Ideal.Construct.Intersection R
20+
open import Algebra.Morphism.Structures
21+
open import Algebra.Properties.Ring R
22+
open import Data.Product.Base
23+
open import Relation.Binary.Reasoning.Setoid setoid
24+
25+
module _
26+
{c₁ c₂ ℓ₁ ℓ₂}
27+
(I : Ideal c₁ ℓ₁) (J : Ideal c₂ ℓ₂)
28+
where
29+
30+
private
31+
module I = Ideal I
32+
module J = Ideal J
33+
34+
CRT : Coprime I J → IsRingIsomorphism (quotientRawRing R (I ∩ J)) (DP.rawRing (quotientRawRing R I) (quotientRawRing R J)) λ x → x , x
35+
CRT ((m , n) , m+n≈1) = record
36+
{ isRingMonomorphism = record
37+
{ isRingHomomorphism = record
38+
{ isSemiringHomomorphism = record
39+
{ isNearSemiringHomomorphism = record
40+
{ +-isMonoidHomomorphism = record
41+
{ isMagmaHomomorphism = record
42+
{ isRelHomomorphism = record
43+
{ cong = λ { (t R/I∩J.by p) → (ICarrier.a t R/I.by p) , (ICarrier.b t R/J.by trans p (ICarrier.a≈b t)) }
44+
}
45+
; homo = λ x y → R/I.≋-refl , R/J.≋-refl
46+
}
47+
; ε-homo = R/I.≋-refl , R/J.≋-refl
48+
}
49+
; *-homo = λ x y → R/I.≋-refl , R/J.≋-refl
50+
}
51+
; 1#-homo = R/I.≋-refl , R/J.≋-refl
52+
}
53+
; -‿homo = λ x → R/I.≋-refl , R/J.≋-refl
54+
}
55+
; injective = λ {((i R/I.by p) , (j R/J.by q)) → record { a≈b = trans (sym p) q } R/I∩J.by p}
56+
}
57+
; surjective = λ (a₁ , a₂) → a₁ * J.ι n + a₂ * I.ι m , λ {z} → λ
58+
{ (record {a = a; b = b; a≈b = a≈b} R/I∩J.by p) → record
59+
{ fst = a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m R/I.by begin
60+
-- introduce a coprimality term
61+
z - a₁ ≈⟨ +-congˡ (-‿cong (*-identityʳ a₁)) ⟨
62+
z - a₁ * 1# ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨
63+
-- lots and lots of rearrangement
64+
z - a₁ * (I.ι m + J.ι n) ≈⟨ +-congˡ (-‿cong (distribˡ a₁ (I.ι m) (J.ι n))) ⟩
65+
z - (a₁ * I.ι m + a₁ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-comm (a₁ * I.ι m) (a₁ * J.ι n))) ⟩
66+
z - (a₁ * J.ι n + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₁ * J.ι n)))) ⟨
67+
z - (a₁ * J.ι n + 0# + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₂ * I.ι m))))) ⟨
68+
z - (a₁ * J.ι n + (a₂ * I.ι m - a₂ * I.ι m) + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc _ _ _))) ⟨
69+
z - (a₁ * J.ι n + a₂ * I.ι m - a₂ * I.ι m + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-assoc _ _ _)) ⟩
70+
z - (a₁ * J.ι n + a₂ * I.ι m + (- (a₂ * I.ι m) + a₁ * I.ι m)) ≈⟨ +-congˡ (-‿+-comm _ _) ⟨
71+
z + (- (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m)) ≈⟨ +-assoc z _ _ ⟨
72+
z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m) ≈⟨ +-congˡ (-‿+-comm _ _) ⟨
73+
z - (a₁ * J.ι n + a₂ * I.ι m) + (- - (a₂ * I.ι m) - a₁ * I.ι m) ≈⟨ +-congˡ (+-congʳ (-‿involutive _)) ⟩
74+
z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ * I.ι m - a₁ * I.ι m) ≈⟨ +-congˡ ([y-z]x≈yx-zx _ _ _) ⟨
75+
-- substitute z-t
76+
z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ - a₁) * I.ι m ≈⟨ +-congʳ p ⟩
77+
-- show we're in I
78+
I.ι a + (a₂ - a₁) * I.ι m ≈⟨ +-congˡ (I.ι.*ₗ-homo (a₂ - a₁) m) ⟨
79+
I.ι a + I.ι ((a₂ - a₁) I.I.*ₗ m) ≈⟨ I.ι.+ᴹ-homo a _ ⟨
80+
I.ι (a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m) ∎
81+
; snd = b J.I.+ᴹ (a₁ - a₂) J.I.*ₗ n R/J.by begin
82+
-- introduce a coprimality term
83+
z - a₂ ≈⟨ +-congˡ (-‿cong (*-identityʳ a₂)) ⟨
84+
z - a₂ * 1# ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨
85+
-- lots and lots of rearrangement
86+
z - a₂ * (I.ι m + J.ι n) ≈⟨ +-congˡ (-‿cong (distribˡ a₂ (I.ι m) (J.ι n))) ⟩
87+
z - (a₂ * I.ι m + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₂ * I.ι m)))) ⟨
88+
z - (a₂ * I.ι m + 0# + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₁ * J.ι n))))) ⟨
89+
z - (a₂ * I.ι m + (a₁ * J.ι n - a₁ * J.ι n) + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc (a₂ * I.ι m) (a₁ * J.ι n) _))) ⟨
90+
z - (a₂ * I.ι m + a₁ * J.ι n - a₁ * J.ι n + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-assoc (a₂ * I.ι m + a₁ * J.ι n) (- (a₁ * J.ι n)) _)) ⟩
91+
z - (a₂ * I.ι m + a₁ * J.ι n + (- (a₁ * J.ι n) + a₂ * J.ι n)) ≈⟨ +-congˡ (-‿+-comm (a₂ * I.ι m + a₁ * J.ι n) (- (a₁ * J.ι n) + a₂ * J.ι n)) ⟨
92+
z + (- (a₂ * I.ι m + a₁ * J.ι n) - (- (a₁ * J.ι n) + a₂ * J.ι n)) ≈⟨ +-assoc z (- (a₂ * I.ι m + a₁ * J.ι n)) (- (- (a₁ * J.ι n) + a₂ * J.ι n)) ⟨
93+
z - (a₂ * I.ι m + a₁ * J.ι n) - (- (a₁ * J.ι n) + a₂ * J.ι n) ≈⟨ +-cong (+-congˡ (-‿cong (+-comm _ _))) (-‿cong (+-congˡ (-‿involutive _))) ⟨
94+
z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₁ * J.ι n) - - (a₂ * J.ι n)) ≈⟨ +-congˡ (-‿cong (-‿+-comm (a₁ * J.ι n) (- (a₂ * J.ι n)))) ⟩
95+
z - (a₁ * J.ι n + a₂ * I.ι m) - - (a₁ * J.ι n - a₂ * J.ι n) ≈⟨ +-congˡ (-‿involutive (a₁ * J.ι n - a₂ * J.ι n)) ⟩
96+
z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ * J.ι n - a₂ * J.ι n) ≈⟨ +-congˡ ([y-z]x≈yx-zx (J.ι n) a₁ a₂) ⟨
97+
-- substitute z-t
98+
z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ - a₂) * J.ι n ≈⟨ +-congʳ (trans p a≈b) ⟩
99+
-- show we're in I
100+
J.ι b + (a₁ - a₂) * J.ι n ≈⟨ +-congˡ (J.ι.*ₗ-homo (a₁ - a₂) n) ⟨
101+
J.ι b + J.ι ((a₁ - a₂) J.I.*ₗ n) ≈⟨ J.ι.+ᴹ-homo b ((a₁ - a₂) J.I.*ₗ n) ⟨
102+
J.ι (b J.I.+ᴹ (a₁ - a₂) J.I.*ₗ n) ∎
103+
}
104+
}
105+
}
106+
where
107+
module R/I = QR R I
108+
module R/J = QR R J
109+
module R/I∩J = QR R (I ∩ J)

‎src/Algebra/Ideal/Construct/Intersection.agda

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -20,27 +20,27 @@ open import Function.Base
2020
open import Level
2121
open import Relation.Binary.Reasoning.Setoid setoid
2222

23+
open NS public using (ICarrier; icarrier)
24+
2325
_∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → Ideal c₁ ℓ₁ → Ideal c₂ ℓ₂ → Ideal (ℓ ⊔ c₁ ⊔ c₂) ℓ₁
2426
I ∩ J = record
2527
{ I = record
2628
{ Carrierᴹ = NSI.N.Carrier
2729
; _≈ᴹ_ = NSI.N._≈_
2830
; _+ᴹ_ = NSI.N._∙_
29-
; _*ₗ_ = λ r ((i , j) , p) → record
30-
{ fst = r I.I.*ₗ i , r J.I.*ₗ j
31-
; snd = begin
32-
I.ι (r I.I.*ₗ i) ≈⟨ I.ι.*ₗ-homo r i ⟩
33-
r * I.ι i ≈⟨ *-congˡ p ⟩
34-
r * J.ι j ≈⟨ J.ι.*ₗ-homo r j ⟨
35-
J.ι (r J.I.*ₗ j) ∎
31+
; _*ₗ_ = λ r p → record
32+
{ a≈b = begin
33+
I.ι (r I.I.*ₗ _) ≈⟨ I.ι.*ₗ-homo r _ ⟩
34+
r * I.ι _ ≈⟨ *-congˡ (NS.ICarrier.a≈b p) ⟩
35+
r * J.ι _ ≈⟨ J.ι.*ₗ-homo r _ ⟨
36+
J.ι (r J.I.*ₗ _) ∎
3637
}
37-
; _*ᵣ_ = λ ((i , j) , p) r → record
38-
{ fst = i I.I.*ᵣ r , j J.I.*ᵣ r
39-
; snd = begin
40-
I.ι (i I.I.*ᵣ r) ≈⟨ I.ι.*ᵣ-homo r i ⟩
41-
I.ι i * r ≈⟨ *-congʳ p ⟩
42-
J.ι j * r ≈⟨ J.ι.*ᵣ-homo r j ⟨
43-
J.ι (j J.I.*ᵣ r) ∎
38+
; _*ᵣ_ = λ p r → record
39+
{ a≈b = begin
40+
I.ι (_ I.I.*ᵣ r) ≈⟨ I.ι.*ᵣ-homo r _ ⟩
41+
I.ι _ * r ≈⟨ *-congʳ (NS.ICarrier.a≈b p) ⟩
42+
J.ι _ * r ≈⟨ J.ι.*ᵣ-homo r _ ⟨
43+
J.ι (_ J.I.*ᵣ r) ∎
4444
}
4545
; 0ᴹ = NSI.N.ε
4646
; -ᴹ_ = NSI.N._⁻¹
@@ -50,8 +50,8 @@ I ∩ J = record
5050
{ isModuleHomomorphism = record
5151
{ isBimoduleHomomorphism = record
5252
{ +ᴹ-isGroupHomomorphism = NSI.ι.isGroupHomomorphism
53-
; *ₗ-homo = λ r ((i , _) , _) → I.ι.*ₗ-homo r i
54-
; *ᵣ-homo = λ r ((i , _) , _) → I.ι.*ᵣ-homo r i
53+
; *ₗ-homo = λ r p → I.ι.*ₗ-homo r _
54+
; *ᵣ-homo = λ r p → I.ι.*ᵣ-homo r _
5555
}
5656
}
5757
; injective = λ p → I.ι.injective p

‎src/Algebra/NormalSubgroup/Construct/Intersection.agda

Lines changed: 37 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -18,63 +18,71 @@ open import Function.Base
1818
open import Level
1919
open import Relation.Binary.Reasoning.Setoid setoid
2020

21+
record ICarrier {c₁ ℓ₁ c₂ ℓ₂} (N : NormalSubgroup c₁ ℓ₁) (M : NormalSubgroup c₂ ℓ₂) : Set (ℓ ⊔ c₁ ⊔ c₂) where
22+
constructor icarrier
23+
private
24+
module N = NormalSubgroup N
25+
module M = NormalSubgroup M
26+
field
27+
{a} : N.N.Carrier
28+
{b} : M.N.Carrier
29+
a≈b : N.ι a ≈ M.ι b
30+
2131
_∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → NormalSubgroup c₁ ℓ₁ → NormalSubgroup c₂ ℓ₂ → NormalSubgroup (ℓ ⊔ c₁ ⊔ c₂) ℓ₁
2232
N ∩ M = record
2333
{ N = record
24-
{ Carrier = Σ[ (a , b) ∈ N.N.Carrier × M.N.Carrier ] N.ι a ≈ M.ι b
25-
; _≈_ = N.N._≈_ on proj₁ on proj₁
26-
; _∙_ = λ ((xₙ , xₘ) , p) ((yₙ , yₘ) , q) → record
27-
{ fst = xₙ N.N.∙ yₙ , xₘ M.N.∙ yₘ
28-
; snd = begin
29-
N.ι (xₙ N.N.∙ yₙ) ≈⟨ N.ι.∙-homo xₙ yₙ ⟩
30-
N.ι xₙ ∙ N.ι yₙ ≈⟨ ∙-cong p q ⟩
31-
M.ι xₘ ∙ M.ι yₘ ≈⟨ M.ι.∙-homo xₘ yₘ ⟨
32-
M.ι (xₘ M.N.∙ yₘ) ∎
34+
{ Carrier = ICarrier N M
35+
; _≈_ = N.N._≈_ on ICarrier.a
36+
; _∙_ = λ p q → record
37+
{ a≈b = begin
38+
N.ι (_ N.N.∙ _) ≈⟨ N.ι.∙-homo _ _ ⟩
39+
N.ι _ ∙ N.ι _ ≈⟨ ∙-cong (ICarrier.a≈b p) (ICarrier.a≈b q) ⟩
40+
M.ι _ ∙ M.ι _ ≈⟨ M.ι.∙-homo _ _ ⟨
41+
M.ι (_ M.N.∙ _) ∎
3342
}
3443
; ε = record
35-
{ fst = N.N.ε , M.N.ε
36-
; snd = begin
44+
{ a≈b = begin
3745
N.ι N.N.ε ≈⟨ N.ι.ε-homo ⟩
3846
ε ≈⟨ M.ι.ε-homo ⟨
3947
M.ι M.N.ε ∎
4048
}
41-
; _⁻¹ = λ ((n , m) , p) → record
42-
{ fst = n N.N.⁻¹ , m M.N.⁻¹
43-
; snd = begin
44-
N.ι (n N.N.⁻¹) ≈⟨ N.ι.⁻¹-homo n ⟩
45-
N.ι n ⁻¹ ≈⟨ ⁻¹-cong p ⟩
46-
M.ι m ⁻¹ ≈⟨ M.ι.⁻¹-homo m ⟨
47-
M.ι (m M.N.⁻¹) ∎
49+
; _⁻¹ = λ p → record
50+
{ a≈b = begin
51+
N.ι (_ N.N.⁻¹) ≈⟨ N.ι.⁻¹-homo _ ⟩
52+
N.ι _ ⁻¹ ≈⟨ ⁻¹-cong (ICarrier.a≈b p) ⟩
53+
M.ι _ ⁻¹ ≈⟨ M.ι.⁻¹-homo _ ⟨
54+
M.ι (_ M.N.⁻¹) ∎
4855
}
4956
}
50-
; ι = λ ((n , _) , _) → N.ι n
57+
; ι = λ p → N.ι _
5158
; ι-monomorphism = record
5259
{ isGroupHomomorphism = record
5360
{ isMonoidHomomorphism = record
5461
{ isMagmaHomomorphism = record
5562
{ isRelHomomorphism = record
5663
{ cong = N.ι.⟦⟧-cong
5764
}
58-
; homo = λ ((x , _) , _) ((y , _) , _) → N.ι.∙-homo x y
65+
; homo = λ p q → N.ι.∙-homo _ _
5966
}
6067
; ε-homo = N.ι.ε-homo
6168
}
62-
; ⁻¹-homo = λ ((x , _) , _) → N.ι.⁻¹-homo x
69+
; ⁻¹-homo = λ p → N.ι.⁻¹-homo _
6370
}
6471
; injective = λ p → N.ι.injective p
6572
}
66-
; normal = λ ((n , m) , p) g → record
73+
; normal = λ p g → record
6774
{ fst = record
68-
{ fst = proj₁ (N.normal n g) , proj₁ (M.normal m g)
69-
; snd = begin
70-
N.ι (proj₁ (N.normal n g)) ≈⟨ proj₂ (N.normal n g) ⟨
71-
g ∙ N.ι n ∙ g ⁻¹ ≈⟨ ∙-congʳ (∙-cong refl p) ⟩
72-
g ∙ M.ι m ∙ g ⁻¹ ≈⟨ proj₂ (M.normal m g) ⟩
73-
M.ι (proj₁ (M.normal m g)) ∎
75+
{ a≈b = begin
76+
N.ι (proj₁ (N.normal _ g)) ≈⟨ proj₂ (N.normal _ g) ⟨
77+
g ∙ N.ι _ ∙ g ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (ICarrier.a≈b p)) ⟩
78+
g ∙ M.ι _ ∙ g ⁻¹ ≈⟨ proj₂ (M.normal _ g) ⟩
79+
M.ι (proj₁ (M.normal _ g)) ∎
7480
}
75-
; snd = proj₂ (N.normal n g)
81+
; snd = proj₂ (N.normal _ g)
7682
}
7783
}
7884
where
7985
module N = NormalSubgroup N
8086
module M = NormalSubgroup M
87+
88+

0 commit comments

Comments
 (0)