Mathlib.RingTheory.TwoSidedIdeal.Kernel

Module docstring

{"# Kernel of a ring homomorphism as a two-sided ideal

In this file we define the kernel of a ring homomorphism f : R → S as a two-sided ideal of R.

We put this in a separate file so that we could import it in SimpleRing/Basic.lean without importing any finiteness result. "}

TwoSidedIdeal.ker definition

: TwoSidedIdeal R

Full source

/--
The kernel of a ring homomorphism, as a two-sided ideal.
-/
def ker : TwoSidedIdeal R :=
  .mk
  { r := fun x y ↦ f x = f y
    iseqv := by constructor <;> aesop
    mul' := by intro; simp_all [map_add]
    add' := by intro; simp_all [map_mul] }

Kernel of a ring homomorphism as a two-sided ideal

Informal description

The kernel of a ring homomorphism $ f : R \to S $ is the two-sided ideal of $ R $ consisting of all elements $ x \in R $ such that $ f(x) = 0 $.

TwoSidedIdeal.ker_ringCon theorem

{x y : R} : (ker f).ringCon x y ↔ f x = f y

Full source

@[simp]
lemma ker_ringCon {x y : R} : (ker f).ringCon x y ↔ f x = f y := Iff.rfl

Kernel Congruence Relation Characterization: $(x, y) \in \text{ker}(f).\text{ringCon} \leftrightarrow f(x) = f(y)$

Informal description

For any elements $x, y$ in a ring $R$, the ring congruence relation induced by the kernel of a ring homomorphism $f : R \to S$ satisfies $(x, y) \in \text{ker}(f).\text{ringCon}$ if and only if $f(x) = f(y)$.

TwoSidedIdeal.mem_ker theorem

{x : R} : x ∈ ker f ↔ f x = 0

Full source

lemma mem_ker {x : R} : x ∈ ker fx ∈ ker f ↔ f x = 0 := by
  rw [mem_iff, ker_ringCon, map_zero]

Characterization of Kernel Membership: $x \in \ker f \leftrightarrow f(x) = 0$

Informal description

For any element $x$ in a ring $R$, $x$ belongs to the kernel of a ring homomorphism $f : R \to S$ if and only if $f(x) = 0$.

TwoSidedIdeal.ker_eq_bot theorem

: ker f = ⊥ ↔ Function.Injective f

Full source

lemma ker_eq_bot : kerker f = ⊥ ↔ Function.Injective f := by
  fconstructor
  · intro h x y hxy
    simpa [h, rel_iff, mem_bot, sub_eq_zero] using show (ker f).ringCon x y from hxy
  · exact fun h ↦ eq_bot_iff.2 fun x hx => h hx

Kernel is Trivial if and only if Homomorphism is Injective

Informal description

For a ring homomorphism $f \colon R \to S$, the kernel of $f$ is equal to the zero ideal $\{0\}$ if and only if $f$ is injective.

TwoSidedIdeal.ker_ringCon_mk' theorem

(I : TwoSidedIdeal R) : ker I.ringCon.mk' = I

Full source

/--
The kernel of the ring homomorphism `R → R⧸I` is `I`.
-/
@[simp]
lemma ker_ringCon_mk' (I : TwoSidedIdeal R) : ker I.ringCon.mk' = I :=
  le_antisymm
    (fun _ h => by simpa using I.rel_iff _ _ |>.1 (Quotient.eq'.1 h))
    (fun _ h => Quotient.sound' <| I.rel_iff _ _ |>.2 (by simpa using h))

Kernel of Quotient Projection Equals Ideal: $\ker(R \to R/I) = I$

Informal description

For any two-sided ideal $I$ of a ring $R$, the kernel of the canonical projection homomorphism $R \to R/I$ is equal to $I$ itself.