summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
blob: dbce970f665dc5862aecc48e385d88311e06df57 (plain)
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
------------------------------------------------------------------------
-- Agda Helium
--
-- Morphisms for ordered algebraic structures.
------------------------------------------------------------------------

{-# OPTIONS --safe --without-K #-}

module Helium.Algebra.Ordered.StrictTotal.Morphism.Structures where

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Helium.Algebra.Ordered.StrictTotal.Bundles
open import Level using (Level; _⊔_)
open import Relation.Binary.Morphism.Structures

private
  variable
    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

module MagmaMorphisms (M₁ : RawMagma a ℓ₁ ℓ₂) (M₂ : RawMagma b ℓ₃ ℓ₄) where
  private
    module M₁ = RawMagma M₁
    module M₂ = RawMagma M₂

  open M₁ using () renaming (Carrier to A)
  open M₂ using () renaming (Carrier to B)
  open MorphismDefinitions A B M₂._≈_

  record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    field
      isOrderHomomorphism : IsOrderHomomorphism M₁._≈_ M₂._≈_ M₁._<_ M₂._<_ ⟦_⟧
      homo                : Homomorphic₂ ⟦_⟧ M₁._∙_ M₂._∙_

    open IsOrderHomomorphism isOrderHomomorphism public

module MonoidMorphisms (M₁ : RawMonoid a ℓ₁ ℓ₂) (M₂ : RawMonoid b ℓ₃ ℓ₄) where
  private
    module M₁ = RawMonoid M₁
    module M₂ = RawMonoid M₂

  open M₁ using () renaming (Carrier to A)
  open M₂ using () renaming (Carrier to B)
  open MorphismDefinitions A B M₂._≈_
  open MagmaMorphisms M₁.rawMagma M₂.rawMagma

  record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    field
      isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
      ε-homo              : Homomorphic₀ ⟦_⟧ M₁.ε M₂.ε

    open IsMagmaHomomorphism isMagmaHomomorphism public

module GroupMorphisms (G₁ : RawGroup a ℓ₁ ℓ₂) (G₂ : RawGroup b ℓ₃ ℓ₄) where
  private
    module G₁ = RawGroup G₁
    module G₂ = RawGroup G₂

  open G₁ using () renaming (Carrier to A)
  open G₂ using () renaming (Carrier to B)
  open MorphismDefinitions A B G₂._≈_
  open MonoidMorphisms G₁.rawMonoid G₂.rawMonoid

  record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    field
      isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
      ⁻¹-homo              : Homomorphic₁ ⟦_⟧ G₁._⁻¹ G₂._⁻¹

    open IsMonoidHomomorphism isMonoidHomomorphism public

module RingMorphisms (R₁ : RawRing a ℓ₁ ℓ₂) (R₂ : RawRing b ℓ₃ ℓ₄) where
  private
    module R₁ = RawRing R₁
    module R₂ = RawRing R₂

  open R₁ using () renaming (Carrier to A)
  open R₂ using () renaming (Carrier to B)
  open MorphismDefinitions A B R₂._≈_
  open GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup

  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    field
      +-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
      *-homo                : Homomorphic₂ ⟦_⟧ R₁._*_ R₂._*_
      1#-homo               : Homomorphic₀ ⟦_⟧ R₁.1# R₂.1#

    open IsGroupHomomorphism +-isGroupHomomorphism public
      renaming
      ( homo to +-homo
      ; ε-homo to 0#-homo
      ; ⁻¹-homo to -‿homo
      ; isMagmaHomomorphism to +-isMagmaHomomorphism
      ; isMonoidHomomorphism to +-isMonoidHomomorphism
      )

open MagmaMorphisms public
open MonoidMorphisms public
open GroupMorphisms public
open RingMorphisms public