{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Morphism where
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra
import Algebra.Properties.Group as GroupP
open import Function hiding (Morphism)
open import Level
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as EqR
private
variable
a b ℓ₁ ℓ₂ : Level
A : Set a
B : Set b
module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
open MorphismDefinitions A B _≈_ public
open import Algebra.Morphism.Structures public
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
{-# WARNING_ON_USAGE IsSemigroupMorphism
"Warning: IsSemigroupMorphism was deprecated in v1.5.
Please use IsSemigroupHomomorphism instead."
#-}
{-# WARNING_ON_USAGE IsMonoidMorphism
"Warning: IsMonoidMorphism was deprecated in v1.5.
Please use IsMonoidHomomorphism instead."
#-}
{-# WARNING_ON_USAGE IsCommutativeMonoidMorphism
"Warning: IsCommutativeMonoidMorphism was deprecated in v1.5.
Please use IsMonoidHomomorphism instead."
#-}
{-# WARNING_ON_USAGE IsIdempotentCommutativeMonoidMorphism
"Warning: IsIdempotentCommutativeMonoidMorphism was deprecated in v1.5.
Please use IsMonoidHomomorphism instead."
#-}
{-# WARNING_ON_USAGE IsGroupMorphism
"Warning: IsGroupMorphism was deprecated in v1.5.
Please use IsGroupHomomorphism instead."
#-}
{-# WARNING_ON_USAGE IsAbelianGroupMorphism
"Warning: IsAbelianGroupMorphism was deprecated in v1.5.
Please use IsGroupHomomorphism instead."
#-}