{-# OPTIONS --without-K --safe #-}
open import Relation.Binary.Core
module Algebra.Morphism.Structures where
open import Algebra.Core
open import Algebra.Bundles
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
import Function.Definitions as FunctionDefinitions
open import Relation.Binary.Morphism.Structures
private
variable
a b ℓ₁ ℓ₂ : Level
module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) where
open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
homo : Homomorphic₂ ⟦_⟧ _∙_ _◦_
open IsRelHomomorphism isRelHomomorphism public
renaming (cong to ⟦⟧-cong)
record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsMagmaHomomorphism isMagmaHomomorphism public
isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
isRelMonomorphism = record
{ isHomomorphism = isRelHomomorphism
; injective = injective
}
record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsMagmaMonomorphism isMagmaMonomorphism public
isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
isRelIsomorphism = record
{ isMonomorphism = isRelMonomorphism
; surjective = surjective
}
module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) where
open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂)
record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
ε-homo : Homomorphic₀ ⟦_⟧ ε₁ ε₂
open IsMagmaHomomorphism isMagmaHomomorphism public
record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsMonoidHomomorphism isMonoidHomomorphism public
isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
isMagmaMonomorphism = record
{ isMagmaHomomorphism = isMagmaHomomorphism
; injective = injective
}
open IsMagmaMonomorphism isMagmaMonomorphism public
using (isRelMonomorphism)
record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsMonoidMonomorphism isMonoidMonomorphism public
isMagmaIsomorphism : IsMagmaIsomorphism ⟦_⟧
isMagmaIsomorphism = record
{ isMagmaMonomorphism = isMagmaMonomorphism
; surjective = surjective
}
open IsMagmaIsomorphism isMagmaIsomorphism public
using (isRelIsomorphism)
module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) where
open RawGroup G₁ renaming
(Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
open RawGroup G₂ renaming
(Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
open MagmaMorphisms (RawGroup.rawMagma G₁) (RawGroup.rawMagma G₂)
open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂)
record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
⁻¹-homo : Homomorphic₁ ⟦_⟧ _⁻¹₁ _⁻¹₂
open IsMonoidHomomorphism isMonoidHomomorphism public
record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsGroupHomomorphism isGroupHomomorphism public
renaming (homo to ∙-homo)
isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
isMonoidMonomorphism = record
{ isMonoidHomomorphism = isMonoidHomomorphism
; injective = injective
}
open IsMonoidMonomorphism isMonoidMonomorphism public
using (isRelMonomorphism; isMagmaMonomorphism)
record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsGroupMonomorphism isGroupMonomorphism public
isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧
isMonoidIsomorphism = record
{ isMonoidMonomorphism = isMonoidMonomorphism
; surjective = surjective
}
open IsMonoidIsomorphism isMonoidIsomorphism public
using (isRelIsomorphism; isMagmaIsomorphism)
module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSemiring b ℓ₂) where
open RawNearSemiring R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; +-rawMonoid to +-rawMonoid₁
; _*_ to _*₁_
; *-rawMagma to *-rawMagma₁)
open RawNearSemiring R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; +-rawMonoid to +-rawMonoid₂
; _*_ to _*₂_
; *-rawMagma to *-rawMagma₂)
private
module + = MonoidMorphisms +-rawMonoid₁ +-rawMonoid₂
module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
record IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
+-isMonoidHomomorphism : +.IsMonoidHomomorphism ⟦_⟧
*-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
open +.IsMonoidHomomorphism +-isMonoidHomomorphism public
renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism)
*-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
*-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = *-homo
}
record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsNearSemiringHomomorphism isNearSemiringHomomorphism public
+-isMonoidMonomorphism : +.IsMonoidMonomorphism ⟦_⟧
+-isMonoidMonomorphism = record
{ isMonoidHomomorphism = +-isMonoidHomomorphism
; injective = injective
}
open +.IsMonoidMonomorphism +-isMonoidMonomorphism public
using (isRelMonomorphism)
renaming (isMagmaMonomorphism to +-isMagmaMonomorphsm)
*-isMagmaMonomorphism : *.IsMagmaMonomorphism ⟦_⟧
*-isMagmaMonomorphism = record
{ isMagmaHomomorphism = *-isMagmaHomomorphism
; injective = injective
}
record IsNearSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsNearSemiringMonomorphism isNearSemiringMonomorphism public
+-isMonoidIsomorphism : +.IsMonoidIsomorphism ⟦_⟧
+-isMonoidIsomorphism = record
{ isMonoidMonomorphism = +-isMonoidMonomorphism
; surjective = surjective
}
open +.IsMonoidIsomorphism +-isMonoidIsomorphism public
using (isRelIsomorphism)
renaming (isMagmaIsomorphism to +-isMagmaIsomorphism)
*-isMagmaIsomorphism : *.IsMagmaIsomorphism ⟦_⟧
*-isMagmaIsomorphism = record
{ isMagmaMonomorphism = *-isMagmaMonomorphism
; surjective = surjective
}
module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ₂) where
open RawSemiring R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; 1# to 1#₁
; rawNearSemiring to rawNearSemiring₁
; *-rawMonoid to *-rawMonoid₁)
open RawSemiring R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; 1# to 1#₂
; rawNearSemiring to rawNearSemiring₂
; *-rawMonoid to *-rawMonoid₂)
private
module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
open NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂
record IsSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
1#-homo : Homomorphic₀ ⟦_⟧ 1#₁ 1#₂
open IsNearSemiringHomomorphism isNearSemiringHomomorphism public
*-isMonoidHomomorphism : *.IsMonoidHomomorphism ⟦_⟧
*-isMonoidHomomorphism = record
{ isMagmaHomomorphism = *-isMagmaHomomorphism
; ε-homo = 1#-homo
}
record IsSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsSemiringHomomorphism isSemiringHomomorphism public
isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧
isNearSemiringMonomorphism = record
{ isNearSemiringHomomorphism = isNearSemiringHomomorphism
; injective = injective
}
open IsNearSemiringMonomorphism isNearSemiringMonomorphism public
using (+-isMonoidMonomorphism; *-isMagmaMonomorphism)
*-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧
*-isMonoidMonomorphism = record
{ isMonoidHomomorphism = *-isMonoidHomomorphism
; injective = injective
}
record IsSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsSemiringMonomorphism isSemiringMonomorphism public
isNearSemiringIsomorphism : IsNearSemiringIsomorphism ⟦_⟧
isNearSemiringIsomorphism = record
{ isNearSemiringMonomorphism = isNearSemiringMonomorphism
; surjective = surjective
}
open IsNearSemiringIsomorphism isNearSemiringIsomorphism public
using (+-isMonoidIsomorphism; *-isMagmaIsomorphism)
*-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧
*-isMonoidIsomorphism = record
{ isMonoidMonomorphism = *-isMonoidMonomorphism
; surjective = surjective
}
module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
open RawRing R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; -_ to -₁_
; rawSemiring to rawSemiring₁
; *-rawMonoid to *-rawMonoid₁
; +-rawGroup to +-rawGroup₁)
open RawRing R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; -_ to -₂_
; rawSemiring to rawSemiring₂
; *-rawMonoid to *-rawMonoid₂
; +-rawGroup to +-rawGroup₂)
module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂
module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
open SemiringMorphisms rawSemiring₁ rawSemiring₂
record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
-‿homo : Homomorphic₁ ⟦_⟧ -₁_ -₂_
open IsSemiringHomomorphism isSemiringHomomorphism public
+-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧
+-isGroupHomomorphism = record
{ isMonoidHomomorphism = +-isMonoidHomomorphism
; ⁻¹-homo = -‿homo
}
record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRingHomomorphism : IsRingHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsRingHomomorphism isRingHomomorphism public
isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧
isSemiringMonomorphism = record
{ isSemiringHomomorphism = isSemiringHomomorphism
; injective = injective
}
+-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
+-isGroupMonomorphism = record
{ isGroupHomomorphism = +-isGroupHomomorphism
; injective = injective
}
open +.IsGroupMonomorphism +-isGroupMonomorphism
using (isRelMonomorphism)
renaming ( isMagmaMonomorphism to +-isMagmaMonomorphism
; isMonoidMonomorphism to +-isMonoidMonomorphism
)
*-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧
*-isMonoidMonomorphism = record
{ isMonoidHomomorphism = *-isMonoidHomomorphism
; injective = injective
}
open *.IsMonoidMonomorphism *-isMonoidMonomorphism public
using ()
renaming (isMagmaMonomorphism to *-isMagmaMonomorphism)
record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRingMonomorphism : IsRingMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsRingMonomorphism isRingMonomorphism public
isSemiringIsomorphism : IsSemiringIsomorphism ⟦_⟧
isSemiringIsomorphism = record
{ isSemiringMonomorphism = isSemiringMonomorphism
; surjective = surjective
}
+-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧
+-isGroupIsomorphism = record
{ isGroupMonomorphism = +-isGroupMonomorphism
; surjective = surjective
}
open +.IsGroupIsomorphism +-isGroupIsomorphism
using (isRelIsomorphism)
renaming ( isMagmaIsomorphism to +-isMagmaIsomorphism
; isMonoidIsomorphism to +-isMonoidIsomorphisn
)
*-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧
*-isMonoidIsomorphism = record
{ isMonoidMonomorphism = *-isMonoidMonomorphism
; surjective = surjective
}
open *.IsMonoidIsomorphism *-isMonoidIsomorphism public
using ()
renaming (isMagmaIsomorphism to *-isMagmaIsomorphisn)
module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂) where
open RawLattice L₁ renaming
( Carrier to A; _≈_ to _≈₁_
; _∧_ to _∧₁_; _∨_ to _∨₁_
; ∧-rawMagma to ∧-rawMagma₁
; ∨-rawMagma to ∨-rawMagma₁)
open RawLattice L₂ renaming
( Carrier to B; _≈_ to _≈₂_
; _∧_ to _∧₂_; _∨_ to _∨₂_
; ∧-rawMagma to ∧-rawMagma₂
; ∨-rawMagma to ∨-rawMagma₂)
module ∨ = MagmaMorphisms ∨-rawMagma₁ ∨-rawMagma₂
module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂
open MorphismDefinitions A B _≈₂_
open FunctionDefinitions _≈₁_ _≈₂_
record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
∧-homo : Homomorphic₂ ⟦_⟧ _∧₁_ _∧₂_
∨-homo : Homomorphic₂ ⟦_⟧ _∨₁_ _∨₂_
open IsRelHomomorphism isRelHomomorphism public
renaming (cong to ⟦⟧-cong)
∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧
∧-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = ∧-homo
}
∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧
∨-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = ∨-homo
}
record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧
injective : Injective ⟦_⟧
open IsLatticeHomomorphism isLatticeHomomorphism public
∨-isMagmaMonomorphism : ∨.IsMagmaMonomorphism ⟦_⟧
∨-isMagmaMonomorphism = record
{ isMagmaHomomorphism = ∨-isMagmaHomomorphism
; injective = injective
}
∧-isMagmaMonomorphism : ∧.IsMagmaMonomorphism ⟦_⟧
∧-isMagmaMonomorphism = record
{ isMagmaHomomorphism = ∧-isMagmaHomomorphism
; injective = injective
}
open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public
using (isRelMonomorphism)
record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧
surjective : Surjective ⟦_⟧
open IsLatticeMonomorphism isLatticeMonomorphism public
∨-isMagmaIsomorphism : ∨.IsMagmaIsomorphism ⟦_⟧
∨-isMagmaIsomorphism = record
{ isMagmaMonomorphism = ∨-isMagmaMonomorphism
; surjective = surjective
}
∧-isMagmaIsomorphism : ∧.IsMagmaIsomorphism ⟦_⟧
∧-isMagmaIsomorphism = record
{ isMagmaMonomorphism = ∧-isMagmaMonomorphism
; surjective = surjective
}
open ∧.IsMagmaIsomorphism ∧-isMagmaIsomorphism public
using (isRelIsomorphism)
open MagmaMorphisms public
open MonoidMorphisms public
open GroupMorphisms public
open NearSemiringMorphisms public
open SemiringMorphisms public
open RingMorphisms public
open LatticeMorphisms public