{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Morphism.Structures where
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Bundles
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
open import Function.Definitions using (Injective; Surjective)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Morphism.Structures
using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism)
private
variable
a b ℓ₁ ℓ₂ : Level
module SuccessorSetMorphisms
(N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂)
where
open RawSuccessorSet N₁
renaming (Carrier to A; _≈_ to _≈₁_; suc# to suc#₁; zero# to zero#₁)
open RawSuccessorSet N₂
renaming (Carrier to B; _≈_ to _≈₂_; suc# to suc#₂; zero# to zero#₂)
open MorphismDefinitions A B _≈₂_
record IsSuccessorSetHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
suc#-homo : Homomorphic₁ ⟦_⟧ suc#₁ suc#₂
zero#-homo : Homomorphic₀ ⟦_⟧ zero#₁ zero#₂
record IsSuccessorSetMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSuccessorSetHomomorphism : IsSuccessorSetHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsSuccessorSetHomomorphism isSuccessorSetHomomorphism public
isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
isRelMonomorphism = record
{ isHomomorphism = isRelHomomorphism
; injective = injective
}
record IsSuccessorSetIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSuccessorSetMonomorphism : IsSuccessorSetMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsSuccessorSetMonomorphism isSuccessorSetMonomorphism public
isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
isRelIsomorphism = record
{ isMonomorphism = isRelMonomorphism
; surjective = surjective
}
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 _≈₂_
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 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 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 _≈₂_
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 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 RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRingWithoutOne b ℓ₂) where
open RawRingWithoutOne R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; _*_ to _*₁_
; *-rawMagma to *-rawMagma₁
; +-rawGroup to +-rawGroup₁
; rawNearSemiring to rawNearSemiring₁)
open RawRingWithoutOne R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; _*_ to _*₂_
; *-rawMagma to *-rawMagma₂
; +-rawGroup to +-rawGroup₂
; rawNearSemiring to rawNearSemiring₂)
private
module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂
module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂
module +* = NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂
open MorphismDefinitions A B _≈₂_
record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
+-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧
*-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
open +.IsGroupHomomorphism +-isGroupHomomorphism public
renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism)
isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧
isNearSemiringHomomorphism = record
{ +-isMonoidHomomorphism = +-isMonoidHomomorphism
; *-homo = *-homo
}
*-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
*-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = *-homo
}
record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public
+-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
+-isGroupMonomorphism = record
{ isGroupHomomorphism = +-isGroupHomomorphism
; injective = injective
}
open +.IsGroupMonomorphism +-isGroupMonomorphism public
using (isRelMonomorphism)
renaming (isMagmaMonomorphism to +-isMagmaMonomorphsm; isMonoidMonomorphism to +-isMonoidMonomorphism)
*-isMagmaMonomorphism : *.IsMagmaMonomorphism ⟦_⟧
*-isMagmaMonomorphism = record
{ isMagmaHomomorphism = *-isMagmaHomomorphism
; injective = injective
}
record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRingWithoutOneMonomorphism : IsRingWithoutOneMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsRingWithoutOneMonomorphism isRingWithoutOneMonomorphism public
+-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧
+-isGroupIsomorphism = record
{ isGroupMonomorphism = +-isGroupMonomorphism
; surjective = surjective
}
open +.IsGroupIsomorphism +-isGroupIsomorphism public
using (isRelIsomorphism)
renaming (isMagmaIsomorphism to +-isMagmaIsomorphism; isMonoidIsomorphism to +-isMonoidIsomorphism)
*-isMagmaIsomorphism : *.IsMagmaIsomorphism ⟦_⟧
*-isMagmaIsomorphism = record
{ isMagmaMonomorphism = *-isMagmaMonomorphism
; surjective = surjective
}
module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
open RawRing R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; -_ to -₁_
; rawRingWithoutOne to rawRingWithoutOne₁
; rawSemiring to rawSemiring₁
; *-rawMonoid to *-rawMonoid₁
; +-rawGroup to +-rawGroup₁)
open RawRing R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; -_ to -₂_
; rawRingWithoutOne to rawRingWithoutOne₂
; rawSemiring to rawSemiring₂
; *-rawMonoid to *-rawMonoid₂
; +-rawGroup to +-rawGroup₂)
module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂
module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
module *+0 = RingWithoutOneMorphisms rawRingWithoutOne₁ rawRingWithoutOne₂
open MorphismDefinitions A B _≈₂_
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
}
isRingWithoutOneHomomorphism : *+0.IsRingWithoutOneHomomorphism ⟦_⟧
isRingWithoutOneHomomorphism = record
{ +-isGroupHomomorphism = +-isGroupHomomorphism
; *-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 QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup b ℓ₂) where
open RawQuasigroup Q₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
\\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
_≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_)
open RawQuasigroup Q₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
\\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
_≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_)
module ∙ = MagmaMorphisms ∙-rawMagma₁ ∙-rawMagma₂
module \\ = MagmaMorphisms \\-rawMagma₁ \\-rawMagma₂
module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂
open MorphismDefinitions A B _≈₂_
record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
∙-homo : Homomorphic₂ ⟦_⟧ _∙₁_ _∙₂_
\\-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
}
//-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧
//-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = //-homo
}
record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
∙-isMagmaMonomorphism : ∙.IsMagmaMonomorphism ⟦_⟧
∙-isMagmaMonomorphism = record
{ isMagmaHomomorphism = ∙-isMagmaHomomorphism
; injective = injective
}
\\-isMagmaMonomorphism : \\.IsMagmaMonomorphism ⟦_⟧
\\-isMagmaMonomorphism = record
{ isMagmaHomomorphism = \\-isMagmaHomomorphism
; injective = injective
}
//-isMagmaMonomorphism : //.IsMagmaMonomorphism ⟦_⟧
//-isMagmaMonomorphism = record
{ isMagmaHomomorphism = //-isMagmaHomomorphism
; injective = injective
}
open //.IsMagmaMonomorphism //-isMagmaMonomorphism public
using (isRelMonomorphism)
record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsQuasigroupMonomorphism isQuasigroupMonomorphism public
∙-isMagmaIsomorphism : ∙.IsMagmaIsomorphism ⟦_⟧
∙-isMagmaIsomorphism = record
{ isMagmaMonomorphism = ∙-isMagmaMonomorphism
; surjective = surjective
}
\\-isMagmaIsomorphism : \\.IsMagmaIsomorphism ⟦_⟧
\\-isMagmaIsomorphism = record
{ isMagmaMonomorphism = \\-isMagmaMonomorphism
; surjective = surjective
}
//-isMagmaIsomorphism : //.IsMagmaIsomorphism ⟦_⟧
//-isMagmaIsomorphism = record
{ isMagmaMonomorphism = //-isMagmaMonomorphism
; surjective = surjective
}
open //.IsMagmaIsomorphism //-isMagmaIsomorphism public
using (isRelIsomorphism)
module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
open RawLoop L₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
\\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
_≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_; ε to ε₁)
open RawLoop L₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
\\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
_≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂)
open MorphismDefinitions A B _≈₂_
open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂)
record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
ε-homo : Homomorphic₀ ⟦_⟧ ε₁ ε₂
open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLoopHomomorphism : IsLoopHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsLoopHomomorphism isLoopHomomorphism public
record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLoopMonomorphism : IsLoopMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsLoopMonomorphism isLoopMonomorphism public
module KleeneAlgebraMorphisms (R₁ : RawKleeneAlgebra a ℓ₁) (R₂ : RawKleeneAlgebra b ℓ₂) where
open RawKleeneAlgebra R₁ renaming
( Carrier to A; _≈_ to _≈₁_
; _⋆ to _⋆₁
; rawSemiring to rawSemiring₁
)
open RawKleeneAlgebra R₂ renaming
( Carrier to B; _≈_ to _≈₂_
; _⋆ to _⋆₂
; rawSemiring to rawSemiring₂
)
open MorphismDefinitions A B _≈₂_
open SemiringMorphisms rawSemiring₁ rawSemiring₂
record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
⋆-homo : Homomorphic₁ ⟦_⟧ _⋆₁ _⋆₂
open IsSemiringHomomorphism isSemiringHomomorphism public
record IsKleeneAlgebraMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public
record IsKleeneAlgebraIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isKleeneAlgebraMonomorphism : IsKleeneAlgebraMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsKleeneAlgebraMonomorphism isKleeneAlgebraMonomorphism public
open MagmaMorphisms public
open MonoidMorphisms public
open GroupMorphisms public
open NearSemiringMorphisms public
open SemiringMorphisms public
open RingWithoutOneMorphisms public
open RingMorphisms public
open QuasigroupMorphisms public
open LoopMorphisms public
open KleeneAlgebraMorphisms public