Contents Previous Next

• Groups and family 2
  • Magma
  • Semigroup
  • Monoid
  • Commutative Monoid
  • Group
  • Abelian Group

Groups and family 2

Here we define the objects based on the conditions defined in the previous section. It might be helpful here to think of Data fields as various common datatypes as used in computer sciences, and the objects as the structure defined on operations of that datatype.

We are bound to write this code in a new file as we are using a different module without the pre-supplied _==_ and A : Set a.

module Algebra.groups2 where

open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)

open import Types.relations
open import Types.equality
open import Algebra.groups

We recall operations again here:

★_ : ∀ {a} → Set a → Set a
★ A = A → A → A

♠_ : ∀ {a} → Set a → Set a
♠ A = A → A

Magma

record Magma a ℓ : Set (lsuc (a ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _==_
  field
    Data      : Set a
    _==_      : Rel Data ℓ
    _∙_       : ★ Data
    isMagma   : IsMagma _==_ _∙_

  open IsMagma isMagma public

Semigroup

record Semigroup c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _==_
  field
    Data        : Set c
    _==_        : Rel Data ℓ
    _∙_         : ★ Data
    isSemigroup : IsSemigroup _==_ _∙_

  open IsSemigroup isSemigroup public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Monoid

record Monoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _==_
  field
    Data     : Set c
    _==_      : Rel Data ℓ
    _∙_      : ★ Data
    ε        : Data
    isMonoid : IsMonoid _==_ _∙_ ε

  open IsMonoid isMonoid public

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Commutative Monoid

record CommutativeMonoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _==_
  field
    Data                : Set c
    _==_                 : Rel Data ℓ
    _∙_                 : ★ Data
    ε                   : Data
    isCommutativeMonoid : IsCommutativeMonoid _==_ _∙_ ε

  open IsCommutativeMonoid isCommutativeMonoid public

  monoid : Monoid c ℓ
  monoid = record { isMonoid = isMonoid }

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Group

record Group c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _==_
  field
    Data    : Set c
    _==_    : Rel Data ℓ
    _∙_     : ★ Data
    ε       : Data
    _⁻¹     : ♠ Data
    isGroup : IsGroup _==_ _∙_ ε _⁻¹

  open IsGroup isGroup public

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Abelian Group

open import Algebra.groups using (IsAbelianGroup)

record AbelianGroup c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _==_
  field
    Data           : Set c
    _==_            : Rel Data ℓ
    _∙_            : ★ Data
    ε              : Data
    _⁻¹            : ♠ Data
    isAbelianGroup : IsAbelianGroup _==_ _∙_ ε _⁻¹

  open IsAbelianGroup isAbelianGroup public

  group : Group c ℓ
  group = record { isGroup = isGroup }

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

Group Morphisms