agda-stdlib/src/Algebra/Construct/Centre/Monoid.agda at b0b4651e504cc78c91c6e1e843cd114b46c2f68c · jamesmckinna/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definition of the centre of an Monoid
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical-compatible #-}

open import Algebra.Bundles
  using (Monoid; CommutativeMonoid; RawMagma; RawMonoid)

module Algebra.Construct.Centre.Monoid
  {c ℓ} (monoid : Monoid c ℓ)
  where

open import Algebra.Morphism.Structures using (IsMonoidMonomorphism)
open import Algebra.Morphism.MonoidMonomorphism using (isMonoid)
open import Function.Base using (id)

open import Algebra.Properties.Monoid monoid using (ε-central)

private
  module X = Monoid monoid


------------------------------------------------------------------------
-- Definition

-- Re-export the underlying sub-Semigroup

open import Algebra.Construct.Centre.Semigroup X.semigroup as Z public
  using (Centre; ι; ∙-comm)

-- Now, can define a sub-Monoid

domain : RawMonoid _ _
domain = record { RawMagma Z.domain; ε = ε }
  where
  ε : Centre
  ε = record
    { ι = X.ε
    ; central = ε-central
    }

isMonoidMonomorphism : IsMonoidMonomorphism domain X.rawMonoid ι
isMonoidMonomorphism = record
  { isMonoidHomomorphism = record
    { isMagmaHomomorphism = Z.isMagmaHomomorphism
    ; ε-homo = X.refl
    }
  ; injective = id
  }

-- Public export of the sub-X-homomorphisms

open IsMonoidMonomorphism isMonoidMonomorphism public
  using (isMonoidHomomorphism; isMagmaHomomorphism)

-- And hence a CommutativeMonoid

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
  { isCommutativeMonoid = record
    { isMonoid = isMonoid isMonoidMonomorphism X.isMonoid
    ; comm = ∙-comm
    }
  }

-- Public export of the sub-X-structures/bundles

open CommutativeMonoid commutativeMonoid public
  using (isCommutativeMonoid; isMonoid
        ; isCommutativeSemigroup; isSemigroup
        ; isCommutativeMagma; isMagma
        ; monoid
        ; commutativeSemigroup; semigroup
        ; commutativeMagma; magma
        )

-- Public export of the bundle

Z[_] = commutativeMonoid