module Algebra.ringMorphisms where
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.relations
open import Types.equality
open import Types.functions2
open import Algebra.groups
open import Algebra.groups2
open import Algebra.groupMorphisms
open import Algebra.rings
open import Algebra.rings2Ring morphisms are maps between two rings that preserve the ring structure. These follow the same theme that the group-like objects did in Group Morphisms.
module _ {f t ℓ₁ ℓ₂} (From : Ring f ℓ₁) (To : Ring t ℓ₂) where
private
module F = Ring From
module T = Ring To
open Homomorphism F.Data T.Data T._≈_
record IsRingHomomorphism (𝕄⟦_⟧ : Morphism) : Set (f ⊔ t ⊔ ℓ₁ ⊔ ℓ₂) where
field
+-isGroupHomomorphism : IsGroupHomomorphism F.+-group T.+-group 𝕄⟦_⟧
*-isMonoidHomomorphism : IsMonoidHomomorphism F.*-monoid T.*-monoid 𝕄⟦_⟧Automorphisms are pretty straightforward:
module _ {f t ℓ} (Self : Ring f ℓ) where
private
module F = Ring Self
module T = Ring Self
open Homomorphism F.Data T.Data T._≈_
record IsRingAutomorphism (𝕄⟦_⟧ : Morphism) : Set (f ⊔ t ⊔ ℓ) where
field
+-isGroupHomomorphism : IsGroupHomomorphism F.+-group T.+-group 𝕄⟦_⟧
*-isMonoidHomomorphism : IsMonoidHomomorphism F.*-monoid T.*-monoid 𝕄⟦_⟧For monomorphism we add the injective condition:
module _ {f t ℓ₁ ℓ₂} (From : Ring f ℓ₁) (To : Ring t ℓ₂) where
private
module F = Ring From
module T = Ring To
open Homomorphism F.Data T.Data T._≈_
record IsRingMonomorphism (𝕄⟦_⟧ : Morphism) : Set (f ⊔ t ⊔ ℓ₁ ⊔ ℓ₂) where
field
is-ring-homomorphism : IsRingHomomorphism From To 𝕄⟦_⟧
is-injective : Injective 𝕄⟦_⟧Finally for isomorphism we add the surjective condition:
module _ {f t ℓ₁ ℓ₂} (From : Ring f ℓ₁) (To : Ring t ℓ₂) where
private
module F = Ring From
module T = Ring To
open Homomorphism F.Data T.Data T._≈_
record IsRingIsomorphism (𝕄⟦_⟧ : Morphism) : Set (f ⊔ t ⊔ ℓ₁ ⊔ ℓ₂) where
field
is-ring-homomorphism : IsRingMonomorphism From To 𝕄⟦_⟧
is-injective : Surjective 𝕄⟦_⟧