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 Mathlib/RingTheory/SimpleRing/Basic.lean without importing any finiteness result.

def TwoSidedIdeal.ker {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) : TwoSidedIdeal R

The kernel of a ring homomorphism, as a two-sided ideal.

Equations

• TwoSidedIdeal.ker f = { ringCon := { r := fun (x y : R) => f x = f y, iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

@[simp]

theorem TwoSidedIdeal.ker_ringCon {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x y : R} : (ker f).ringCon x y ↔ f x = f y

theorem TwoSidedIdeal.mem_ker {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R} : x ∈ ker f ↔ f x = 0

theorem TwoSidedIdeal.ker_eq_bot {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) : ker f = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem TwoSidedIdeal.ker_ringCon_mk' {R : Type u_4} [NonAssocRing R] (I : TwoSidedIdeal R) : ker I.ringCon.mk' = I

The kernel of the ring homomorphism R → R⧸I is I.