Ideals and coideals

Definition of ideals and coideals

Let R be a ring. At this moment all CRings are commutative and non-trivial. So our ideals are automatically two-sided. As soon as non-commutative rings are represented in CoRN left and right ideals should be defined.

Section Ideals.

Variable R : CRing.

Record is_ideal (idP : wd_pred R) : CProp :=
  { idax : forall a x:R, idP a -> idP (a[*]x);
    idprpl : forall x y : R, idP x -> idP y -> idP (x[+]y)}.

Record ideal : Type :=
  { idpred :> wd_pred R;
    idproof : is_ideal idpred}.

We actually define strongly non-trivival co-ideals.

Record is_coideal (ciP : wd_pred R) : CProp :=
  { ciapzero : forall x:R, ciP x -> x[#]0;
    ciplus : forall x y:R, ciP (x[+]y) -> ciP x or ciP y;
    cimult : forall x y:R, ciP (x[*]y) -> ciP x and ciP y;
    cinontriv : ciP 1}.

Record coideal : Type :=
  { cipred :> wd_pred R;
    ciproof : is_coideal cipred}.

End Ideals.

Axioms of ideals and coideals

Let R be a ring, I and ideal of R and C a coideal of R.

Section Ideal_Axioms.

Variable R : CRing.
Variable I : ideal R.
Variable C : coideal R.

Lemma ideal_is_ideal : is_ideal I.

Lemma coideal_is_coideal : is_coideal C.

Lemma coideal_apzero : forall x:R, C x -> x[#]0.

Lemma coideal_nonzero : ~ (C 0).

Lemma coideal_plus : forall x y:R, C (x[+]y) -> C x or C y.

Lemma coideal_mult : forall x y:R, C (x[*]y) -> C x and C y.

Lemma coideal_nontriv : C 1.

Lemma coideal_wd : forall x y:R, x[=]y -> C x -> C y.

End Ideal_Axioms.