Quotient Modules
Let R be a ring, A an R-Module and cm a comodule of A. We will prove that A / ~cm is a module, called QuotMod.QuotMod is a setoid
To achieve this we define a new apartness on the elements of A.Section QuotMod.
Variable R : CRing.
Variable A :RModule R.
Variable cm: comod A.
Definition ap_quotmod (x y:A) := cm(x[-]y).
Lemma ap_quotmod_irreflexive : irreflexive ap_quotmod.
Lemma ap_quotmod_symmetric : Csymmetric ap_quotmod.
Lemma ap_quotmod_cotransitive : cotransitive ap_quotmod.
We take `not apart' as the new equality.
Definition eq_quotmod (x y:A) := ~ (cm(x[-]y)).
Lemma eq_quotmod_wd : forall (x y:A), x[=]y -> (eq_quotmod x y).
Lemma ap_quotmod_tight : tight_apart eq_quotmod ap_quotmod.
Definition ap_quotmod_is_apartness :=
Build_is_CSetoid A eq_quotmod ap_quotmod
ap_quotmod_irreflexive
ap_quotmod_symmetric
ap_quotmod_cotransitive
ap_quotmod_tight.
Definition quotmod_as_CSetoid := Build_CSetoid _ _ _
ap_quotmod_is_apartness.
Lemma dmplus_is_ext : bin_fun_strext quotmod_as_CSetoid
quotmod_as_CSetoid quotmod_as_CSetoid (csg_op (c:=A)).
Definition dmplus_is_bin_fun :=
Build_CSetoid_bin_fun quotmod_as_CSetoid quotmod_as_CSetoid
quotmod_as_CSetoid (csg_op (c:=A)) dmplus_is_ext.
Lemma dmplus_is_assoc : associative dmplus_is_bin_fun.
Definition quotmod_as_CSemiGroup := Build_CSemiGroup quotmod_as_CSetoid
dmplus_is_bin_fun dmplus_is_assoc.
Lemma zero_as_rht_unit : is_rht_unit dmplus_is_bin_fun 0.
Lemma zero_as_lft_unit : is_lft_unit dmplus_is_bin_fun 0.
Definition quotmod_is_CMonoid := Build_is_CMonoid quotmod_as_CSemiGroup
0 zero_as_rht_unit zero_as_lft_unit.
Definition quotmod_as_CMonoid := Build_CMonoid quotmod_as_CSemiGroup
0 quotmod_is_CMonoid.
Lemma dminv_is_ext : un_op_strext quotmod_as_CSetoid (cg_inv (c:=A)).
Definition dminv_is_un_op :=
Build_CSetoid_un_op quotmod_as_CSetoid (cg_inv (c:=A)) dminv_is_ext.
Lemma dminv_is_inv : is_CGroup quotmod_as_CMonoid dminv_is_un_op.
Definition quotmod_as_CGroup := Build_CGroup quotmod_as_CMonoid
dminv_is_un_op dminv_is_inv.
Lemma dmplus_is_commutative : commutes dmplus_is_bin_fun.
Definition quotmod_as_CAbGroup := Build_CAbGroup quotmod_as_CGroup
dmplus_is_commutative.
Lemma dmmu_is_ext : bin_fun_strext R
quotmod_as_CAbGroup quotmod_as_CAbGroup (rm_mu A).
Definition dmmu_is_bin_fun :=
Build_CSetoid_bin_fun R quotmod_as_CAbGroup
quotmod_as_CAbGroup (rm_mu A) dmmu_is_ext.
Lemma quotmod_is_RModule : is_RModule quotmod_as_CAbGroup
dmmu_is_bin_fun.
Definition quotmod_as_RModule := Build_RModule R quotmod_as_CAbGroup
dmmu_is_bin_fun quotmod_is_RModule.
End QuotMod.