From 38f83d3d0316c825e734d1c31b0d17bfeabf6f11 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 4 Jun 2025 10:38:28 +0100 Subject: [PATCH 01/10] Add notion of quotient groups --- src/Algebra/Construct/Quotient/Group.agda | 140 ++++++++++++++++++ src/Algebra/NormalSubgroup.agda | 34 +++++ .../NormalSubgroup/Construct/Kernel.agda | 114 ++++++++++++++ 3 files changed, 288 insertions(+) create mode 100644 src/Algebra/Construct/Quotient/Group.agda create mode 100644 src/Algebra/NormalSubgroup.agda create mode 100644 src/Algebra/NormalSubgroup/Construct/Kernel.agda diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda new file mode 100644 index 0000000000..95a354aa36 --- /dev/null +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -0,0 +1,140 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient groups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) +open import Algebra.NormalSubgroup using (NormalSubgroup) + +module Algebra.Construct.Quotient.Group {c ℓ c′ ℓ′} (G : Group c ℓ) (N : NormalSubgroup G c′ ℓ′) where + +open Group G + +import Algebra.Definitions as AlgDefs +open import Algebra.Morphism.Structures +open import Algebra.Properties.Group G +open import Algebra.Structures using (IsGroup) +open import Data.Product.Base +open import Level using (_⊔_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Reasoning.Setoid setoid + +open NormalSubgroup N + +infix 0 _by_ + +data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where + _by_ : ∀ g → x // y ≈ ι g → x ≋ y + +≋-refl : Reflexive _≋_ +≋-refl {x} = N.ε by begin + x // x ≈⟨ inverseʳ x ⟩ + ε ≈⟨ ι.ε-homo ⟨ + ι N.ε ∎ + +≋-sym : Symmetric _≋_ +≋-sym {x} {y} (g by x//y≈ιg) = g N.⁻¹ by begin + y // x ≈⟨ ⁻¹-anti-homo-// x y ⟨ + (x // y) ⁻¹ ≈⟨ ⁻¹-cong x//y≈ιg ⟩ + ι g ⁻¹ ≈⟨ ι.⁻¹-homo g ⟨ + ι (g N.⁻¹) ∎ + + +≋-trans : Transitive _≋_ +≋-trans {x} {y} {z} (g by x//y≈ιg) (h by y//z≈ιh) = g N.∙ h by begin + x // z ≈⟨ ∙-congʳ (identityʳ x) ⟨ + x ∙ ε // z ≈⟨ ∙-congʳ (∙-congˡ (inverseˡ y)) ⟨ + x ∙ (y \\ y) // z ≈⟨ ∙-congʳ (assoc x (y ⁻¹) y) ⟨ + (x // y) ∙ y // z ≈⟨ assoc (x // y) y (z ⁻¹) ⟩ + (x // y) ∙ (y // z) ≈⟨ ∙-cong x//y≈ιg y//z≈ιh ⟩ + ι g ∙ ι h ≈⟨ ι.∙-homo g h ⟨ + ι (g N.∙ h) ∎ + +≋-isEquivalence : IsEquivalence _≋_ +≋-isEquivalence = record + { refl = ≋-refl + ; sym = ≋-sym + ; trans = ≋-trans + } + +≈⇒≋ : _≈_ ⇒ _≋_ +≈⇒≋ {x} {y} x≈y = N.ε by begin + x // y ≈⟨ x≈y⇒x∙y⁻¹≈ε x≈y ⟩ + ε ≈⟨ ι.ε-homo ⟨ + ι N.ε ∎ + +open AlgDefs _≋_ + +≋-∙-cong : Congruent₂ _∙_ +≋-∙-cong {x} {y} {u} {v} (g by x//y≈ιg) (h by u//v≈ιh) = g N.∙ normal h y .proj₁ by begin + x ∙ u // y ∙ v ≈⟨ ∙-congˡ (⁻¹-anti-homo-∙ y v) ⟩ + x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹) ≈⟨ assoc (x ∙ u) (v ⁻¹) (y ⁻¹) ⟨ + (x ∙ u // v) // y ≈⟨ ∙-congʳ (assoc x u (v ⁻¹)) ⟩ + x ∙ (u // v) // y ≈⟨ ∙-congʳ (∙-congˡ u//v≈ιh) ⟩ + x ∙ ι h // y ≈⟨ ∙-congʳ (∙-congˡ (identityˡ (ι h))) ⟨ + x ∙ (ε ∙ ι h) // y ≈⟨ ∙-congʳ (∙-congˡ (∙-congʳ (inverseˡ y))) ⟨ + x ∙ ((y \\ y) ∙ ι h) // y ≈⟨ ∙-congʳ (∙-congˡ (assoc (y ⁻¹) y (ι h))) ⟩ + x ∙ (y \\ y ∙ ι h) // y ≈⟨ ∙-congʳ (assoc x (y ⁻¹) (y ∙ ι h)) ⟨ + (x // y) ∙ (y ∙ ι h) // y ≈⟨ assoc (x // y) (y ∙ ι h) (y ⁻¹) ⟩ + (x // y) ∙ (y ∙ ι h // y) ≈⟨ ∙-cong x//y≈ιg (proj₂ (normal h y)) ⟩ + ι g ∙ ι (normal h y .proj₁) ≈⟨ ι.∙-homo g (normal h y .proj₁) ⟨ + ι (g N.∙ normal h y .proj₁) ∎ + +≋-⁻¹-cong : Congruent₁ _⁻¹ +≋-⁻¹-cong {x} {y} (g by x//y≈ιg) = normal (g N.⁻¹) (y ⁻¹) .proj₁ by begin + x ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (identityˡ (x ⁻¹)) ⟨ + (ε ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congʳ (inverseʳ (y ⁻¹))) ⟨ + ((y ⁻¹ ∙ y ⁻¹ ⁻¹) ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (assoc (y ⁻¹) ((y ⁻¹) ⁻¹) (x ⁻¹)) ⟩ + y ⁻¹ ∙ (y ⁻¹ ⁻¹ ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-anti-homo-∙ x (y ⁻¹))) ⟨ + y ⁻¹ ∙ (x ∙ y ⁻¹) ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-cong x//y≈ιg)) ⟩ + y ⁻¹ ∙ ι g ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (ι.⁻¹-homo g)) ⟨ + y ⁻¹ ∙ ι (g N.⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ proj₂ (normal (g N.⁻¹) (y ⁻¹)) ⟩ + ι (normal (g N.⁻¹) (y ⁻¹) .proj₁) ∎ + +quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹ +quotientIsGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≋-isEquivalence + ; ∙-cong = ≋-∙-cong + } + ; assoc = λ x y z → ≈⇒≋ (assoc x y z) + } + ; identity = record + { fst = λ x → ≈⇒≋ (identityˡ x) + ; snd = λ x → ≈⇒≋ (identityʳ x) + } + } + ; inverse = record + { fst = λ x → ≈⇒≋ (inverseˡ x) + ; snd = λ x → ≈⇒≋ (inverseʳ x) + } + ; ⁻¹-cong = ≋-⁻¹-cong + } + +quotientGroup : Group c (c ⊔ ℓ ⊔ c′) +quotientGroup = record { isGroup = quotientIsGroup } + +η : Group.Carrier G → Group.Carrier quotientGroup +η x = x -- because we do all the work in the relation + +η-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) η +η-isHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = ≈⇒≋ + } + ; homo = λ _ _ → ≋-refl + } + ; ε-homo = ≋-refl + } + ; ⁻¹-homo = λ _ → ≋-refl + } + diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda new file mode 100644 index 0000000000..b1ab8ac93d --- /dev/null +++ b/src/Algebra/NormalSubgroup.agda @@ -0,0 +1,34 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of normal subgroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; RawGroup) + +module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where + +open Group G + +open import Algebra.Structures using (IsGroup) +open import Algebra.Morphism.Structures +import Algebra.Morphism.GroupMonomorphism as GM +open import Data.Product.Base +open import Level using (suc; _⊔_) + +record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + -- N is a subgroup of G + N : RawGroup c′ ℓ′ + ι : RawGroup.Carrier N → Carrier + ι-monomorphism : IsGroupMonomorphism N rawGroup ι + -- every element of N commutes in G + normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′ + + module N = RawGroup N + module ι = IsGroupMonomorphism ι-monomorphism + + N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹ + N-isGroup = GM.isGroup ι-monomorphism isGroup diff --git a/src/Algebra/NormalSubgroup/Construct/Kernel.agda b/src/Algebra/NormalSubgroup/Construct/Kernel.agda new file mode 100644 index 0000000000..c2a0ca5c11 --- /dev/null +++ b/src/Algebra/NormalSubgroup/Construct/Kernel.agda @@ -0,0 +1,114 @@ +------------------------------------------------------------------------ +-- The kernel of a group homomorphism is a normal subgroup +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles +open import Algebra.Morphism.Structures + +module Algebra.NormalSubgroup.Construct.Kernel + {c ℓ c′ ℓ′} + {G : Group c ℓ} + {H : Group c′ ℓ′} + (ρ : Group.Carrier G → Group.Carrier H) + (homomorphism : IsGroupHomomorphism (Group.rawGroup G) (Group.rawGroup H) ρ) + where + +open import Algebra.NormalSubgroup +open import Algebra.Properties.Group +open import Data.Product.Base +open import Function.Base +open import Level +open import Relation.Binary.Reasoning.MultiSetoid + +private + module G = Group G + module H = Group H + module ρ = IsGroupHomomorphism homomorphism + +record Kernel : Set (c ⊔ ℓ′) where + field + element : G.Carrier + inKernel : ρ element H.≈ H.ε + +_∙ₖ_ : Kernel → Kernel → Kernel +x ∙ₖ y = record + { element = X.element G.∙ Y.element + ; inKernel = begin⟨ H.setoid ⟩ + ρ (X.element G.∙ Y.element) ≈⟨ ρ.homo X.element Y.element ⟩ + ρ X.element H.∙ ρ Y.element ≈⟨ H.∙-cong X.inKernel Y.inKernel ⟩ + H.ε H.∙ H.ε ≈⟨ H.identityˡ H.ε ⟩ + H.ε ∎ + } + where + module X = Kernel x + module Y = Kernel y + +εₖ : Kernel +εₖ = record + { element = G.ε + ; inKernel = ρ.ε-homo + } + +_⁻¹ₖ : Kernel → Kernel +x ⁻¹ₖ = record + { element = X.element G.⁻¹ + ; inKernel = begin⟨ H.setoid ⟩ + ρ (X.element G.⁻¹) ≈⟨ ρ.⁻¹-homo X.element ⟩ + ρ X.element H.⁻¹ ≈⟨ H.⁻¹-cong X.inKernel ⟩ + H.ε H.⁻¹ ≈⟨ ε⁻¹≈ε H ⟩ + H.ε ∎ + } + where + module X = Kernel x + +Kernel-rawGroup : RawGroup (c ⊔ ℓ′) ℓ +Kernel-rawGroup = record + { Carrier = Kernel + ; _≈_ = G._≈_ on Kernel.element + ; _∙_ = _∙ₖ_ + ; ε = εₖ + ; _⁻¹ = _⁻¹ₖ + } + +element-isGroupMonomorphism : IsGroupMonomorphism Kernel-rawGroup G.rawGroup Kernel.element +element-isGroupMonomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = λ p → p + } + ; homo = λ x y → G.refl + } + ; ε-homo = G.refl + } + ; ⁻¹-homo = λ x → G.refl + } + ; injective = λ p → p + } + +kernelNormalSubgroup : NormalSubgroup G (c ⊔ ℓ′) ℓ +kernelNormalSubgroup = record + { N = Kernel-rawGroup + ; ι = Kernel.element + ; ι-monomorphism = element-isGroupMonomorphism + ; normal = λ n g → let module N = Kernel n in record + { fst = record + { element = g G.∙ N.element G.∙ g G.⁻¹ + ; inKernel = begin⟨ H.setoid ⟩ + ρ (g G.∙ N.element G.∙ g G.⁻¹) ≈⟨ ρ.homo (g G.∙ N.element) (g G.⁻¹) ⟩ + ρ (g G.∙ N.element) H.∙ ρ (g G.⁻¹) ≈⟨ H.∙-congʳ (ρ.homo g N.element) ⟩ + ρ g H.∙ ρ N.element H.∙ ρ (g G.⁻¹) ≈⟨ H.∙-congʳ (H.∙-congˡ N.inKernel) ⟩ + ρ g H.∙ H.ε H.∙ ρ (g G.⁻¹) ≈⟨ H.∙-congʳ (H.identityʳ (ρ g)) ⟩ + ρ g H.∙ ρ (g G.⁻¹) ≈⟨ ρ.homo g (g G.⁻¹) ⟨ + ρ (g G.∙ g G.⁻¹) ≈⟨ ρ.⟦⟧-cong (G.inverseʳ g) ⟩ + ρ G.ε ≈⟨ ρ.ε-homo ⟩ + H.ε ∎ + } + ; snd = G.refl + } + } From 69b9aee6663591789ae2699fe819ae5ab5c8cbc5 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 7 Jun 2025 15:19:54 +0200 Subject: [PATCH 02/10] Quotient rings --- src/Algebra/Construct/Quotient/Ring.agda | 57 ++++++++++++++++++ src/Algebra/Ideal.agda | 47 +++++++++++++++ src/Algebra/Ideal/Construct/Kernel.agda | 77 ++++++++++++++++++++++++ 3 files changed, 181 insertions(+) create mode 100644 src/Algebra/Construct/Quotient/Ring.agda create mode 100644 src/Algebra/Ideal.agda create mode 100644 src/Algebra/Ideal/Construct/Kernel.agda diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda new file mode 100644 index 0000000000..706558b67c --- /dev/null +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient rings +------------------------------------------------------------------------ + +open import Algebra.Bundles using (Ring) +open import Algebra.Ideal using (Ideal) + +module Algebra.Construct.Quotient.Ring {c ℓ c′ ℓ′} (R : Ring c ℓ) (I : Ideal R c′ ℓ′) where + +open Ring R +open Ideal I + +open import Algebra.Construct.Quotient.Group +-group normalSubgroup + public + using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup) + renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong) + +open import Algebra.Definitions _≋_ +open import Algebra.Properties.Ring R +open import Algebra.Structures +open import Level +open import Relation.Binary.Reasoning.Setoid setoid + +≋-*-cong : Congruent₂ _*_ +≋-*-cong {x} {y} {u} {v} (j by x-y≈ιj) (k by u-v≈ιk) = j I.*ᵣ u I.+ᴹ y I.*ₗ k by begin + x * u - y * v ≈⟨ +-congʳ (+-identityʳ (x * u)) ⟨ + x * u + 0# - y * v ≈⟨ +-congʳ (+-congˡ (-‿inverseˡ (y * u))) ⟨ + x * u + (- (y * u) + y * u) - y * v ≈⟨ +-congʳ (+-assoc (x * u) (- (y * u)) (y * u)) ⟨ + ((x * u - y * u) + y * u) - y * v ≈⟨ +-assoc (x * u - y * u) (y * u) (- (y * v)) ⟩ + (x * u - y * u) + (y * u - y * v) ≈⟨ +-cong ([y-z]x≈yx-zx u x y) (x[y-z]≈xy-xz y u v) ⟨ + (x - y) * u + y * (u - v) ≈⟨ +-cong (*-congʳ x-y≈ιj) (*-congˡ u-v≈ιk) ⟩ + ι j * u + y * ι k ≈⟨ +-cong (ι.*ᵣ-homo u j) (ι.*ₗ-homo y k) ⟨ + ι (j I.*ᵣ u) + ι (y I.*ₗ k) ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨ + ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k) ∎ + +quotientIsRing : IsRing _≋_ _+_ _*_ (-_) 0# 1# +quotientIsRing = record + { +-isAbelianGroup = record + { isGroup = quotientIsGroup + ; comm = λ x y → ≈⇒≋ (+-comm x y) + } + ; *-cong = ≋-*-cong + ; *-assoc = λ x y z → ≈⇒≋ (*-assoc x y z) + ; *-identity = record + { fst = λ x → ≈⇒≋ (*-identityˡ x) + ; snd = λ x → ≈⇒≋ (*-identityʳ x) + } + ; distrib = record + { fst = λ x y z → ≈⇒≋ (distribˡ x y z) + ; snd = λ x y z → ≈⇒≋ (distribʳ x y z) + } + } + +quotientRing : Ring c (c ⊔ ℓ ⊔ c′) +quotientRing = record { isRing = quotientIsRing } diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda new file mode 100644 index 0000000000..43be876a45 --- /dev/null +++ b/src/Algebra/Ideal.agda @@ -0,0 +1,47 @@ +------------------------------------------------------------------------ +-- Ideals of a ring +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.Ideal {c ℓ} (R : Ring c ℓ) where + +open Ring R + +open import Algebra.Module.Bundles.Raw +import Algebra.Module.Construct.TensorUnit as TU +open import Algebra.Module.Morphism.Structures +open import Algebra.NormalSubgroup (+-group) +open import Data.Product.Base +open import Level +open import Relation.Binary.Reasoning.Setoid setoid + +record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + I : RawModule Carrier c′ ℓ′ + ι : RawModule.Carrierᴹ I → Carrier + ι-monomorphism : IsModuleMonomorphism I (TU.rawModule {R = rawRing}) ι + + module I = RawModule I + module ι = IsModuleMonomorphism ι-monomorphism + + normalSubgroup : NormalSubgroup c′ ℓ′ + normalSubgroup = record + { N = I.+ᴹ-rawGroup + ; ι = ι + ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism + ; normal = λ n g → record + { fst = n + ; snd = begin + g + ι n - g ≈⟨ +-assoc g (ι n) (- g) ⟩ + g + (ι n - g) ≈⟨ +-congˡ (+-comm (ι n) (- g)) ⟩ + g + (- g + ι n) ≈⟨ +-assoc g (- g) (ι n) ⟨ + g - g + ι n ≈⟨ +-congʳ (-‿inverseʳ g) ⟩ + 0# + ι n ≈⟨ +-identityˡ (ι n) ⟩ + ι n ∎ + } + } diff --git a/src/Algebra/Ideal/Construct/Kernel.agda b/src/Algebra/Ideal/Construct/Kernel.agda new file mode 100644 index 0000000000..2c5fdbfe0d --- /dev/null +++ b/src/Algebra/Ideal/Construct/Kernel.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --safe --without-K #-} + +open import Algebra.Bundles +open import Algebra.Morphism.Structures + +module Algebra.Ideal.Construct.Kernel + {c ℓ c′ ℓ′} + {R : Ring c ℓ} + {S : Ring c′ ℓ′} + (ρ : Ring.Carrier R → Ring.Carrier S) + (homomorphism : IsRingHomomorphism (Ring.rawRing R) (Ring.rawRing S) ρ) + where + +private + module R = Ring R + module S = Ring S + module ρ = IsRingHomomorphism homomorphism + +open import Algebra.NormalSubgroup.Construct.Kernel {G = R.+-group} {H = S.+-group} ρ ρ.+-isGroupHomomorphism public + renaming (_∙ₖ_ to _+ₖ_; εₖ to 0#ₖ; _⁻¹ₖ to -ₖ_) + +open import Algebra.Ideal R +open import Algebra.Module.Bundles.Raw +open import Function.Base +open import Level +open import Relation.Binary.Reasoning.Setoid S.setoid + + +_*ₗₖ_ : R.Carrier → Kernel → Kernel +r *ₗₖ x = record + { element = r R.* X.element + ; inKernel = begin + ρ (r R.* X.element) ≈⟨ ρ.*-homo r X.element ⟩ + ρ r S.* ρ X.element ≈⟨ S.*-congˡ X.inKernel ⟩ + ρ r S.* S.0# ≈⟨ S.zeroʳ (ρ r) ⟩ + S.0# ∎ + } + where module X = Kernel x + +_*ᵣₖ_ : Kernel → R.Carrier → Kernel +x *ᵣₖ r = record + { element = X.element R.* r + ; inKernel = begin + ρ (X.element R.* r) ≈⟨ ρ.*-homo X.element r ⟩ + ρ X.element S.* ρ r ≈⟨ S.*-congʳ X.inKernel ⟩ + S.0# S.* ρ r ≈⟨ S.zeroˡ (ρ r) ⟩ + S.0# ∎ + } + where module X = Kernel x + +Kernel-rawModule : RawModule R.Carrier (c ⊔ ℓ′) ℓ +Kernel-rawModule = record + { Carrierᴹ = Kernel + ; _≈ᴹ_ = R._≈_ on Kernel.element + ; _+ᴹ_ = _+ₖ_ + ; _*ₗ_ = _*ₗₖ_ + ; _*ᵣ_ = _*ᵣₖ_ + ; 0ᴹ = 0#ₖ + ; -ᴹ_ = -ₖ_ + } + where open RawGroup Kernel-rawGroup + +kernelIdeal : Ideal (c ⊔ ℓ′) ℓ +kernelIdeal = record + { I = Kernel-rawModule + ; ι = Kernel.element + ; ι-monomorphism = record + { isModuleHomomorphism = record + { isBimoduleHomomorphism = record + { +ᴹ-isGroupHomomorphism = IsGroupMonomorphism.isGroupHomomorphism element-isGroupMonomorphism + ; *ₗ-homo = λ _ _ → R.refl + ; *ᵣ-homo = λ _ _ → R.refl + } + } + ; injective = λ p → p + } + } From 83ab24815e1f21b9c5b49579f0919896fc034c35 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 7 Jun 2025 16:42:35 +0200 Subject: [PATCH 03/10] Intersection of ideals --- src/Algebra/Ideal/Construct/Intersection.agda | 64 +++++++++++++++ .../Construct/Intersection.agda | 80 +++++++++++++++++++ 2 files changed, 144 insertions(+) create mode 100644 src/Algebra/Ideal/Construct/Intersection.agda create mode 100644 src/Algebra/NormalSubgroup/Construct/Intersection.agda diff --git a/src/Algebra/Ideal/Construct/Intersection.agda b/src/Algebra/Ideal/Construct/Intersection.agda new file mode 100644 index 0000000000..3e75163b38 --- /dev/null +++ b/src/Algebra/Ideal/Construct/Intersection.agda @@ -0,0 +1,64 @@ +------------------------------------------------------------------------ +-- Intersection of ideals +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.Ideal.Construct.Intersection {c ℓ} (R : Ring c ℓ) where + +open Ring R + +open import Algebra.NormalSubgroup +import Algebra.NormalSubgroup.Construct.Intersection +-group as NS +open import Algebra.Ideal R +open import Data.Product.Base +open import Function.Base +open import Level +open import Relation.Binary.Reasoning.Setoid setoid + +_∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → Ideal c₁ ℓ₁ → Ideal c₂ ℓ₂ → Ideal (ℓ ⊔ c₁ ⊔ c₂) ℓ₁ +I ∩ J = record + { I = record + { Carrierᴹ = NSI.N.Carrier + ; _≈ᴹ_ = NSI.N._≈_ + ; _+ᴹ_ = NSI.N._∙_ + ; _*ₗ_ = λ r ((i , j) , p) → record + { fst = r I.I.*ₗ i , r J.I.*ₗ j + ; snd = begin + I.ι (r I.I.*ₗ i) ≈⟨ I.ι.*ₗ-homo r i ⟩ + r * I.ι i ≈⟨ *-congˡ p ⟩ + r * J.ι j ≈⟨ J.ι.*ₗ-homo r j ⟨ + J.ι (r J.I.*ₗ j) ∎ + } + ; _*ᵣ_ = λ ((i , j) , p) r → record + { fst = i I.I.*ᵣ r , j J.I.*ᵣ r + ; snd = begin + I.ι (i I.I.*ᵣ r) ≈⟨ I.ι.*ᵣ-homo r i ⟩ + I.ι i * r ≈⟨ *-congʳ p ⟩ + J.ι j * r ≈⟨ J.ι.*ᵣ-homo r j ⟨ + J.ι (j J.I.*ᵣ r) ∎ + } + ; 0ᴹ = NSI.N.ε + ; -ᴹ_ = NSI.N._⁻¹ + } + ; ι = NSI.ι + ; ι-monomorphism = record + { isModuleHomomorphism = record + { isBimoduleHomomorphism = record + { +ᴹ-isGroupHomomorphism = NSI.ι.isGroupHomomorphism + ; *ₗ-homo = λ r ((i , _) , _) → I.ι.*ₗ-homo r i + ; *ᵣ-homo = λ r ((i , _) , _) → I.ι.*ᵣ-homo r i + } + } + ; injective = λ p → I.ι.injective p + } + } + where + module I = Ideal I + module J = Ideal J + module NSI = NormalSubgroup (I.normalSubgroup NS.∩ J.normalSubgroup) + diff --git a/src/Algebra/NormalSubgroup/Construct/Intersection.agda b/src/Algebra/NormalSubgroup/Construct/Intersection.agda new file mode 100644 index 0000000000..dab696335d --- /dev/null +++ b/src/Algebra/NormalSubgroup/Construct/Intersection.agda @@ -0,0 +1,80 @@ +------------------------------------------------------------------------ +-- Intersection of normal subgroups +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.NormalSubgroup.Construct.Intersection {c ℓ} (G : Group c ℓ) where + +open Group G + +open import Algebra.NormalSubgroup G +open import Data.Product.Base +open import Function.Base +open import Level +open import Relation.Binary.Reasoning.Setoid setoid + +_∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → NormalSubgroup c₁ ℓ₁ → NormalSubgroup c₂ ℓ₂ → NormalSubgroup (ℓ ⊔ c₁ ⊔ c₂) ℓ₁ +N ∩ M = record + { N = record + { Carrier = Σ[ (a , b) ∈ N.N.Carrier × M.N.Carrier ] N.ι a ≈ M.ι b + ; _≈_ = N.N._≈_ on proj₁ on proj₁ + ; _∙_ = λ ((xₙ , xₘ) , p) ((yₙ , yₘ) , q) → record + { fst = xₙ N.N.∙ yₙ , xₘ M.N.∙ yₘ + ; snd = begin + N.ι (xₙ N.N.∙ yₙ) ≈⟨ N.ι.∙-homo xₙ yₙ ⟩ + N.ι xₙ ∙ N.ι yₙ ≈⟨ ∙-cong p q ⟩ + M.ι xₘ ∙ M.ι yₘ ≈⟨ M.ι.∙-homo xₘ yₘ ⟨ + M.ι (xₘ M.N.∙ yₘ) ∎ + } + ; ε = record + { fst = N.N.ε , M.N.ε + ; snd = begin + N.ι N.N.ε ≈⟨ N.ι.ε-homo ⟩ + ε ≈⟨ M.ι.ε-homo ⟨ + M.ι M.N.ε ∎ + } + ; _⁻¹ = λ ((n , m) , p) → record + { fst = n N.N.⁻¹ , m M.N.⁻¹ + ; snd = begin + N.ι (n N.N.⁻¹) ≈⟨ N.ι.⁻¹-homo n ⟩ + N.ι n ⁻¹ ≈⟨ ⁻¹-cong p ⟩ + M.ι m ⁻¹ ≈⟨ M.ι.⁻¹-homo m ⟨ + M.ι (m M.N.⁻¹) ∎ + } + } + ; ι = λ ((n , _) , _) → N.ι n + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = N.ι.⟦⟧-cong + } + ; homo = λ ((x , _) , _) ((y , _) , _) → N.ι.∙-homo x y + } + ; ε-homo = N.ι.ε-homo + } + ; ⁻¹-homo = λ ((x , _) , _) → N.ι.⁻¹-homo x + } + ; injective = λ p → N.ι.injective p + } + ; normal = λ ((n , m) , p) g → record + { fst = record + { fst = proj₁ (N.normal n g) , proj₁ (M.normal m g) + ; snd = begin + N.ι (proj₁ (N.normal n g)) ≈⟨ proj₂ (N.normal n g) ⟨ + g ∙ N.ι n ∙ g ⁻¹ ≈⟨ ∙-congʳ (∙-cong refl p) ⟩ + g ∙ M.ι m ∙ g ⁻¹ ≈⟨ proj₂ (M.normal m g) ⟩ + M.ι (proj₁ (M.normal m g)) ∎ + } + ; snd = proj₂ (N.normal n g) + } + } + where + module N = NormalSubgroup N + module M = NormalSubgroup M From a40ce81717a0e3d2238b1c71c1966dec5bafcfa3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 7 Jun 2025 16:49:41 +0200 Subject: [PATCH 04/10] Add coprimality of ideals --- src/Algebra/Ideal/Coprimality.agda | 36 ++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 src/Algebra/Ideal/Coprimality.agda diff --git a/src/Algebra/Ideal/Coprimality.agda b/src/Algebra/Ideal/Coprimality.agda new file mode 100644 index 0000000000..768a75806b --- /dev/null +++ b/src/Algebra/Ideal/Coprimality.agda @@ -0,0 +1,36 @@ +------------------------------------------------------------------------ +-- Coprimality of ideals +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.Ideal.Coprimality {c ℓ} (R : Ring c ℓ) where + +open Ring R hiding (sym) + +open import Algebra.Ideal R +open import Data.Product.Base +open import Level +open import Relation.Binary.Reasoning.Setoid setoid + +Coprime : ∀ {c₁ c₂ ℓ₁ ℓ₂} → Ideal c₁ ℓ₁ → Ideal c₂ ℓ₂ → Set (ℓ ⊔ c₁ ⊔ c₂) +Coprime I J = Σ[ (i , j) ∈ I.I.Carrierᴹ × J.I.Carrierᴹ ] I.ι i + J.ι j ≈ 1# + where + module I = Ideal I + module J = Ideal J + +sym : ∀ {c₁ c₂ ℓ₁ ℓ₂} {I : Ideal c₁ ℓ₁} {J : Ideal c₂ ℓ₂} → Coprime I J → Coprime J I +sym {I = I} {J = J} ((i , j) , p) = record + { fst = j , i + ; snd = begin + J.ι j + I.ι i ≈⟨ +-comm (J.ι j) (I.ι i) ⟩ + I.ι i + J.ι j ≈⟨ p ⟩ + 1# ∎ + } + where + module I = Ideal I + module J = Ideal J From 9a2b9fb0876d2da3cb0d7258bce02e489e08f928 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 7 Jun 2025 16:53:51 +0200 Subject: [PATCH 05/10] Add missing options pragma from ring quotient module --- src/Algebra/Construct/Quotient/Ring.agda | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda index 706558b67c..8ecea9ea89 100644 --- a/src/Algebra/Construct/Quotient/Ring.agda +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -4,6 +4,8 @@ -- Quotient rings ------------------------------------------------------------------------ +{-# OPTIONS --safe --cubical-compatible #-} + open import Algebra.Bundles using (Ring) open import Algebra.Ideal using (Ideal) From 8ec7935acec51db3ef3c0ecde25c5b82beed2bea Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 8 Jun 2025 11:10:37 +0200 Subject: [PATCH 06/10] Chinese remainder theorem --- src/Algebra/Construct/Quotient/Group.agda | 2 +- src/Algebra/Construct/Quotient/Ring.agda | 18 ++- .../Properties/ChineseRemainderTheorem.agda | 109 ++++++++++++++++++ src/Algebra/Ideal/Construct/Intersection.agda | 32 ++--- .../Construct/Intersection.agda | 66 ++++++----- 5 files changed, 177 insertions(+), 50 deletions(-) create mode 100644 src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 95a354aa36..28523e23f7 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -9,7 +9,7 @@ open import Algebra.Bundles using (Group) open import Algebra.NormalSubgroup using (NormalSubgroup) -module Algebra.Construct.Quotient.Group {c ℓ c′ ℓ′} (G : Group c ℓ) (N : NormalSubgroup G c′ ℓ′) where +module Algebra.Construct.Quotient.Group {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where open Group G diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda index 8ecea9ea89..88189ec7f7 100644 --- a/src/Algebra/Construct/Quotient/Ring.agda +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -6,16 +6,15 @@ {-# OPTIONS --safe --cubical-compatible #-} -open import Algebra.Bundles using (Ring) +open import Algebra.Bundles using (Ring; RawRing) open import Algebra.Ideal using (Ideal) -module Algebra.Construct.Quotient.Ring {c ℓ c′ ℓ′} (R : Ring c ℓ) (I : Ideal R c′ ℓ′) where +module Algebra.Construct.Quotient.Ring {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) where open Ring R open Ideal I -open import Algebra.Construct.Quotient.Group +-group normalSubgroup - public +open import Algebra.Construct.Quotient.Group +-group normalSubgroup public using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup) renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong) @@ -37,6 +36,17 @@ open import Relation.Binary.Reasoning.Setoid setoid ι (j I.*ᵣ u) + ι (y I.*ₗ k) ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨ ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k) ∎ +quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′) +quotientRawRing = record + { Carrier = Carrier + ; _≈_ = _≋_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } + quotientIsRing : IsRing _≋_ _+_ _*_ (-_) 0# 1# quotientIsRing = record { +-isAbelianGroup = record diff --git a/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda b/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda new file mode 100644 index 0000000000..5109eb4aea --- /dev/null +++ b/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda @@ -0,0 +1,109 @@ +------------------------------------------------------------------------ +-- The Chinese Remainder Theorem for arbitrary rings +-- +-- The Agda standard library +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.Construct.Quotient.Ring.Properties.ChineseRemainderTheorem {c ℓ} (R : Ring c ℓ) where + +open Ring R + +import Algebra.Construct.DirectProduct as DP +open import Algebra.Construct.Quotient.Ring as QR using (quotientRawRing) +open import Algebra.Ideal R +open import Algebra.Ideal.Coprimality R using (Coprime) +open import Algebra.Ideal.Construct.Intersection R +open import Algebra.Morphism.Structures +open import Algebra.Properties.Ring R +open import Data.Product.Base +open import Relation.Binary.Reasoning.Setoid setoid + +module _ + {c₁ c₂ ℓ₁ ℓ₂} + (I : Ideal c₁ ℓ₁) (J : Ideal c₂ ℓ₂) + where + + private + module I = Ideal I + module J = Ideal J + + CRT : Coprime I J → IsRingIsomorphism (quotientRawRing R (I ∩ J)) (DP.rawRing (quotientRawRing R I) (quotientRawRing R J)) λ x → x , x + CRT ((m , n) , m+n≈1) = record + { isRingMonomorphism = record + { isRingHomomorphism = record + { isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { 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)) } + } + ; homo = λ x y → R/I.≋-refl , R/J.≋-refl + } + ; ε-homo = R/I.≋-refl , R/J.≋-refl + } + ; *-homo = λ x y → R/I.≋-refl , R/J.≋-refl + } + ; 1#-homo = R/I.≋-refl , R/J.≋-refl + } + ; -‿homo = λ x → R/I.≋-refl , R/J.≋-refl + } + ; injective = λ {((i R/I.by p) , (j R/J.by q)) → record { a≈b = trans (sym p) q } R/I∩J.by p} + } + ; surjective = λ (a₁ , a₂) → a₁ * J.ι n + a₂ * I.ι m , λ {z} → λ + { (record {a = a; b = b; a≈b = a≈b} R/I∩J.by p) → record + { fst = a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m R/I.by begin + -- introduce a coprimality term + z - a₁ ≈⟨ +-congˡ (-‿cong (*-identityʳ a₁)) ⟨ + z - a₁ * 1# ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨ + -- lots and lots of rearrangement + z - a₁ * (I.ι m + J.ι n) ≈⟨ +-congˡ (-‿cong (distribˡ a₁ (I.ι m) (J.ι n))) ⟩ + z - (a₁ * I.ι m + a₁ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-comm (a₁ * I.ι m) (a₁ * J.ι n))) ⟩ + z - (a₁ * J.ι n + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₁ * J.ι n)))) ⟨ + z - (a₁ * J.ι n + 0# + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₂ * I.ι m))))) ⟨ + z - (a₁ * J.ι n + (a₂ * I.ι m - a₂ * I.ι m) + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc _ _ _))) ⟨ + z - (a₁ * J.ι n + a₂ * I.ι m - a₂ * I.ι m + a₁ * I.ι m) ≈⟨ +-congˡ (-‿cong (+-assoc _ _ _)) ⟩ + z - (a₁ * J.ι n + a₂ * I.ι m + (- (a₂ * I.ι m) + a₁ * I.ι m)) ≈⟨ +-congˡ (-‿+-comm _ _) ⟨ + z + (- (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m)) ≈⟨ +-assoc z _ _ ⟨ + z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m) ≈⟨ +-congˡ (-‿+-comm _ _) ⟨ + z - (a₁ * J.ι n + a₂ * I.ι m) + (- - (a₂ * I.ι m) - a₁ * I.ι m) ≈⟨ +-congˡ (+-congʳ (-‿involutive _)) ⟩ + z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ * I.ι m - a₁ * I.ι m) ≈⟨ +-congˡ ([y-z]x≈yx-zx _ _ _) ⟨ + -- substitute z-t + z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ - a₁) * I.ι m ≈⟨ +-congʳ p ⟩ + -- show we're in I + I.ι a + (a₂ - a₁) * I.ι m ≈⟨ +-congˡ (I.ι.*ₗ-homo (a₂ - a₁) m) ⟨ + I.ι a + I.ι ((a₂ - a₁) I.I.*ₗ m) ≈⟨ I.ι.+ᴹ-homo a _ ⟨ + I.ι (a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m) ∎ + ; snd = b J.I.+ᴹ (a₁ - a₂) J.I.*ₗ n R/J.by begin + -- introduce a coprimality term + z - a₂ ≈⟨ +-congˡ (-‿cong (*-identityʳ a₂)) ⟨ + z - a₂ * 1# ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨ + -- lots and lots of rearrangement + z - a₂ * (I.ι m + J.ι n) ≈⟨ +-congˡ (-‿cong (distribˡ a₂ (I.ι m) (J.ι n))) ⟩ + z - (a₂ * I.ι m + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₂ * I.ι m)))) ⟨ + z - (a₂ * I.ι m + 0# + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₁ * J.ι n))))) ⟨ + z - (a₂ * I.ι m + (a₁ * J.ι n - a₁ * J.ι n) + a₂ * J.ι n) ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc (a₂ * I.ι m) (a₁ * J.ι n) _))) ⟨ + 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)) _)) ⟩ + 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)) ⟨ + 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)) ⟨ + z - (a₂ * I.ι m + a₁ * J.ι n) - (- (a₁ * J.ι n) + a₂ * J.ι n) ≈⟨ +-cong (+-congˡ (-‿cong (+-comm _ _))) (-‿cong (+-congˡ (-‿involutive _))) ⟨ + z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₁ * J.ι n) - - (a₂ * J.ι n)) ≈⟨ +-congˡ (-‿cong (-‿+-comm (a₁ * J.ι n) (- (a₂ * J.ι n)))) ⟩ + z - (a₁ * J.ι n + a₂ * I.ι m) - - (a₁ * J.ι n - a₂ * J.ι n) ≈⟨ +-congˡ (-‿involutive (a₁ * J.ι n - a₂ * J.ι n)) ⟩ + z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ * J.ι n - a₂ * J.ι n) ≈⟨ +-congˡ ([y-z]x≈yx-zx (J.ι n) a₁ a₂) ⟨ + -- substitute z-t + z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ - a₂) * J.ι n ≈⟨ +-congʳ (trans p a≈b) ⟩ + -- show we're in I + J.ι b + (a₁ - a₂) * J.ι n ≈⟨ +-congˡ (J.ι.*ₗ-homo (a₁ - a₂) n) ⟨ + J.ι b + J.ι ((a₁ - a₂) J.I.*ₗ n) ≈⟨ J.ι.+ᴹ-homo b ((a₁ - a₂) J.I.*ₗ n) ⟨ + J.ι (b J.I.+ᴹ (a₁ - a₂) J.I.*ₗ n) ∎ + } + } + } + where + module R/I = QR R I + module R/J = QR R J + module R/I∩J = QR R (I ∩ J) diff --git a/src/Algebra/Ideal/Construct/Intersection.agda b/src/Algebra/Ideal/Construct/Intersection.agda index 3e75163b38..66f824f508 100644 --- a/src/Algebra/Ideal/Construct/Intersection.agda +++ b/src/Algebra/Ideal/Construct/Intersection.agda @@ -20,27 +20,27 @@ open import Function.Base open import Level open import Relation.Binary.Reasoning.Setoid setoid +open NS public using (ICarrier; icarrier) + _∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → Ideal c₁ ℓ₁ → Ideal c₂ ℓ₂ → Ideal (ℓ ⊔ c₁ ⊔ c₂) ℓ₁ I ∩ J = record { I = record { Carrierᴹ = NSI.N.Carrier ; _≈ᴹ_ = NSI.N._≈_ ; _+ᴹ_ = NSI.N._∙_ - ; _*ₗ_ = λ r ((i , j) , p) → record - { fst = r I.I.*ₗ i , r J.I.*ₗ j - ; snd = begin - I.ι (r I.I.*ₗ i) ≈⟨ I.ι.*ₗ-homo r i ⟩ - r * I.ι i ≈⟨ *-congˡ p ⟩ - r * J.ι j ≈⟨ J.ι.*ₗ-homo r j ⟨ - J.ι (r J.I.*ₗ j) ∎ + ; _*ₗ_ = λ r p → record + { a≈b = begin + I.ι (r I.I.*ₗ _) ≈⟨ I.ι.*ₗ-homo r _ ⟩ + r * I.ι _ ≈⟨ *-congˡ (NS.ICarrier.a≈b p) ⟩ + r * J.ι _ ≈⟨ J.ι.*ₗ-homo r _ ⟨ + J.ι (r J.I.*ₗ _) ∎ } - ; _*ᵣ_ = λ ((i , j) , p) r → record - { fst = i I.I.*ᵣ r , j J.I.*ᵣ r - ; snd = begin - I.ι (i I.I.*ᵣ r) ≈⟨ I.ι.*ᵣ-homo r i ⟩ - I.ι i * r ≈⟨ *-congʳ p ⟩ - J.ι j * r ≈⟨ J.ι.*ᵣ-homo r j ⟨ - J.ι (j J.I.*ᵣ r) ∎ + ; _*ᵣ_ = λ p r → record + { a≈b = begin + I.ι (_ I.I.*ᵣ r) ≈⟨ I.ι.*ᵣ-homo r _ ⟩ + I.ι _ * r ≈⟨ *-congʳ (NS.ICarrier.a≈b p) ⟩ + J.ι _ * r ≈⟨ J.ι.*ᵣ-homo r _ ⟨ + J.ι (_ J.I.*ᵣ r) ∎ } ; 0ᴹ = NSI.N.ε ; -ᴹ_ = NSI.N._⁻¹ @@ -50,8 +50,8 @@ I ∩ J = record { isModuleHomomorphism = record { isBimoduleHomomorphism = record { +ᴹ-isGroupHomomorphism = NSI.ι.isGroupHomomorphism - ; *ₗ-homo = λ r ((i , _) , _) → I.ι.*ₗ-homo r i - ; *ᵣ-homo = λ r ((i , _) , _) → I.ι.*ᵣ-homo r i + ; *ₗ-homo = λ r p → I.ι.*ₗ-homo r _ + ; *ᵣ-homo = λ r p → I.ι.*ᵣ-homo r _ } } ; injective = λ p → I.ι.injective p diff --git a/src/Algebra/NormalSubgroup/Construct/Intersection.agda b/src/Algebra/NormalSubgroup/Construct/Intersection.agda index dab696335d..bcc57b3359 100644 --- a/src/Algebra/NormalSubgroup/Construct/Intersection.agda +++ b/src/Algebra/NormalSubgroup/Construct/Intersection.agda @@ -18,36 +18,43 @@ open import Function.Base open import Level open import Relation.Binary.Reasoning.Setoid setoid +record ICarrier {c₁ ℓ₁ c₂ ℓ₂} (N : NormalSubgroup c₁ ℓ₁) (M : NormalSubgroup c₂ ℓ₂) : Set (ℓ ⊔ c₁ ⊔ c₂) where + constructor icarrier + private + module N = NormalSubgroup N + module M = NormalSubgroup M + field + {a} : N.N.Carrier + {b} : M.N.Carrier + a≈b : N.ι a ≈ M.ι b + _∩_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} → NormalSubgroup c₁ ℓ₁ → NormalSubgroup c₂ ℓ₂ → NormalSubgroup (ℓ ⊔ c₁ ⊔ c₂) ℓ₁ N ∩ M = record { N = record - { Carrier = Σ[ (a , b) ∈ N.N.Carrier × M.N.Carrier ] N.ι a ≈ M.ι b - ; _≈_ = N.N._≈_ on proj₁ on proj₁ - ; _∙_ = λ ((xₙ , xₘ) , p) ((yₙ , yₘ) , q) → record - { fst = xₙ N.N.∙ yₙ , xₘ M.N.∙ yₘ - ; snd = begin - N.ι (xₙ N.N.∙ yₙ) ≈⟨ N.ι.∙-homo xₙ yₙ ⟩ - N.ι xₙ ∙ N.ι yₙ ≈⟨ ∙-cong p q ⟩ - M.ι xₘ ∙ M.ι yₘ ≈⟨ M.ι.∙-homo xₘ yₘ ⟨ - M.ι (xₘ M.N.∙ yₘ) ∎ + { Carrier = ICarrier N M + ; _≈_ = N.N._≈_ on ICarrier.a + ; _∙_ = λ p q → record + { a≈b = begin + N.ι (_ N.N.∙ _) ≈⟨ N.ι.∙-homo _ _ ⟩ + N.ι _ ∙ N.ι _ ≈⟨ ∙-cong (ICarrier.a≈b p) (ICarrier.a≈b q) ⟩ + M.ι _ ∙ M.ι _ ≈⟨ M.ι.∙-homo _ _ ⟨ + M.ι (_ M.N.∙ _) ∎ } ; ε = record - { fst = N.N.ε , M.N.ε - ; snd = begin + { a≈b = begin N.ι N.N.ε ≈⟨ N.ι.ε-homo ⟩ ε ≈⟨ M.ι.ε-homo ⟨ M.ι M.N.ε ∎ } - ; _⁻¹ = λ ((n , m) , p) → record - { fst = n N.N.⁻¹ , m M.N.⁻¹ - ; snd = begin - N.ι (n N.N.⁻¹) ≈⟨ N.ι.⁻¹-homo n ⟩ - N.ι n ⁻¹ ≈⟨ ⁻¹-cong p ⟩ - M.ι m ⁻¹ ≈⟨ M.ι.⁻¹-homo m ⟨ - M.ι (m M.N.⁻¹) ∎ + ; _⁻¹ = λ p → record + { a≈b = begin + N.ι (_ N.N.⁻¹) ≈⟨ N.ι.⁻¹-homo _ ⟩ + N.ι _ ⁻¹ ≈⟨ ⁻¹-cong (ICarrier.a≈b p) ⟩ + M.ι _ ⁻¹ ≈⟨ M.ι.⁻¹-homo _ ⟨ + M.ι (_ M.N.⁻¹) ∎ } } - ; ι = λ ((n , _) , _) → N.ι n + ; ι = λ p → N.ι _ ; ι-monomorphism = record { isGroupHomomorphism = record { isMonoidHomomorphism = record @@ -55,26 +62,27 @@ N ∩ M = record { isRelHomomorphism = record { cong = N.ι.⟦⟧-cong } - ; homo = λ ((x , _) , _) ((y , _) , _) → N.ι.∙-homo x y + ; homo = λ p q → N.ι.∙-homo _ _ } ; ε-homo = N.ι.ε-homo } - ; ⁻¹-homo = λ ((x , _) , _) → N.ι.⁻¹-homo x + ; ⁻¹-homo = λ p → N.ι.⁻¹-homo _ } ; injective = λ p → N.ι.injective p } - ; normal = λ ((n , m) , p) g → record + ; normal = λ p g → record { fst = record - { fst = proj₁ (N.normal n g) , proj₁ (M.normal m g) - ; snd = begin - N.ι (proj₁ (N.normal n g)) ≈⟨ proj₂ (N.normal n g) ⟨ - g ∙ N.ι n ∙ g ⁻¹ ≈⟨ ∙-congʳ (∙-cong refl p) ⟩ - g ∙ M.ι m ∙ g ⁻¹ ≈⟨ proj₂ (M.normal m g) ⟩ - M.ι (proj₁ (M.normal m g)) ∎ + { a≈b = begin + N.ι (proj₁ (N.normal _ g)) ≈⟨ proj₂ (N.normal _ g) ⟨ + g ∙ N.ι _ ∙ g ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (ICarrier.a≈b p)) ⟩ + g ∙ M.ι _ ∙ g ⁻¹ ≈⟨ proj₂ (M.normal _ g) ⟩ + M.ι (proj₁ (M.normal _ g)) ∎ } - ; snd = proj₂ (N.normal n g) + ; snd = proj₂ (N.normal _ g) } } where module N = NormalSubgroup N module M = NormalSubgroup M + + From 5124b9612241bcdba677c0953e97d55a39f871bb Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 8 Jun 2025 11:14:56 +0200 Subject: [PATCH 07/10] Minor fixes --- .../Quotient/Ring/Properties/ChineseRemainderTheorem.agda | 4 ++-- src/Algebra/Ideal.agda | 4 ++-- src/Algebra/Ideal/Construct/Intersection.agda | 4 ++-- src/Algebra/Ideal/Construct/Kernel.agda | 8 +++++++- src/Algebra/Ideal/Coprimality.agda | 4 ++-- src/Algebra/NormalSubgroup/Construct/Intersection.agda | 6 ++---- src/Algebra/NormalSubgroup/Construct/Kernel.agda | 6 +++--- 7 files changed, 20 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda b/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda index 5109eb4aea..a5af7d33d4 100644 --- a/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda +++ b/src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- The Chinese Remainder Theorem for arbitrary rings --- -- The Agda standard library +-- +-- The Chinese Remainder Theorem for arbitrary rings ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda index 43be876a45..21f92e19e3 100644 --- a/src/Algebra/Ideal.agda +++ b/src/Algebra/Ideal.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- Ideals of a ring --- -- The Agda standard library +-- +-- Ideals of a ring ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Ideal/Construct/Intersection.agda b/src/Algebra/Ideal/Construct/Intersection.agda index 66f824f508..f3f3ab668a 100644 --- a/src/Algebra/Ideal/Construct/Intersection.agda +++ b/src/Algebra/Ideal/Construct/Intersection.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- Intersection of ideals --- -- The Agda standard library +-- +-- Intersection of ideals ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Ideal/Construct/Kernel.agda b/src/Algebra/Ideal/Construct/Kernel.agda index 2c5fdbfe0d..fe2514b228 100644 --- a/src/Algebra/Ideal/Construct/Kernel.agda +++ b/src/Algebra/Ideal/Construct/Kernel.agda @@ -1,4 +1,10 @@ -{-# OPTIONS --safe --without-K #-} +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The kernel of a ring homomorphism is an ideal +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} open import Algebra.Bundles open import Algebra.Morphism.Structures diff --git a/src/Algebra/Ideal/Coprimality.agda b/src/Algebra/Ideal/Coprimality.agda index 768a75806b..4f19e1ec55 100644 --- a/src/Algebra/Ideal/Coprimality.agda +++ b/src/Algebra/Ideal/Coprimality.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- Coprimality of ideals --- -- The Agda standard library +-- +-- Coprimality of ideals ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/NormalSubgroup/Construct/Intersection.agda b/src/Algebra/NormalSubgroup/Construct/Intersection.agda index bcc57b3359..70628e9ac4 100644 --- a/src/Algebra/NormalSubgroup/Construct/Intersection.agda +++ b/src/Algebra/NormalSubgroup/Construct/Intersection.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- Intersection of normal subgroups --- -- The Agda standard library +-- +-- Intersection of normal subgroups ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} @@ -84,5 +84,3 @@ N ∩ M = record where module N = NormalSubgroup N module M = NormalSubgroup M - - diff --git a/src/Algebra/NormalSubgroup/Construct/Kernel.agda b/src/Algebra/NormalSubgroup/Construct/Kernel.agda index c2a0ca5c11..88224be583 100644 --- a/src/Algebra/NormalSubgroup/Construct/Kernel.agda +++ b/src/Algebra/NormalSubgroup/Construct/Kernel.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ --- The kernel of a group homomorphism is a normal subgroup --- -- The Agda standard library +-- +-- The kernel of a group homomorphism is a normal subgroup ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} @@ -52,7 +52,7 @@ x ∙ₖ y = record { element = G.ε ; inKernel = ρ.ε-homo } - + _⁻¹ₖ : Kernel → Kernel x ⁻¹ₖ = record { element = X.element G.⁻¹ From 127f3f19bd46dcaaa98d0e5922936fa87c151eff Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 8 Jun 2025 11:30:55 +0200 Subject: [PATCH 08/10] Principal ideals --- src/Algebra/Ideal/Construct/Principal.agda | 57 ++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 src/Algebra/Ideal/Construct/Principal.agda diff --git a/src/Algebra/Ideal/Construct/Principal.agda b/src/Algebra/Ideal/Construct/Principal.agda new file mode 100644 index 0000000000..88777fe81c --- /dev/null +++ b/src/Algebra/Ideal/Construct/Principal.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ideals generated by a single element +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + +module Algebra.Ideal.Construct.Principal {c ℓ} (R : CommutativeRing c ℓ) where + +open CommutativeRing R + +open import Algebra.Ideal ring +open import Algebra.Properties.Ring ring +open import Function.Base +open import Relation.Binary.Reasoning.Setoid setoid + +⟨_⟩ : Carrier → Ideal c ℓ +⟨ a ⟩ = record + { I = record + { Carrierᴹ = Carrier + ; _≈ᴹ_ = _≈_ on _* a + ; _+ᴹ_ = _+_ + ; _*ₗ_ = _*_ + ; _*ᵣ_ = _*_ + ; 0ᴹ = 0# + ; -ᴹ_ = -_ + } + ; ι = _* a + ; ι-monomorphism = record + { isModuleHomomorphism = record + { isBimoduleHomomorphism = record + { +ᴹ-isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = λ p → p + } + ; homo = distribʳ a + } + ; ε-homo = zeroˡ a + } + ; ⁻¹-homo = λ x → sym (-‿distribˡ-* x a) + } + ; *ₗ-homo = λ r x → *-assoc r x a + ; *ᵣ-homo = λ r x → begin + x * r * a ≈⟨ *-assoc x r a ⟩ + x * (r * a) ≈⟨ *-congˡ (*-comm r a) ⟩ + x * (a * r) ≈⟨ *-assoc x a r ⟨ + x * a * r ∎ + } + } + ; injective = λ p → p + } + } From a4f934debed893158c676beb80ec4dcde6a40df3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 30 Jul 2025 23:46:59 +0200 Subject: [PATCH 09/10] WIP integer special case module --- src/Data/Integer/ModularArithmetic.agda | 96 +++++++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 src/Data/Integer/ModularArithmetic.agda diff --git a/src/Data/Integer/ModularArithmetic.agda b/src/Data/Integer/ModularArithmetic.agda new file mode 100644 index 0000000000..29f6a2253f --- /dev/null +++ b/src/Data/Integer/ModularArithmetic.agda @@ -0,0 +1,96 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Modular arithmetic on integers +------------------------------------------------------------------------ + +open import Data.Integer.Base + +module Data.Integer.ModularArithmetic (m : ℤ) where + +open import Algebra.Bundles +open import Data.Integer.DivMod +open import Data.Integer.Properties +open import Data.Fin.Base as Fin using (Fin) +import Data.Fin.Properties as Fin +open import Data.Nat.Base as ℕ using (zero; suc) +import Data.Nat.DivMod as ℕ +import Data.Nat.Properties as ℕ +open import Function.Base +open import Function.Bundles +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) +open import Relation.Nullary.Decidable + +open import Algebra.Ideal.Construct.Principal +-*-commutativeRing + +open import Algebra.Construct.Quotient.Ring +-*-ring ⟨ m ⟩ + + +ℤ/mℤ : Ring _ _ +ℤ/mℤ = quotientRing + +-- todo: +-- * chinese remainder theorem specialized to integers +-- * finiteness: for non-zero + +module _ .{{_ : NonZero m}} where + + from-% : ∀ {x y} → x % m ≡ y % m → x ≋ y + from-% {x} {y} x%m≡y%m = x / m - y / m by begin + x - y ≡⟨ ≡.cong₂ _-_ (a≡a%n+[a/n]*n x m) (a≡a%n+[a/n]*n y m) ⟩ + (+ (x % m) + (x / m) * m) - (+ (y % m) + (y / m) * m) ≡⟨ ≡.cong (λ z → (+ (x % m) + (x / m) * m) + z) (neg-distrib-+ (+ (y % m)) ((y / m) * m)) ⟩ + (+ (x % m) + (x / m) * m) + (- + (y % m) - (y / m) * m) ≡⟨ +-assoc (+ (x % m) + (x / m) * m) (- + (y % m)) (- ((y / m) * m)) ⟨ + ((+ (x % m) + (x / m) * m) - + (y % m)) - (y / m) * m ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) ((x / m) * m) (- + (y % m))) ⟩ + (+ (x % m) + ((x / m) * m - + (y % m))) - (y / m) * m ≡⟨ ≡.cong (λ z → (+ (x % m) + z) - (y / m) * m) (+-comm ((x / m) * m) (- + (y % m))) ⟩ + (+ (x % m) + (- + (y % m) + (x / m) * m)) - (y / m) * m ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) (- + (y % m)) ((x / m) * m)) ⟨ + ((+ (x % m) - + (y % m)) + (x / m) * m) - (y / m) * m ≡⟨ +-assoc (+ (x % m) - + (y % m)) ((x / m) * m) (- ((y / m) * m)) ⟩ + (+ (x % m) - + (y % m)) + ((x / m) * m - (y / m) * m) ≡⟨ ≡.cong₂ (λ a b → (+ a - + (y % m)) + ((x / m) * m + b)) x%m≡y%m (neg-distribˡ-* (y / m) m) ⟩ + (+ (y % m) - + (y % m)) + ((x / m) * m + - (y / m) * m) ≡⟨ ≡.cong₂ _+_ (+-inverseʳ (+ (y % m))) (≡.sym (*-distribʳ-+ m (x / m) (- (y / m)))) ⟩ + 0ℤ + (x / m - y / m) * m ≡⟨ +-identityˡ ((x / m - y / m) * m) ⟩ + (x / m - y / m) * m ∎ + where open ≡-Reasoning + + to-% : ∀ {x y} → x ≋ y → x % m ≡ y % m + to-% {x} {y} (k by x-y≡km) = {!!} + where + open ≡-Reasoning + lemma : x % m ⊖ y % m ≡ (k - (x / m) + (y / m)) * m + lemma = begin + x % m ⊖ y % m ≡⟨ m-n≡m⊖n (x % m) (y % m) ⟨ + + (x % m) - + (y % m) ≡⟨ {!!} ⟩ + (k - (x / m) + (y / m)) * m ∎ + + bound : ∣ x % m ⊖ y % m ∣ ℕ.< ∣ m ∣ + bound = {!!} + + _≋?′_ : Decidable _≋_ + x ≋?′ y = map′ from-% to-% (x % m ℕ.≟ y % m) + + ℤ/mℤ-finite : Equivalence (Ring.setoid ℤ/mℤ) (≡.setoid (Fin ∣ m ∣)) + ℤ/mℤ-finite = record + { to = λ n → Fin.fromℕ< (n%d Date: Wed, 29 Oct 2025 11:34:14 +0100 Subject: [PATCH 10/10] Try new definition for equivalences --- src/Algebra/Construct/Quotient/Group.agda | 86 +++++++++++------------ src/Algebra/Construct/Quotient/Ring.agda | 18 +++-- src/Algebra/Ideal.agda | 9 +-- src/Algebra/NormalSubgroup.agda | 2 +- src/Data/Integer/ModularArithmetic.agda | 16 +---- 5 files changed, 54 insertions(+), 77 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 28523e23f7..32f43d232d 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -29,31 +29,26 @@ open NormalSubgroup N infix 0 _by_ data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where - _by_ : ∀ g → x // y ≈ ι g → x ≋ y + _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y ≋-refl : Reflexive _≋_ -≋-refl {x} = N.ε by begin - x // x ≈⟨ inverseʳ x ⟩ - ε ≈⟨ ι.ε-homo ⟨ - ι N.ε ∎ +≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x) ≋-sym : Symmetric _≋_ -≋-sym {x} {y} (g by x//y≈ιg) = g N.⁻¹ by begin - y // x ≈⟨ ⁻¹-anti-homo-// x y ⟨ - (x // y) ⁻¹ ≈⟨ ⁻¹-cong x//y≈ιg ⟩ - ι g ⁻¹ ≈⟨ ι.⁻¹-homo g ⟨ - ι (g N.⁻¹) ∎ - +≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin + ι (g N.⁻¹) ∙ y ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩ + ι g ⁻¹ ∙ (ι g ∙ x) ≈⟨ assoc (ι g ⁻¹) (ι g) x ⟨ + (ι g ⁻¹ ∙ ι g) ∙ x ≈⟨ ∙-congʳ (inverseˡ (ι g)) ⟩ + ε ∙ x ≈⟨ identityˡ x ⟩ + x ∎ ≋-trans : Transitive _≋_ -≋-trans {x} {y} {z} (g by x//y≈ιg) (h by y//z≈ιh) = g N.∙ h by begin - x // z ≈⟨ ∙-congʳ (identityʳ x) ⟨ - x ∙ ε // z ≈⟨ ∙-congʳ (∙-congˡ (inverseˡ y)) ⟨ - x ∙ (y \\ y) // z ≈⟨ ∙-congʳ (assoc x (y ⁻¹) y) ⟨ - (x // y) ∙ y // z ≈⟨ assoc (x // y) y (z ⁻¹) ⟩ - (x // y) ∙ (y // z) ≈⟨ ∙-cong x//y≈ιg y//z≈ιh ⟩ - ι g ∙ ι h ≈⟨ ι.∙-homo g h ⟨ - ι (g N.∙ h) ∎ +≋-trans {x} {y} {z} (g by ιg∙x) (h by ιh∙y) = h N.∙ g by begin + ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩ + (ι h ∙ ι g) ∙ x ≈⟨ assoc (ι h) (ι g) x ⟩ + ι h ∙ (ι g ∙ x) ≈⟨ ∙-congˡ ιg∙x ⟩ + ι h ∙ y ≈⟨ ιh∙y ⟩ + z ∎ ≋-isEquivalence : IsEquivalence _≋_ ≋-isEquivalence = record @@ -63,38 +58,39 @@ data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where } ≈⇒≋ : _≈_ ⇒ _≋_ -≈⇒≋ {x} {y} x≈y = N.ε by begin - x // y ≈⟨ x≈y⇒x∙y⁻¹≈ε x≈y ⟩ - ε ≈⟨ ι.ε-homo ⟨ - ι N.ε ∎ +≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y) open AlgDefs _≋_ ≋-∙-cong : Congruent₂ _∙_ -≋-∙-cong {x} {y} {u} {v} (g by x//y≈ιg) (h by u//v≈ιh) = g N.∙ normal h y .proj₁ by begin - x ∙ u // y ∙ v ≈⟨ ∙-congˡ (⁻¹-anti-homo-∙ y v) ⟩ - x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹) ≈⟨ assoc (x ∙ u) (v ⁻¹) (y ⁻¹) ⟨ - (x ∙ u // v) // y ≈⟨ ∙-congʳ (assoc x u (v ⁻¹)) ⟩ - x ∙ (u // v) // y ≈⟨ ∙-congʳ (∙-congˡ u//v≈ιh) ⟩ - x ∙ ι h // y ≈⟨ ∙-congʳ (∙-congˡ (identityˡ (ι h))) ⟨ - x ∙ (ε ∙ ι h) // y ≈⟨ ∙-congʳ (∙-congˡ (∙-congʳ (inverseˡ y))) ⟨ - x ∙ ((y \\ y) ∙ ι h) // y ≈⟨ ∙-congʳ (∙-congˡ (assoc (y ⁻¹) y (ι h))) ⟩ - x ∙ (y \\ y ∙ ι h) // y ≈⟨ ∙-congʳ (assoc x (y ⁻¹) (y ∙ ι h)) ⟨ - (x // y) ∙ (y ∙ ι h) // y ≈⟨ assoc (x // y) (y ∙ ι h) (y ⁻¹) ⟩ - (x // y) ∙ (y ∙ ι h // y) ≈⟨ ∙-cong x//y≈ιg (proj₂ (normal h y)) ⟩ - ι g ∙ ι (normal h y .proj₁) ≈⟨ ι.∙-homo g (normal h y .proj₁) ⟨ - ι (g N.∙ normal h y .proj₁) ∎ +≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin + ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩ + (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ assoc (ι g) (ι h′) (x ∙ u) ⟩ + ι g ∙ (ι h′ ∙ (x ∙ u)) ≈⟨ ∙-congˡ (assoc (ι h′) x u) ⟨ + ι g ∙ ((ι h′ ∙ x) ∙ u) ≈⟨ ∙-congˡ (∙-congʳ x∙ιh≈ιh′∙x) ⟨ + ι g ∙ ((x ∙ ι h) ∙ u) ≈⟨ ∙-congˡ (assoc x (ι h) u) ⟩ + ι g ∙ (x ∙ (ι h ∙ u)) ≈⟨ assoc (ι g) x (ι h ∙ u) ⟨ + (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ + y ∙ v ∎ + where + h′ : N.Carrier + h′ = normal h x .proj₁ + x∙ιh≈ιh′∙x : x ∙ ι h ≈ ι h′ ∙ x + x∙ιh≈ιh′∙x = normal h x .proj₂ + ≋-⁻¹-cong : Congruent₁ _⁻¹ -≋-⁻¹-cong {x} {y} (g by x//y≈ιg) = normal (g N.⁻¹) (y ⁻¹) .proj₁ by begin - x ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (identityˡ (x ⁻¹)) ⟨ - (ε ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congʳ (inverseʳ (y ⁻¹))) ⟨ - ((y ⁻¹ ∙ y ⁻¹ ⁻¹) ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (assoc (y ⁻¹) ((y ⁻¹) ⁻¹) (x ⁻¹)) ⟩ - y ⁻¹ ∙ (y ⁻¹ ⁻¹ ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-anti-homo-∙ x (y ⁻¹))) ⟨ - y ⁻¹ ∙ (x ∙ y ⁻¹) ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-cong x//y≈ιg)) ⟩ - y ⁻¹ ∙ ι g ⁻¹ ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (∙-congˡ (ι.⁻¹-homo g)) ⟨ - y ⁻¹ ∙ ι (g N.⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ proj₂ (normal (g N.⁻¹) (y ⁻¹)) ⟩ - ι (normal (g N.⁻¹) (y ⁻¹) .proj₁) ∎ +≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = g′ by begin + ι g′ ∙ x ⁻¹ ≈⟨ x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ ⟨ + x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩ + x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨ + (ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩ + y ⁻¹ ∎ + where + g′ : N.Carrier + g′ = normal (g N.⁻¹) (x ⁻¹) .proj₁ + x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ : x ⁻¹ ∙ ι (g N.⁻¹) ≈ ι g′ ∙ x ⁻¹ + x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ = normal (g N.⁻¹) (x ⁻¹) .proj₂ quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹ quotientIsGroup = record diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda index 88189ec7f7..286872fabf 100644 --- a/src/Algebra/Construct/Quotient/Ring.agda +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -19,22 +19,20 @@ open import Algebra.Construct.Quotient.Group +-group normalSubgroup public renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong) open import Algebra.Definitions _≋_ +open import Algebra.Properties.Semiring semiring open import Algebra.Properties.Ring R open import Algebra.Structures open import Level open import Relation.Binary.Reasoning.Setoid setoid ≋-*-cong : Congruent₂ _*_ -≋-*-cong {x} {y} {u} {v} (j by x-y≈ιj) (k by u-v≈ιk) = j I.*ᵣ u I.+ᴹ y I.*ₗ k by begin - x * u - y * v ≈⟨ +-congʳ (+-identityʳ (x * u)) ⟨ - x * u + 0# - y * v ≈⟨ +-congʳ (+-congˡ (-‿inverseˡ (y * u))) ⟨ - x * u + (- (y * u) + y * u) - y * v ≈⟨ +-congʳ (+-assoc (x * u) (- (y * u)) (y * u)) ⟨ - ((x * u - y * u) + y * u) - y * v ≈⟨ +-assoc (x * u - y * u) (y * u) (- (y * v)) ⟩ - (x * u - y * u) + (y * u - y * v) ≈⟨ +-cong ([y-z]x≈yx-zx u x y) (x[y-z]≈xy-xz y u v) ⟨ - (x - y) * u + y * (u - v) ≈⟨ +-cong (*-congʳ x-y≈ιj) (*-congˡ u-v≈ιk) ⟩ - ι j * u + y * ι k ≈⟨ +-cong (ι.*ᵣ-homo u j) (ι.*ₗ-homo y k) ⟨ - ι (j I.*ᵣ u) + ι (y I.*ₗ k) ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨ - ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k) ∎ +≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k by begin + ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k) + x * u ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) (x I.*ₗ k)) ⟩ + ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) + ι (x I.*ₗ k) + x * u ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k) (j I.*ᵣ u))) ⟩ + ι (ι j I.*ₗ k) + ι (j I.*ᵣ u) + ι (x I.*ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩ + ι j * ι k + ι j * u + x * ι k + x * u ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨ + (ι j + x) * (ι k + u) ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩ + y * v ∎ quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′) quotientRawRing = record diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda index 21f92e19e3..dc636b6597 100644 --- a/src/Algebra/Ideal.agda +++ b/src/Algebra/Ideal.agda @@ -36,12 +36,7 @@ record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism ; normal = λ n g → record { fst = n - ; snd = begin - g + ι n - g ≈⟨ +-assoc g (ι n) (- g) ⟩ - g + (ι n - g) ≈⟨ +-congˡ (+-comm (ι n) (- g)) ⟩ - g + (- g + ι n) ≈⟨ +-assoc g (- g) (ι n) ⟨ - g - g + ι n ≈⟨ +-congʳ (-‿inverseʳ g) ⟩ - 0# + ι n ≈⟨ +-identityˡ (ι n) ⟩ - ι n ∎ + -- this ends up a lot simpler now + ; snd = +-comm g (ι n) } } diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index b1ab8ac93d..78710f2300 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -25,7 +25,7 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh ι : RawGroup.Carrier N → Carrier ι-monomorphism : IsGroupMonomorphism N rawGroup ι -- every element of N commutes in G - normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′ + normal : ∀ n g → ∃[ n′ ] g ∙ ι n ≈ ι n′ ∙ g module N = RawGroup N module ι = IsGroupMonomorphism ι-monomorphism diff --git a/src/Data/Integer/ModularArithmetic.agda b/src/Data/Integer/ModularArithmetic.agda index 29f6a2253f..6c945e4f0a 100644 --- a/src/Data/Integer/ModularArithmetic.agda +++ b/src/Data/Integer/ModularArithmetic.agda @@ -38,17 +38,8 @@ module _ .{{_ : NonZero m}} where from-% : ∀ {x y} → x % m ≡ y % m → x ≋ y from-% {x} {y} x%m≡y%m = x / m - y / m by begin - x - y ≡⟨ ≡.cong₂ _-_ (a≡a%n+[a/n]*n x m) (a≡a%n+[a/n]*n y m) ⟩ - (+ (x % m) + (x / m) * m) - (+ (y % m) + (y / m) * m) ≡⟨ ≡.cong (λ z → (+ (x % m) + (x / m) * m) + z) (neg-distrib-+ (+ (y % m)) ((y / m) * m)) ⟩ - (+ (x % m) + (x / m) * m) + (- + (y % m) - (y / m) * m) ≡⟨ +-assoc (+ (x % m) + (x / m) * m) (- + (y % m)) (- ((y / m) * m)) ⟨ - ((+ (x % m) + (x / m) * m) - + (y % m)) - (y / m) * m ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) ((x / m) * m) (- + (y % m))) ⟩ - (+ (x % m) + ((x / m) * m - + (y % m))) - (y / m) * m ≡⟨ ≡.cong (λ z → (+ (x % m) + z) - (y / m) * m) (+-comm ((x / m) * m) (- + (y % m))) ⟩ - (+ (x % m) + (- + (y % m) + (x / m) * m)) - (y / m) * m ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) (- + (y % m)) ((x / m) * m)) ⟨ - ((+ (x % m) - + (y % m)) + (x / m) * m) - (y / m) * m ≡⟨ +-assoc (+ (x % m) - + (y % m)) ((x / m) * m) (- ((y / m) * m)) ⟩ - (+ (x % m) - + (y % m)) + ((x / m) * m - (y / m) * m) ≡⟨ ≡.cong₂ (λ a b → (+ a - + (y % m)) + ((x / m) * m + b)) x%m≡y%m (neg-distribˡ-* (y / m) m) ⟩ - (+ (y % m) - + (y % m)) + ((x / m) * m + - (y / m) * m) ≡⟨ ≡.cong₂ _+_ (+-inverseʳ (+ (y % m))) (≡.sym (*-distribʳ-+ m (x / m) (- (y / m)))) ⟩ - 0ℤ + (x / m - y / m) * m ≡⟨ +-identityˡ ((x / m - y / m) * m) ⟩ - (x / m - y / m) * m ∎ + (x / m - y / m) * m + x ≡⟨ {!!} ⟩ + y ∎ where open ≡-Reasoning to-% : ∀ {x y} → x ≋ y → x % m ≡ y % m @@ -91,6 +82,3 @@ _≋?_ : Decidable _≋_ _≋?_ with ℕ.nonZero? ∣ m ∣ ... | yes p = _≋?′_ {{p}} ... | no ¬p = {!!} - - -