{-# OPTIONS --without-K --safe #-}
module Algebra.Morphism where
open import Relation.Binary
open import Algebra
import Algebra.Properties.Group as GroupP
open import Function
open import Level
import Relation.Binary.Reasoning.Setoid as EqR
module Definitions {f t ℓ}
(From : Set f) (To : Set t) (_≈_ : Rel To ℓ) where
Morphism : Set _
Morphism = From → To
Homomorphic₀ : Morphism → From → To → Set _
Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘
Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set _
Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set _
Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : RawMagma c₁ ℓ₁)
(To : RawMagma c₂ ℓ₂) where
private
module F = RawMagma From
module T = RawMagma To
open Definitions F.Carrier T.Carrier T._≈_
record IsRawMagmaMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
F-isMagma : IsMagma F._≈_ F._∙_
T-isMagma : IsMagma T._≈_ T._∙_
⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
open IsMagma F-isMagma public using ()
renaming
( ∙-cong to F-∙-cong
; ∙-congˡ to F-∙-congˡ
; ∙-congʳ to F-∙-congʳ
; setoid to F-setoid
)
open IsMagma T-isMagma public using ()
renaming
( ∙-cong to T-∙-cong
; ∙-congˡ to T-∙-congˡ
; ∙-congʳ to T-∙-congʳ
; setoid to T-setoid
)
IsRawMagmaMorphism-syntax = IsRawMagmaMorphism
syntax IsRawMagmaMorphism-syntax From To F = F Is From -RawMagma⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : RawMonoid c₁ ℓ₁)
(To : RawMonoid c₂ ℓ₂) where
private
module F = RawMonoid From
module T = RawMonoid To
open Definitions F.Carrier T.Carrier T._≈_
record IsRawMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
magma-homo : IsRawMagmaMorphism F.rawMagma T.rawMagma ⟦_⟧
ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε
open IsRawMagmaMorphism magma-homo public
IsRawMonoidMorphism-syntax = IsRawMonoidMorphism
syntax IsRawMonoidMorphism-syntax From To F = F Is From -RawMonoid⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Semigroup c₁ ℓ₁)
(To : Semigroup c₂ ℓ₂) where
private
module F = Semigroup From
module T = Semigroup To
open Definitions F.Carrier T.Carrier T._≈_
record IsSemigroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
IsSemigroupMorphism-syntax = IsSemigroupMorphism
syntax IsSemigroupMorphism-syntax From To F = F Is From -Semigroup⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Monoid c₁ ℓ₁)
(To : Monoid c₂ ℓ₂) where
private
module F = Monoid From
module T = Monoid To
open Definitions F.Carrier T.Carrier T._≈_
record IsMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε
open IsSemigroupMorphism sm-homo public
IsMonoidMorphism-syntax = IsMonoidMorphism
syntax IsMonoidMorphism-syntax From To F = F Is From -Monoid⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : CommutativeMonoid c₁ ℓ₁)
(To : CommutativeMonoid c₂ ℓ₂) where
private
module F = CommutativeMonoid From
module T = CommutativeMonoid To
open Definitions F.Carrier T.Carrier T._≈_
record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
open IsMonoidMorphism mn-homo public
IsCommutativeMonoidMorphism-syntax = IsCommutativeMonoidMorphism
syntax IsCommutativeMonoidMorphism-syntax From To F = F Is From -CommutativeMonoid⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : IdempotentCommutativeMonoid c₁ ℓ₁)
(To : IdempotentCommutativeMonoid c₂ ℓ₂) where
private
module F = IdempotentCommutativeMonoid From
module T = IdempotentCommutativeMonoid To
open Definitions F.Carrier T.Carrier T._≈_
record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
open IsMonoidMorphism mn-homo public
isCommutativeMonoidMorphism :
IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧
isCommutativeMonoidMorphism = record { mn-homo = mn-homo }
IsIdempotentCommutativeMonoidMorphism-syntax = IsIdempotentCommutativeMonoidMorphism
syntax IsIdempotentCommutativeMonoidMorphism-syntax From To F = F Is From -IdempotentCommutativeMonoid⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Group c₁ ℓ₁)
(To : Group c₂ ℓ₂) where
private
module F = Group From
module T = Group To
open Definitions F.Carrier T.Carrier T._≈_
record IsGroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
open IsMonoidMorphism mn-homo public
⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
⟦ x F.⁻¹ F.∙ x ⟧ ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
⟦ F.ε ⟧ ≈⟨ ε-homo ⟩
T.ε ∎
IsGroupMorphism-syntax = IsGroupMorphism
syntax IsGroupMorphism-syntax From To F = F Is From -Group⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : AbelianGroup c₁ ℓ₁)
(To : AbelianGroup c₂ ℓ₂) where
private
module F = AbelianGroup From
module T = AbelianGroup To
open Definitions F.Carrier T.Carrier T._≈_
record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
gp-homo : IsGroupMorphism F.group T.group ⟦_⟧
open IsGroupMorphism gp-homo public
IsAbelianGroupMorphism-syntax = IsAbelianGroupMorphism
syntax IsAbelianGroupMorphism-syntax From To F = F Is From -AbelianGroup⟶ To
module _ {c₁ ℓ₁ c₂ ℓ₂}
(From : Ring c₁ ℓ₁)
(To : Ring c₂ ℓ₂) where
private
module F = Ring From
module T = Ring To
open Definitions F.Carrier T.Carrier T._≈_
record IsRingMorphism (⟦_⟧ : Morphism) :
Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
field
+-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup
*-mn-homo : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid
IsRingMorphism-syntax = IsRingMorphism
syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To