From 6495ef2b0efc8e6fedc3bf8e41e23d9a282d4c5e Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 29 Oct 2025 19:41:54 +0100 Subject: [PATCH 1/5] Add subgroups and submodules --- CHANGELOG.md | 4 ++ src/Algebra/Construct/Sub/Group.agda | 40 ++++++++++++++++ src/Algebra/Module/Construct/Sub/Module.agda | 50 ++++++++++++++++++++ 3 files changed, 94 insertions(+) create mode 100644 src/Algebra/Construct/Sub/Group.agda create mode 100644 src/Algebra/Module/Construct/Sub/Module.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 6679049fd0..5aa7c7df30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,6 +79,10 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Sub.Group` for the definition of subgroups. + +* `Algebra.Module.Construct.Sub.Module` for the definition of submodules. + * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda new file mode 100644 index 0000000000..b8bcef0435 --- /dev/null +++ b/src/Algebra/Construct/Sub/Group.agda @@ -0,0 +1,40 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of subgroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; RawGroup) + +module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where + +private + module G = Group G + +open import Algebra.Structures using (IsGroup) +open import Algebra.Morphism.Structures using (IsGroupMonomorphism) +import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism +open import Level using (suc; _⊔_) + +record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + Sub : RawGroup c′ ℓ′ + + private + module Sub = RawGroup Sub + + field + ι : Sub.Carrier → G.Carrier + ι-monomorphism : IsGroupMonomorphism Sub G.rawGroup ι + + module ι = IsGroupMonomorphism ι-monomorphism + + isGroup : IsGroup Sub._≈_ Sub._∙_ Sub.ε Sub._⁻¹ + isGroup = GroupMonomorphism.isGroup ι-monomorphism G.isGroup + + group : Group _ _ + group = record { isGroup = isGroup } + + open Group group public hiding (isGroup) diff --git a/src/Algebra/Module/Construct/Sub/Module.agda b/src/Algebra/Module/Construct/Sub/Module.agda new file mode 100644 index 0000000000..8b2863b3e4 --- /dev/null +++ b/src/Algebra/Module/Construct/Sub/Module.agda @@ -0,0 +1,50 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of submodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (CommutativeRing) +open import Algebra.Module.Bundles using (Module; RawModule) + +module Algebra.Module.Construct.Sub.Module {c ℓ cm ℓm} {R : CommutativeRing c ℓ} (M : Module R cm ℓm) where + +private + module R = CommutativeRing R + module M = Module M + +open import Algebra.Construct.Sub.Group M.+ᴹ-group +open import Algebra.Module.Structures using (IsModule) +open import Algebra.Module.Morphism.Structures using (IsModuleMonomorphism) +import Algebra.Module.Morphism.ModuleMonomorphism as ModuleMonomorphism +open import Level using (suc; _⊔_) + +record Submodule cm′ ℓm′ : Set (c ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where + field + Sub : RawModule R.Carrier cm′ ℓm′ + + private + module Sub = RawModule Sub + + field + ι : Sub.Carrierᴹ → M.Carrierᴹ + ι-monomorphism : IsModuleMonomorphism Sub M.rawModule ι + + module ι = IsModuleMonomorphism ι-monomorphism + + isModule : IsModule R Sub._≈ᴹ_ Sub._+ᴹ_ Sub.0ᴹ Sub.-ᴹ_ Sub._*ₗ_ Sub._*ᵣ_ + isModule = ModuleMonomorphism.isModule ι-monomorphism R.isCommutativeRing M.isModule + + ⟨module⟩ : Module R _ _ + ⟨module⟩ = record { isModule = isModule } + + open Module ⟨module⟩ public hiding (isModule) + + subgroup : Subgroup cm′ ℓm′ + subgroup = record + { Sub = Sub.+ᴹ-rawGroup + ; ι = ι + ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism + } From ce383b17e3cca574926b187e04f6a9010c345049 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 30 Oct 2025 09:18:50 +0100 Subject: [PATCH 2/5] Let Agda fill in a record for me --- src/Algebra/Module/Construct/Sub/Module.agda | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Algebra/Module/Construct/Sub/Module.agda b/src/Algebra/Module/Construct/Sub/Module.agda index 8b2863b3e4..3ab239d628 100644 --- a/src/Algebra/Module/Construct/Sub/Module.agda +++ b/src/Algebra/Module/Construct/Sub/Module.agda @@ -43,8 +43,4 @@ record Submodule cm′ ℓm′ : Set (c ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm open Module ⟨module⟩ public hiding (isModule) subgroup : Subgroup cm′ ℓm′ - subgroup = record - { Sub = Sub.+ᴹ-rawGroup - ; ι = ι - ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism - } + subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism } From 07ccc28eba2f72deb294e29f9b6ddff73cea174d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 30 Oct 2025 10:41:54 +0100 Subject: [PATCH 3/5] Try different names for the underlying structure --- src/Algebra/Construct/Sub/Group.agda | 10 +++++----- src/Algebra/Module/Construct/Sub/Module.agda | 10 +++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda index b8bcef0435..31d3673887 100644 --- a/src/Algebra/Construct/Sub/Group.agda +++ b/src/Algebra/Construct/Sub/Group.agda @@ -20,18 +20,18 @@ open import Level using (suc; _⊔_) record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field - Sub : RawGroup c′ ℓ′ + domain : RawGroup c′ ℓ′ private - module Sub = RawGroup Sub + module H = RawGroup domain field - ι : Sub.Carrier → G.Carrier - ι-monomorphism : IsGroupMonomorphism Sub G.rawGroup ι + ι : H.Carrier → G.Carrier + ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι module ι = IsGroupMonomorphism ι-monomorphism - isGroup : IsGroup Sub._≈_ Sub._∙_ Sub.ε Sub._⁻¹ + isGroup : IsGroup H._≈_ H._∙_ H.ε H._⁻¹ isGroup = GroupMonomorphism.isGroup ι-monomorphism G.isGroup group : Group _ _ diff --git a/src/Algebra/Module/Construct/Sub/Module.agda b/src/Algebra/Module/Construct/Sub/Module.agda index 3ab239d628..0e68a6ba0c 100644 --- a/src/Algebra/Module/Construct/Sub/Module.agda +++ b/src/Algebra/Module/Construct/Sub/Module.agda @@ -23,18 +23,18 @@ open import Level using (suc; _⊔_) record Submodule cm′ ℓm′ : Set (c ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where field - Sub : RawModule R.Carrier cm′ ℓm′ + domain : RawModule R.Carrier cm′ ℓm′ private - module Sub = RawModule Sub + module N = RawModule domain field - ι : Sub.Carrierᴹ → M.Carrierᴹ - ι-monomorphism : IsModuleMonomorphism Sub M.rawModule ι + ι : N.Carrierᴹ → M.Carrierᴹ + ι-monomorphism : IsModuleMonomorphism domain M.rawModule ι module ι = IsModuleMonomorphism ι-monomorphism - isModule : IsModule R Sub._≈ᴹ_ Sub._+ᴹ_ Sub.0ᴹ Sub.-ᴹ_ Sub._*ₗ_ Sub._*ᵣ_ + isModule : IsModule R N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ isModule = ModuleMonomorphism.isModule ι-monomorphism R.isCommutativeRing M.isModule ⟨module⟩ : Module R _ _ From 99c90aef47de119e743058d97c11900770ede751 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 31 Oct 2025 09:56:55 +0100 Subject: [PATCH 4/5] Bimodule rather than module --- CHANGELOG.md | 2 +- .../Module/Construct/Sub/Bimodule.agda | 47 +++++++++++++++++++ src/Algebra/Module/Construct/Sub/Module.agda | 46 ------------------ 3 files changed, 48 insertions(+), 47 deletions(-) create mode 100644 src/Algebra/Module/Construct/Sub/Bimodule.agda delete mode 100644 src/Algebra/Module/Construct/Sub/Module.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 5aa7c7df30..4e2b1a7c72 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -81,7 +81,7 @@ New modules * `Algebra.Construct.Sub.Group` for the definition of subgroups. -* `Algebra.Module.Construct.Sub.Module` for the definition of submodules. +* `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules. * `Algebra.Properties.BooleanRing`. diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda new file mode 100644 index 0000000000..c0f334ea6b --- /dev/null +++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda @@ -0,0 +1,47 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of submodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Ring) +open import Algebra.Module.Bundles using (Bimodule; RawBimodule) + +module Algebra.Module.Construct.Sub.Bimodule {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) where + +private + module R = Ring R + module S = Ring S + module M = Bimodule M + +open import Algebra.Construct.Sub.Group M.+ᴹ-group +open import Algebra.Module.Structures using (IsBimodule) +open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism) +import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism +open import Level using (suc; _⊔_) + +record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where + field + domain : RawBimodule R.Carrier S.Carrier cm′ ℓm′ + + private + module N = RawBimodule domain + + field + ι : N.Carrierᴹ → M.Carrierᴹ + ι-monomorphism : IsBimoduleMonomorphism domain M.rawBimodule ι + + module ι = IsBimoduleMonomorphism ι-monomorphism + + isBimodule : IsBimodule R S N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + isBimodule = BimoduleMonomorphism.isBimodule ι-monomorphism R.isRing S.isRing M.isBimodule + + bimodule : Bimodule R S _ _ + bimodule = record { isBimodule = isBimodule } + + open Bimodule bimodule public hiding (isBimodule) + + subgroup : Subgroup cm′ ℓm′ + subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism } diff --git a/src/Algebra/Module/Construct/Sub/Module.agda b/src/Algebra/Module/Construct/Sub/Module.agda deleted file mode 100644 index 0e68a6ba0c..0000000000 --- a/src/Algebra/Module/Construct/Sub/Module.agda +++ /dev/null @@ -1,46 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Definition of submodules ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Algebra.Bundles using (CommutativeRing) -open import Algebra.Module.Bundles using (Module; RawModule) - -module Algebra.Module.Construct.Sub.Module {c ℓ cm ℓm} {R : CommutativeRing c ℓ} (M : Module R cm ℓm) where - -private - module R = CommutativeRing R - module M = Module M - -open import Algebra.Construct.Sub.Group M.+ᴹ-group -open import Algebra.Module.Structures using (IsModule) -open import Algebra.Module.Morphism.Structures using (IsModuleMonomorphism) -import Algebra.Module.Morphism.ModuleMonomorphism as ModuleMonomorphism -open import Level using (suc; _⊔_) - -record Submodule cm′ ℓm′ : Set (c ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where - field - domain : RawModule R.Carrier cm′ ℓm′ - - private - module N = RawModule domain - - field - ι : N.Carrierᴹ → M.Carrierᴹ - ι-monomorphism : IsModuleMonomorphism domain M.rawModule ι - - module ι = IsModuleMonomorphism ι-monomorphism - - isModule : IsModule R N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ - isModule = ModuleMonomorphism.isModule ι-monomorphism R.isCommutativeRing M.isModule - - ⟨module⟩ : Module R _ _ - ⟨module⟩ = record { isModule = isModule } - - open Module ⟨module⟩ public hiding (isModule) - - subgroup : Subgroup cm′ ℓm′ - subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism } From 3c7bbdd463ba5a29e58eed4ec5f58959a8646dba Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:50:50 +0100 Subject: [PATCH 5/5] style --- src/Algebra/Construct/Sub/Group.agda | 6 +++--- src/Algebra/Module/Construct/Sub/Bimodule.agda | 13 ++++++++----- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda index 31d3673887..b51309d542 100644 --- a/src/Algebra/Construct/Sub/Group.agda +++ b/src/Algebra/Construct/Sub/Group.agda @@ -10,14 +10,14 @@ open import Algebra.Bundles using (Group; RawGroup) module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where -private - module G = Group G - open import Algebra.Structures using (IsGroup) open import Algebra.Morphism.Structures using (IsGroupMonomorphism) import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism open import Level using (suc; _⊔_) +private + module G = Group G + record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field domain : RawGroup c′ ℓ′ diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda index c0f334ea6b..c193be5d11 100644 --- a/src/Algebra/Module/Construct/Sub/Bimodule.agda +++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda @@ -9,7 +9,14 @@ open import Algebra.Bundles using (Ring) open import Algebra.Module.Bundles using (Bimodule; RawBimodule) -module Algebra.Module.Construct.Sub.Bimodule {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) where +module Algebra.Module.Construct.Sub.Bimodule + {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) + where + +open import Algebra.Module.Structures using (IsBimodule) +open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism) +import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism +open import Level using (suc; _⊔_) private module R = Ring R @@ -17,10 +24,6 @@ private module M = Bimodule M open import Algebra.Construct.Sub.Group M.+ᴹ-group -open import Algebra.Module.Structures using (IsBimodule) -open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism) -import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism -open import Level using (suc; _⊔_) record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where field