------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic structures ------------------------------------------------------------------------ {-# OPTIONS --without-K --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 ------------------------------------------------------------------------ -- 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 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." #-}
Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.