# Kernels of ring homomorphisms

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.

module ring-theory.kernels-of-ring-homomorphisms where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.kernels-homomorphisms-groups
open import group-theory.subgroups-abelian-groups

open import ring-theory.homomorphisms-rings
open import ring-theory.ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


## Idea

The kernel of a ring homomorphism f : R → S is the ideal of R consisting of all elements x : R equipped with an identification f x ＝ 0.

## Definitions

### The kernel of a ring homomorphism

module _
{l1 l2 : Level} (R : Ring l1) (S : Ring l2) (f : hom-Ring R S)
where

subgroup-kernel-hom-Ring : Subgroup-Ab l2 (ab-Ring R)
subgroup-kernel-hom-Ring =
subgroup-kernel-hom-Group
( group-Ring R)
( group-Ring S)
( hom-group-hom-Ring R S f)

subset-kernel-hom-Ring : subset-Ring l2 R
subset-kernel-hom-Ring =
subset-Subgroup-Ab (ab-Ring R) subgroup-kernel-hom-Ring

contains-zero-kernel-hom-Ring :
contains-zero-subset-Ring R subset-kernel-hom-Ring
contains-zero-kernel-hom-Ring =
contains-zero-Subgroup-Ab (ab-Ring R) subgroup-kernel-hom-Ring

is-closed-under-negatives-kernel-hom-Ring :
is-closed-under-negatives-subset-Ring R subset-kernel-hom-Ring
is-closed-under-negatives-kernel-hom-Ring =
is-closed-under-negatives-Subgroup-Ab (ab-Ring R) subgroup-kernel-hom-Ring

contains-zero-kernel-hom-Ring
is-closed-under-negatives-kernel-hom-Ring

is-closed-under-left-multiplication-kernel-hom-Ring :
is-closed-under-left-multiplication-subset-Ring R subset-kernel-hom-Ring
is-closed-under-left-multiplication-kernel-hom-Ring x y H =
( inv (right-zero-law-mul-Ring S _)) ∙
( ap (mul-Ring S _) H) ∙
( inv (preserves-mul-hom-Ring R S f))

is-closed-under-right-multiplication-kernel-hom-Ring :
is-closed-under-right-multiplication-subset-Ring R subset-kernel-hom-Ring
is-closed-under-right-multiplication-kernel-hom-Ring x y H =
( inv (left-zero-law-mul-Ring S _)) ∙
( ap (mul-Ring' S _) H) ∙
( inv (preserves-mul-hom-Ring R S f))

kernel-hom-Ring : ideal-Ring l2 R
pr1 kernel-hom-Ring =
subset-kernel-hom-Ring
pr1 (pr2 kernel-hom-Ring) =
pr1 (pr2 (pr2 kernel-hom-Ring)) =
is-closed-under-left-multiplication-kernel-hom-Ring
pr2 (pr2 (pr2 kernel-hom-Ring)) =
is-closed-under-right-multiplication-kernel-hom-Ring