diff --git a/CHANGELOG.md b/CHANGELOG.md index 6679049fd0..963fea24cd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,6 +79,18 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Centre.Group` for the definition of the centre of a group. + +* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups. + +* `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups. + +* `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups. + +* `Algebra.Construct.Sub.Ring.Ideal` for the definition of ideals of a ring. + +* `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules. + * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda new file mode 100644 index 0000000000..0dc87797ee --- /dev/null +++ b/src/Algebra/Construct/Centre/Group.agda @@ -0,0 +1,87 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of Z[ G ] the centre of a Group G +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (AbelianGroup; Group; RawGroup; RawMonoid) + +module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where + +import Algebra.Construct.Centre.Monoid as Centre +open import Algebra.Core using (Op₁) +open import Algebra.Morphism.Structures using (IsGroupMonomorphism) +open import Function.Base using (id; _∘_; const; _$_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup) +open import Algebra.Properties.Group G using (∙-cancelʳ) + +private + module G = Group G + module Z = Centre G.monoid + + +------------------------------------------------------------------------ +-- Definition + +open Z public + using (Center; ι; central; ∙-comm) + hiding (module ι) + +_⁻¹ : Op₁ Center +g ⁻¹ = record + { ι = ι g G.⁻¹ + ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin + (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ + ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ central g k ⟨ + ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ + (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ + G.ε G.∙ k ≈⟨ central Z.ε k ⟩ + k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ + k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ + (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ + } where open ≈-Reasoning G.setoid + +domain : RawGroup _ _ +domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } + +ι-isGroupMonomorphism : IsGroupMonomorphism domain _ _ +ι-isGroupMonomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = Z.ι.isMonoidHomomorphism + ; ⁻¹-homo = λ _ → G.refl + } + ; injective = id + } + + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsGroupMonomorphism ι-isGroupMonomorphism + +normalSubgroup : NormalSubgroup _ _ +normalSubgroup = record + { subgroup = record { ι-monomorphism = ι-isGroupMonomorphism } + ; isNormal = record + { conjugate = const + ; normal = central + } + } + +open NormalSubgroup normalSubgroup public + using (group) + +abelianGroup : AbelianGroup _ _ +abelianGroup = record + { isAbelianGroup = record + { isGroup = isGroup + ; comm = ∙-comm + } + } where open Group group using (isGroup) + +Z[_] = abelianGroup + diff --git a/src/Algebra/Construct/Centre/Magma.agda b/src/Algebra/Construct/Centre/Magma.agda new file mode 100644 index 0000000000..23692665e1 --- /dev/null +++ b/src/Algebra/Construct/Centre/Magma.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Magma +-- +-- NB this doesn't make sense a priori, because in the absence of +-- associativity, it's not possible to define even a Magma operation +-- on the Center type defined below, as underlying Carrier. +-- +-- Yet a Magma *is* sufficient to define such a type, and thus can be +-- inherited up through the whole `Algebra.Construct.Centre.X` hierarchy. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Magma) + +module Algebra.Construct.Centre.Magma {c ℓ} (G : Magma c ℓ) where + +open import Algebra.Core using (Op₂) +open import Algebra.Definitions using (Central) +open import Function.Base using (id; _on_) +open import Level using (_⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Morphism.Structures + using (IsRelHomomorphism; IsRelMonomorphism) + +private + module G = Magma G + + +------------------------------------------------------------------------ +-- Definition + +record Center : Set (c ⊔ ℓ) where + field + ι : G.Carrier + central : Central G._≈_ G._∙_ ι + +open Center public + +_≈_ : Rel Center _ +_≈_ = G._≈_ on ι + +ι-isRelHomomorphism : IsRelHomomorphism _≈_ G._≈_ ι +ι-isRelHomomorphism = record { cong = id } + +ι-isRelMonomorphism : IsRelMonomorphism _≈_ _ _ +ι-isRelMonomorphism = record + { isHomomorphism = ι-isRelHomomorphism + ; injective = id + } + +module ι = IsRelMonomorphism ι-isRelMonomorphism + +∙-comm : ∀ g h → ι g G.∙ ι h G.≈ ι h G.∙ ι g +∙-comm g h = central g (ι h) diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda new file mode 100644 index 0000000000..06bf399dc3 --- /dev/null +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -0,0 +1,68 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of Z[ G ] the centre of a Monoid G +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (CommutativeMonoid; Monoid; RawMonoid; RawMagma) + +module Algebra.Construct.Centre.Monoid {c ℓ} (G : Monoid c ℓ) where + +open import Algebra.Morphism.Structures using (IsMonoidMonomorphism) +open import Function.Base using (id; _∘_) + +import Algebra.Construct.Centre.Semigroup as Centre +open import Algebra.Construct.Sub.Monoid G using (Submonoid) + +private + module G = Monoid G + module Z = Centre G.semigroup + + +------------------------------------------------------------------------ +-- Definition + +open Z public + using (Center; ι; central; ∙-comm) + hiding (module ι) + +ε : Center +ε = record + { ι = G.ε + ; central = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) + } + +domain : RawMonoid _ _ +domain = record { RawMagma Z.domain ; ε = ε } + +ι-isMonoidMonomorphism : IsMonoidMonomorphism domain _ _ +ι-isMonoidMonomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = Z.ι.isMagmaHomomorphism + ; ε-homo = G.refl + } + ; injective = id + } + +monoid : Monoid _ _ +monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism } + +commutativeMonoid : CommutativeMonoid _ _ +commutativeMonoid = record + { isCommutativeMonoid = record + { isMonoid = isMonoid + ; comm = ∙-comm + } + } where open Monoid monoid using (isMonoid) + + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism + +Z[_] = commutativeMonoid + diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda new file mode 100644 index 0000000000..fc86c4483b --- /dev/null +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -0,0 +1,78 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of Z[ G ] the centre of a Semigroup +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (CommutativeSemigroup; Semigroup; RawMagma) + +module Algebra.Construct.Centre.Semigroup {c ℓ} (G : Semigroup c ℓ) where + +import Algebra.Construct.Centre.Magma as Centre +open import Algebra.Core using (Op₂) +open import Algebra.Definitions using (Commutative) +open import Algebra.Morphism.Structures using (IsMagmaMonomorphism) +open import Function.Base using (id; _∘_; const; _$_; _on_) +open import Level using (_⊔_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +import Algebra.Construct.Sub.Semigroup G as Subsemigroup + +private + module G = Semigroup G + module Z = Centre G.magma + + +------------------------------------------------------------------------ +-- Definition + +open Z public + using (Center; ι; central; ∙-comm) + hiding (module ι) + +_∙_ : Op₂ Center +ι (g ∙ h) = ι g G.∙ ι h +central (g ∙ h) = λ k → begin + (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ + ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ + ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ + k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (ι g G.∙ ι h) ∎ + where open ≈-Reasoning G.setoid + +domain : RawMagma _ _ +domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } + +ι-isMagmaMonomorphism : IsMagmaMonomorphism domain _ _ +ι-isMagmaMonomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = Z.ι.isHomomorphism + ; homo = λ _ _ → G.refl + } + ; injective = id + } + +submagma : Subsemigroup.Submagma _ _ +submagma = record { ι-monomorphism = ι-isMagmaMonomorphism } + +semigroup : Semigroup _ _ +semigroup = Subsemigroup.semigroup submagma + +commutativeSemigroup : CommutativeSemigroup _ _ +commutativeSemigroup = record + { isCommutativeSemigroup = record + { isSemigroup = isSemigroup + ; comm = ∙-comm + } + } where open Semigroup semigroup using (isSemigroup) + + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism + +Z[_] = commutativeSemigroup diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda new file mode 100644 index 0000000000..c81cdf0952 --- /dev/null +++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda @@ -0,0 +1,35 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient of an Abelian group by a subgroup +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; AbelianGroup) +import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup + +module Algebra.Construct.Quotient.AbelianGroup + {c ℓ} (G : AbelianGroup c ℓ) + (open AbelianSubgroup G using (Subgroup; normalSubgroup)) + {c′ ℓ′} (N : Subgroup c′ ℓ′) + where + +private + module G = AbelianGroup G + +-- Re-export the quotient group + +open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public + +-- With its additional bundle + +quotientAbelianGroup : AbelianGroup c _ +quotientAbelianGroup = record + { isAbelianGroup = record + { isGroup = isGroup + ; comm = λ g h → ≈⇒≋ (G.comm g h) + } + } where open Group quotientGroup + +-- Public re-exports, as needed? diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda new file mode 100644 index 0000000000..9f018deb40 --- /dev/null +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -0,0 +1,126 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient of a Group by a NormalSubgroup +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) +open import Algebra.Construct.Sub.Group.Normal using (NormalSubgroup) + +module Algebra.Construct.Quotient.Group + {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where + +open import Algebra.Definitions using (Congruent₁; Congruent₂) +open import Algebra.Morphism.Structures + using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism) +open import Data.Product.Base using (_,_) +open import Function.Base using (_∘_) +open import Function.Definitions using (Surjective) +open import Level using (_⊔_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) + +private + open module G = Group G + +open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) +open import Algebra.Properties.Monoid monoid +open import Relation.Binary.Reasoning.Setoid setoid + +private + open module N = NormalSubgroup N + using (ι; module ι; conjugate; normal) + +infix 0 _by_ + +data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where + _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y + +≈⇒≋ : _≈_ ⇒ _≋_ +≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _) + +≋-refl : Reflexive _≋_ +≋-refl = ≈⇒≋ refl + +≋-sym : Symmetric _≋_ +≋-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) ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩ + x ∎ + +≋-trans : Transitive _≋_ +≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin + ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩ + (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩ + ι h ∙ y ≈⟨ ιh∙y≈z ⟩ + z ∎ + +≋-∙-cong : Congruent₂ _≋_ _∙_ +≋-∙-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) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩ + (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ + y ∙ v ∎ + where h′ = conjugate h x + +≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹ +≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin + ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩ + x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩ + x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨ + (ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩ + y ⁻¹ ∎ + where h = conjugate (g N.⁻¹) (x ⁻¹) + +quotientGroup : Group c (c ⊔ ℓ ⊔ c′) +quotientGroup = record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = record + { refl = ≋-refl + ; sym = ≋-sym + ; trans = ≋-trans + } + ; ∙-cong = ≋-∙-cong + } + ; assoc = λ x y z → ≈⇒≋ (assoc x y z) + } + ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ + } + ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ + ; ⁻¹-cong = ≋-⁻¹-cong + } + } + +_/_ : Group c (c ⊔ ℓ ⊔ c′) +_/_ = quotientGroup + +π : Group.Carrier G → Group.Carrier quotientGroup +π x = x -- because we do all the work in the relation + +π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π +π-isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = ≈⇒≋ + } + ; homo = λ _ _ → ≋-refl + } + +π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π +π-isMonoidHomomorphism = record + { isMagmaHomomorphism = π-isMagmaHomomorphism + ; ε-homo = ≋-refl + } + +π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π +π-isGroupHomomorphism = record + { isMonoidHomomorphism = π-isMonoidHomomorphism + ; ⁻¹-homo = λ _ → ≋-refl + } + +π-surjective : Surjective _≈_ _≋_ π +π-surjective g = g , ≈⇒≋ diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda new file mode 100644 index 0000000000..10ff1c8f34 --- /dev/null +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -0,0 +1,76 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient of a Ring by an Ideal +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (AbelianGroup; Ring; RawRing) +open import Algebra.Construct.Sub.Ring.Ideal using (Ideal) + +module Algebra.Construct.Quotient.Ring + {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) + where + +open import Algebra.Morphism.Structures using (IsRingHomomorphism) +open import Data.Product.Base using (_,_) +open import Function.Base using (_∘_) +open import Level using (_⊔_) + +import Algebra.Construct.Quotient.AbelianGroup as Quotient + +private + module R = Ring R + module I = Ideal I + module R/I = Quotient R.+-abelianGroup I.subgroup + + +open R/I public + using (_≋_; _by_; ≋-refl; ≈⇒≋ + ; quotientAbelianGroup + ; π; π-isMonoidHomomorphism; π-surjective + ) + +open import Algebra.Definitions _≋_ using (Congruent₂) + +≋-*-cong : Congruent₂ R._*_ +≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin + ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩ + ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩ + ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ 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 ∎ + where + open R using (_+_; _*_; +-congʳ ;+-cong; *-cong) + open import Algebra.Properties.Semiring R.semiring using (binomial-expansion) + open import Relation.Binary.Reasoning.Setoid R.setoid + open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_) + +quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′) +quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ } + +quotientRing : Ring c (c ⊔ ℓ ⊔ c′) +quotientRing = record + { isRing = record + { +-isAbelianGroup = isAbelianGroup + ; *-cong = ≋-*-cong + ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z) + ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ + ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z)) + } + } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup) + +π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π +π-isRingHomomorphism = record + { isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = π-isMonoidHomomorphism + ; *-homo = λ _ _ → ≋-refl + } + ; 1#-homo = ≋-refl + } + ; -‿homo = λ _ → ≋-refl + } + diff --git a/src/Algebra/Construct/Sub/AbelianGroup.agda b/src/Algebra/Construct/Sub/AbelianGroup.agda new file mode 100644 index 0000000000..be527587cd --- /dev/null +++ b/src/Algebra/Construct/Sub/AbelianGroup.agda @@ -0,0 +1,48 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Subgroups of Abelian groups: necessarily Normal +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (AbelianGroup) + +module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where + +open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup) + +private + module G = AbelianGroup G + +open import Algebra.Construct.Sub.Group.Normal G.group + using (IsNormal; NormalSubgroup) + +-- Re-export the notion of subgroup of the underlying Group + +open import Algebra.Construct.Sub.Group G.group public + using (Subgroup) + +-- Then, for any such Subgroup: +-- * it defines an AbelianGroup +-- * and is, in fact, Normal + +module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where + + open Subgroup subgroup public + using (ι; ι-monomorphism) + + abelianGroup : AbelianGroup c′ ℓ′ + abelianGroup = record + { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup } + + open AbelianGroup abelianGroup public + + isNormal : IsNormal subgroup + isNormal = record { normal = λ n → G.comm (ι n) } + + normalSubgroup : NormalSubgroup c′ ℓ′ + normalSubgroup = record { isNormal = isNormal } + + open NormalSubgroup normalSubgroup public + using (conjugate; normal) diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda new file mode 100644 index 0000000000..a43a2070de --- /dev/null +++ b/src/Algebra/Construct/Sub/Group.agda @@ -0,0 +1,31 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of subgroup via Group monomorphism +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; RawGroup) + +module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where + +open import Algebra.Morphism.Structures using (IsGroupMonomorphism) +open import Algebra.Morphism.GroupMonomorphism using (isGroup) +open import Level using (suc; _⊔_) + +private + module G = Group G + +record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + domain : RawGroup c′ ℓ′ + ι : _ → G.Carrier + ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι + + module ι = IsGroupMonomorphism ι-monomorphism + + group : Group _ _ + group = record { isGroup = isGroup ι-monomorphism G.isGroup } + + open Group group public diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda new file mode 100644 index 0000000000..653bdba37a --- /dev/null +++ b/src/Algebra/Construct/Sub/Group/Normal.agda @@ -0,0 +1,32 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of normal subgroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) + +module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ) where + +open import Algebra.Construct.Sub.Group G using (Subgroup) +open import Level using (suc; _⊔_) + +private + module G = Group G + +-- every element of the subgroup commutes in G +record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where + open Subgroup subgroup using (ι) + field + conjugate : ∀ n g → _ + normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n + +record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + subgroup : Subgroup c′ ℓ′ + isNormal : IsNormal subgroup + + open Subgroup subgroup public + open IsNormal isNormal public diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda new file mode 100644 index 0000000000..8e40d0d7e1 --- /dev/null +++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda @@ -0,0 +1,25 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ideals of a ring +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Ring) + +module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where + +open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule) +open import Algebra.Module.Construct.TensorUnit using (bimodule) +open import Level using (suc; _⊔_) + +------------------------------------------------------------------------ +-- Definition +-- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself + +record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + subbimodule : Subbimodule {R = R} bimodule c′ ℓ′ + + open Subbimodule subbimodule public diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index e42958da4d..d210052c9b 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -53,6 +53,9 @@ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) LeftIdentity : A → Op₂ A → Set _ LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x +Central : Op₂ A → A → Set _ +Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x) + RightIdentity : A → Op₂ A → Set _ RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda new file mode 100644 index 0000000000..19c778a4bf --- /dev/null +++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda @@ -0,0 +1,53 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of sub-bimodules +------------------------------------------------------------------------ + +{-# 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.Morphism.Structures using (IsBimoduleMonomorphism) +open import Algebra.Module.Morphism.BimoduleMonomorphism using (isBimodule) +open import Level using (suc; _⊔_) + +private + module R = Ring R + module S = Ring S + module M = Bimodule M + +open import Algebra.Construct.Sub.AbelianGroup M.+ᴹ-abelianGroup + as AbelianSubgroup + using (Subgroup) + +------------------------------------------------------------------------ +-- Definition + +record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where + field + domain : RawBimodule R.Carrier S.Carrier cm′ ℓm′ + ι : _ → M.Carrierᴹ + ι-monomorphism : IsBimoduleMonomorphism domain M.rawBimodule ι + + module ι = IsBimoduleMonomorphism ι-monomorphism + + bimodule : Bimodule R S _ _ + bimodule = record + { isBimodule = isBimodule ι-monomorphism R.isRing S.isRing M.isBimodule } + + open Bimodule bimodule public + +-- Additionally, have Abelian (hence: Normal) subgroups of M.+ᴹ-abelianGroup + + subgroup : Subgroup cm′ ℓm′ + subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism } + + isNormal = AbelianSubgroup.isNormal subgroup + + normalSubgroup = AbelianSubgroup.normalSubgroup subgroup