theory.ring_ideals

Require Import
Ring
ua_congruence abstract_algebra theory.rings.
Require varieties.rings.

Section ideal_congruence.
Context `{Ring R}.

Context (P: R Prop) `{!Proper ((=) ==> iff) P}.

Class Ideal: Prop :=
{ Ideal_NonEmpty:> NonEmpty P
; Ideal_closed_plus_opp: `(P x P y P (x + - y))
; Ideal_closed_mult_r: `(P x P (x * y))
; Ideal_closed_mult_l: `(P y P (x * y)) }.

Hypothesis ideal: Ideal.

Hint Resolve Ideal_closed_plus_opp Ideal_closed_mult_l Ideal_closed_mult_r.

Lemma P0: P 0.

Hint Resolve P0.

Lemma Pinv: `(P x P (- x)).

Hint Resolve Pinv.

Lemma Pplus: `(P x P y P (x + y)).

Hint Resolve Pplus.

Program Instance congruence: Equiv R := λ x y, P (x + - y).

Instance: Equivalence congruence.

Instance cong_proper: Proper ((=) ==> (=) ==> iff) congruence.

Instance: Proper (congruence ==> congruence ==> congruence) (+).

Instance: Proper (congruence ==> congruence ==> congruence) (.*.).

Instance: Proper (congruence ==> congruence) (-).

Let hint := rings.encode_operations R.

Instance: Congruence rings.sig (λ _, congruence).

Instance: Ring R (e:=congruence).

End ideal_congruence.

Section kernel_is_ideal.
Context `{Ring A} `{Ring B} `{f : A B} `{!SemiRing_Morphism f}.