------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic structures ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Morphism where import Algebra.Morphism.Definitions as MorphismDefinitions open import Algebra open import Function.Base open import Level open import Relation.Binary.Core using (Rel; _Preserves_⟶_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable a b ℓ₁ ℓ₂ : Level A : Set a B : Set b ------------------------------------------------------------------------ -- Re-export module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where open MorphismDefinitions A B _≈_ public open import Algebra.Morphism.Structures public ------------------------------------------------------------------------ -- DEPRECATED ------------------------------------------------------------------------ -- Please use the new definitions re-exported from -- `Algebra.Morphism.Structures` as continuing support for the below is -- no guaranteed. -- Version 1.5 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 ≈-Reasoning 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 IsMagmaHomomorphism 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." #-}