Add subgroups and submodules (#2852)

* Add subgroups and submodules

* Let Agda fill in a record for me

* Try different names for the underlying structure

* Bimodule rather than module

* style

Author: Taneb

CHANGELOG.md

@@ -79,6 +79,10 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Sub.Group` for the definition of subgroups.
+
+* `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.
+
 * `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
+
+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′ ℓ′
+
+  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/Bimodule.agda

@@ -0,0 +1,50 @@
+------------------------------------------------------------------------
+-- 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
+
+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
+  module S = Ring S
+  module M = Bimodule M
+
+open import Algebra.Construct.Sub.Group M.+ᴹ-group
+
+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 }