Add subgroups and submodules

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`.

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
+    domain : RawGroup c′ ℓ′
+
+  private
+    module H = RawGroup domain
+
+  field
+    ι : H.Carrier → G.Carrier
+    ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
+
+  module ι = IsGroupMonomorphism ι-monomorphism
+
+  isGroup : IsGroup H._≈_ H._∙_ H.ε H._⁻¹
+  isGroup = GroupMonomorphism.isGroup ι-monomorphism G.isGroup
+
+  group : Group _ _
+  group = record { isGroup = isGroup }
+
+  open Group group public hiding (isGroup)

src/Algebra/Module/Construct/Sub/Module.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- 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 }