CoRN.old.CQuotient_Rings

Require Export CIdeals.

Quotient Rings

Let R be a ring and C a coideal of R. We will prove that A / ~C is a ring, called QuotRing.

QuotRing is a setoid

To achieve this we define a new apartness on the elements of R.

Section QuotRing.

Variable R : CRing.
Variable C : coideal R.

Definition ap_quotring (x y:R) := C(x−y).

Lemma ap_quotring_irreflexive : irreflexive ap_quotring.
Proof.
red in |-*.
intro x.
unfold ap_quotring in |-*.
assert (x−x≡0); algebra.
assert (Not ((cipred R C) 0)); algebra.
intro. apply H0.
apply (coideal_wd R C (x−x) 0); auto.
Qed.

Lemma ap_quotring_symmetric : Csymmetric ap_quotring.
Proof.
red in |-*.
intros x y.
unfold ap_quotring.
intro X.
cut (C −1 and C (y−x)). intuition.
apply (coideal_mult R C −1 (y−x)).
apply (coideal_wd R C (x−y) ([--]1[*](y−x))); algebra.
astepr [--](y−x).
astepr [--](y[+][--]x).
astepr ([--][--]x[+][--]y).
Step_final (x[+][--]y).
Qed.

Lemma ap_quotring_cotransitive : cotransitive ap_quotring.
Proof.
red in |-*.
intros x y; unfold ap_quotring.
intros X z.
apply (coideal_plus R C (x−z) (z−y)).
apply (coideal_wd R C (x−y) ((x−z)[+](z−y))); auto.
astepr ((x−z)[+]z−y).
astepr ((x−z)[+]z[+][--]y).
astepr ((x[+][--]z)[+]z[+][--]y).
astepr (x[+]([--]z+z)[+][--]y).
astepr (x+0[+][--]y).
astepr (x[+][--]y).
astepr (x−y).
apply eq_reflexive.
Qed.

