theory.ring_ideals


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

Section ideal_congruence.
  Context `{Ring R}.

  Add Ring R: (rings.stdlib_ring_theory 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}.

  Add Ring A: (rings.stdlib_ring_theory A).
  Add Ring B: (rings.stdlib_ring_theory B).

  Definition kernel: A Prop := (= 0) f.

  Global Instance: Ideal kernel.
End kernel_is_ideal.