CoRN.old.CIdeals

Require Export CRings.

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 : ∀ a x:R, idP a → idP (a×x);
    idprpl : ∀ 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 : ∀ x:R, ciP x → x[#]0;
    ciplus : ∀ x y:R, ciP (x+y) → ciP x or ciP y;
    cimult : ∀ 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.

Implicit Arguments is_ideal [R].
Implicit Arguments is_coideal [R].

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.
Proof.
elim I; auto.
Qed.

Lemma coideal_is_coideal : is_coideal C.
Proof.
elim C; auto.
Qed.

Lemma coideal_apzero : ∀ x:R, C x → x[#]0.
Proof.
elim C. intuition elim ciproof0.
Qed.

Lemma coideal_nonzero : Not (C 0).
Proof.
intro.
cut ((0:R)[#](0:R)); try apply coideal_apzero; try assumption.
apply ap_irreflexive.
Qed.

Lemma coideal_plus : ∀ x y:R, C (x+y) → C x or C y.
Proof.
elim C. intuition elim ciproof0.
Qed.

Lemma coideal_mult : ∀ x y:R, C (x×y) → C x and C y.
Proof.
elim C. intuition elim ciproof0.
Qed.

Lemma coideal_nontriv : C 1.
Proof.
elim C. intuition elim ciproof0.
Qed.

Lemma coideal_wd : ∀ x y:R, x≡y → C x → C y.
Proof.
elim C. simpl in |-*. intro.
elim cipred0. intros.
apply (wdp_well_def x y); auto.
Qed.

End Ideal_Axioms.

Hint Resolve coideal_apzero coideal_nonzero coideal_plus: algebra.
Hint Resolve coideal_mult coideal_wd coideal_nontriv: algebra.