We take `not apart' as the new equality.

Definition eq_quotring (x y:R) := Not (C(x−y)).

Lemma eq_quotring_wd : ∀ (x y:R), x≡y → (eq_quotring x y).
Proof.
intros x y X; auto.
red in |-*; intro X0.
assert ((cipred R C)(0)); algebra.
apply (coideal_wd R C (x−y) 0); algebra.
apply x_minus_x; auto.
apply (coideal_nonzero R C); assumption.
Qed.

Lemma ap_quotring_tight : tight_apart eq_quotring ap_quotring.
Proof.
red in |-*.
intros x y; intuition.
Qed.

Definition ap_quotring_is_apartness :=
Build_is_CSetoid R eq_quotring ap_quotring
ap_quotring_irreflexive
ap_quotring_symmetric
ap_quotring_cotransitive
ap_quotring_tight.

Definition quotring_as_CSetoid := Build_CSetoid _ _ _
ap_quotring_is_apartness.

QuotRing is a semigroup

We use + as the operation for this.

Lemma drplus_is_ext : bin_fun_strext quotring_as_CSetoid
quotring_as_CSetoid quotring_as_CSetoid (csg_op (c:=R)).
Proof.
red in |-*.
intros x1 x2 y1 y2.
simpl in |-*.
unfold ap_quotring in |-*.
intro X.
apply (coideal_plus R C (x1−x2) (y1−y2)); auto.
apply (coideal_wd R C ((x1+y1)[-](x2+y2)) ((x1−x2)[+](y1−y2))); auto.
astepr ((x1[+][--]x2)[+](y1[+][--]y2)).
astepr ((x1[+][--]x2)[+]y1[+][--]y2).
astepr (((x1[+][--]x2)[+]y1)[+][--]y2).
astepr ([--]y2[+]((x1[+][--]x2)[+]y1)).
astepr ([--]y2[+](x1[+][--]x2)[+]y1).
astepr ([--]y2[+]([--]x2+x1)[+]y1).
astepr (([--]y2[+][--]x2)[+]x1+y1).
astepr (([--]y2[+][--]x2)[+](x1+y1)).
astepr ((x1+y1)[+]([--]y2[+][--]x2)).
astepr ((x1+y1)[+][--](x2+y2)).
algebra.
Qed.

Definition drplus_is_bin_fun :=
Build_CSetoid_bin_fun quotring_as_CSetoid quotring_as_CSetoid
quotring_as_CSetoid (csg_op (c:=R)) drplus_is_ext.

Lemma drplus_is_assoc : associative drplus_is_bin_fun.
Proof.
red in |-*; auto.
intros x y z; simpl in |-*.
apply eq_quotring_wd; algebra.
Qed.

Definition quotring_as_CSemiGroup := Build_CSemiGroup quotring_as_CSetoid
drplus_is_bin_fun drplus_is_assoc.

QuotRing is a monoid

0:R will work as unit.

Lemma zero_as_rht_unit : is_rht_unit drplus_is_bin_fun 0.
Proof.
red in |-*; intro x.
simpl in |-*.
apply eq_quotring_wd; algebra.
Qed.

Lemma zero_as_lft_unit : is_lft_unit drplus_is_bin_fun 0.
Proof.
red in |-*; intro x; simpl in |-*.
apply eq_quotring_wd; algebra.
Qed.

Definition quotring_is_CMonoid := Build_is_CMonoid quotring_as_CSemiGroup
0 zero_as_rht_unit zero_as_lft_unit.

Definition quotring_as_CMonoid := Build_CMonoid quotring_as_CSemiGroup
0 quotring_is_CMonoid.

QuotRing is a group

The same function still works as inverse (i.e. minus).

Lemma drinv_is_ext : un_op_strext quotring_as_CSetoid (cg_inv (c:=R)).
Proof.
red in |-*.
red in |-*.
intros x y.
simpl in |-*.
unfold ap_quotring in |-*.
intro X.
cut (C (x−y) and C −1). intuition.
apply (coideal_mult R C (x−y) −1); algebra.
apply (coideal_wd R C ([--]1[*](x−y)) ((x−y)[*][--]1)); algebra.
apply (coideal_wd R C ([--]x[-][--]y) ([--]1[*](x−y))); algebra.
astepr ([--](x−y)).
astepr ([--](x[+][--]y)).
Step_final ([--]x[+][--][--]y).
Qed.

Definition drinv_is_un_op :=
Build_CSetoid_un_op quotring_as_CSetoid (cg_inv (c:=R)) drinv_is_ext.

Lemma drinv_is_inv : is_CGroup quotring_as_CMonoid drinv_is_un_op.
Proof.
red in |-*.
intro x.
simpl in |-*.
unfold is_inverse in |-*.
simpl in |-*.
split; apply eq_quotring_wd; algebra.
Qed.

Definition quotring_as_CGroup := Build_CGroup quotring_as_CMonoid
drinv_is_un_op drinv_is_inv.

QuotRing is an Abelian group

Lemma drplus_is_commutative : commutes drplus_is_bin_fun.
Proof.
red in |-*.
intros x y.
simpl in |-*.
apply eq_quotring_wd; algebra.
Qed.

Definition quotring_as_CAbGroup := Build_CAbGroup quotring_as_CGroup
drplus_is_commutative.

QuotRing is a ring

Multiplication from R still works as a multiplicative function, making quotring a ring.

Lemma drmult_is_ext : bin_fun_strext quotring_as_CAbGroup
quotring_as_CAbGroup quotring_as_CAbGroup (cr_mult (c:=R)).
Proof.
red in |-*.
intros x1 x2 y1 y2.
simpl in |-*.
unfold ap_quotring.
intro X.
cut (C ((x1[*](y1−y2)) + ((x1−x2)[*]y2))).
  intro.
  assert (C (x1[*](y1−y2)) or C ((x1−x2)[*]y2)); algebra.
  elim X1; intros.
   right. cut (C x1 and C (y1−y2)). intuition.
   apply coideal_mult; assumption.
  left. cut (C (x1−x2) and C y2). intuition.
  apply coideal_mult; assumption.
apply (coideal_wd R C (x1×y1 − x2×y2)); try assumption.
astepr (x1×y1 − x1×y2 + (x1−x2)[*]y2).
  astepr (x1×y1 − x1×y2 + x1×y2 − x2×y2).
   astepr (x1×y1 + [--](x1×y2) + x1×y2 + [--](x2×y2)).
   astepr ((x1×y1 + ([--](x1×y2) + x1×y2)) + [--](x2×y2)).
   astepr ((x1×y1 + 0) + [--](x2×y2)).
   Step_final (x1×y1 + [--](x2×y2)).
  astepl ((x1×y1 − x1×y2)[+](x1×y2)[+][--](x2×y2)).
  astepl ((x1×y1 − x1×y2)[+](x1×y2[+][--](x2×y2))).
  apply plus_resp_eq.
  apply eq_symmetric; apply (ring_distr2 R x1 x2 y2).
astepl ((x1−x2)[*]y2 + (x1×y1 − x1×y2)).
astepr ((x1−x2)[*]y2 + x1[*](y1−y2)).
apply plus_resp_eq.
apply eq_symmetric; apply (ring_distr1 R x1 y1 y2).
Qed.

Definition drmult_is_bin_op :=
Build_CSetoid_bin_op quotring_as_CAbGroup (cr_mult (c:=R)) drmult_is_ext.

Lemma drmult_associative : associative drmult_is_bin_op.
Proof.
red in |-*; simpl in |-*.
intros x y z; apply eq_quotring_wd.
algebra.
Qed.

Lemma drmult_monoid : is_CMonoid (Build_CSemiGroup quotring_as_CAbGroup
   drmult_is_bin_op drmult_associative) 1.
apply Build_is_CMonoid; red in |-*; intro x; simpl in |-*; apply eq_quotring_wd; algebra.
Qed.

Lemma drmult_commutes : commutes drmult_is_bin_op.
Proof.
red in |-*; simpl in |-*; intros x y; apply eq_quotring_wd; algebra.
Qed.

Lemma quotring_distr : distributive drmult_is_bin_op drplus_is_bin_fun.
Proof.
red in |-*; simpl in |-*; intros x y z.
apply eq_quotring_wd; algebra.
Qed.

Lemma quotring_nontriv : (1:quotring_as_CAbGroup) [#] (0:quotring_as_CAbGroup).
Proof.
simpl in |-*.
unfold ap_quotring.
apply (coideal_wd R C 1 (1−0)); algebra.
Qed.

Definition quotring_is_CRing := Build_is_CRing quotring_as_CAbGroup 1
drmult_is_bin_op drmult_associative drmult_monoid
drmult_commutes quotring_distr quotring_nontriv.

Definition quotring_as_CRing := Build_CRing quotring_as_CAbGroup
1 drmult_is_bin_op quotring_is_CRing.

End QuotRing.