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].
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.