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.
Lemma ap_quotring_symmetric : Csymmetric ap_quotring.
Lemma ap_quotring_cotransitive : cotransitive ap_quotring.
We take `not apart' as the new equality.
Definition eq_quotring (x y:R) := ~ (C(x[-]y)).
Lemma eq_quotring_wd : forall (x y:R), x[=]y -> (eq_quotring x y).
Lemma ap_quotring_tight : tight_apart eq_quotring ap_quotring.
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.
Lemma drplus_is_ext : bin_fun_strext quotring_as_CSetoid
quotring_as_CSetoid quotring_as_CSetoid (csg_op (c:=R)).
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.
Definition quotring_as_CSemiGroup := Build_CSemiGroup quotring_as_CSetoid
drplus_is_bin_fun drplus_is_assoc.
Lemma zero_as_rht_unit : is_rht_unit drplus_is_bin_fun 0.
Lemma zero_as_lft_unit : is_lft_unit drplus_is_bin_fun 0.
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.
Lemma drinv_is_ext : un_op_strext quotring_as_CSetoid (cg_inv (c:=R)).
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.
Definition quotring_as_CGroup := Build_CGroup quotring_as_CMonoid
drinv_is_un_op drinv_is_inv.
Lemma drplus_is_commutative : commutes drplus_is_bin_fun.
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)).
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.
Lemma drmult_monoid : is_CMonoid (Build_CSemiGroup quotring_as_CAbGroup
drmult_is_bin_op drmult_associative) 1.
Lemma drmult_commutes : commutes drmult_is_bin_op.
Lemma quotring_distr : distributive drmult_is_bin_op drplus_is_bin_fun.
Lemma quotring_nontriv : (1:quotring_as_CAbGroup) [#] (0:quotring_as_CAbGroup).
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.