CoRN.old.CQuotient_Modules

Require Export CModules.

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.
Proof.
red in |-*.
intro x.
unfold ap_quotmod in |-*.
assert (x−x≡0); algebra.
assert (Not ((cmpred A cm) 0)); algebra.
intro. apply H0.
apply (comod_wd A cm (x−x) 0); auto.
Qed.

Lemma ap_quotmod_symmetric : Csymmetric ap_quotmod.
Proof.
red in |-*.
intros x y.
unfold ap_quotmod.
intro X.
apply (comod_mult A cm (y−x) ([--]1)).
apply (comod_wd A cm (x−y) (rm_mu A −1 (y−x))); algebra.
astepr [--](y−x); try apply eq_symmetric; try apply muminus1.
astepl [--](y[+][--]x).
astepl ([--][--]x[+][--]y).
astepl (x[+][--]y).
algebra.
Qed.

Lemma ap_quotmod_cotransitive : cotransitive ap_quotmod.
Proof.
red in |-*.
intros x y; unfold ap_quotmod.
intros X z.
apply (comod_plus A cm (x−z) (z−y)).
apply (comod_wd A cm (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_quotmod (x y:A) := Not (cm(x−y)).

Lemma eq_quotmod_wd : ∀ (x y:A), x≡y → (eq_quotmod x y).
Proof.
intros x y X; auto.
red in |-*; intro X0.
assert ((cmpred A cm)(0)); algebra.
apply (comod_wd A cm (x−y) 0); algebra.
apply x_minus_x; auto.
apply (comod_nonzero A cm); assumption.
Qed.

Lemma ap_quotmod_tight : tight_apart eq_quotmod ap_quotmod.
Proof.
red in |-*.
intros x y; intuition.
Qed.

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.

QuotMod is a semigroup

We use + as the operation for this.

Lemma dmplus_is_ext : bin_fun_strext quotmod_as_CSetoid
quotmod_as_CSetoid quotmod_as_CSetoid (csg_op (c:=A)).
Proof.
red in |-*.
intros x1 x2 y1 y2.
simpl in |-*.
unfold ap_quotmod in |-*.
intro X.
apply (comod_plus A cm (x1−x2) (y1−y2)); auto.
apply (comod_wd A cm ((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 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.
Proof.
red in |-*; auto.
intros x y z; simpl in |-*.
apply eq_quotmod_wd; algebra.
Qed.

Definition quotmod_as_CSemiGroup := Build_CSemiGroup quotmod_as_CSetoid
dmplus_is_bin_fun dmplus_is_assoc.

QuotMod ia a monoid

0:A will work as unit.

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

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

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.

QuotMod is a group

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

Lemma dminv_is_ext : un_op_strext quotmod_as_CSetoid (cg_inv (c:=A)).
Proof.
red in |-*.
red in |-*.
intros x y.
simpl in |-*.
unfold ap_quotmod in |-*.
intro X.
apply (comod_mult A cm (x−y) −1); algebra.
apply (comod_wd A cm ([--]x[-][--]y) ([--]1['](x−y))); algebra.
astepr ([--](x−y)).
astepr ([--](x[+][--]y)).
astepr ([--]x[+][--][--]y).
algebra.
Qed.

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.
Proof.
red in |-*.
intro x.
simpl in |-*.
unfold is_inverse in |-*.
simpl in |-*.
split; apply eq_quotmod_wd; algebra.
Qed.

Definition quotmod_as_CGroup := Build_CGroup quotmod_as_CMonoid
dminv_is_un_op dminv_is_inv.

QuotMod is an Abelian group

Lemma dmplus_is_commutative : commutes dmplus_is_bin_fun.
Proof.
red in |-*.
intros x y.
simpl in |-*.
apply eq_quotmod_wd; algebra.
Qed.

Definition quotmod_as_CAbGroup := Build_CAbGroup quotmod_as_CGroup
dmplus_is_commutative.

QuotMod is an R-module

rm_mu A does the job.

Lemma dmmu_is_ext : bin_fun_strext R
quotmod_as_CAbGroup quotmod_as_CAbGroup (rm_mu A).
Proof.
red in |-*.
intros a1 a2 x1 x2.
simpl in |-*;simpl in |-*.
unfold ap_quotmod in |-*.
intro X.
cut (cm ( a1['](x1−x2) + (a1−a2)[']x2) ).
  intro.
  assert ( cm (a1['](x1−x2)) or cm ((a1−a2)[']x2) ).
   algebra.
  elim X1;intros.
   right.
   apply (comod_mult A cm (x1−x2) a1); assumption.
  left.
  cut ( (a1−a2)[']x2 [#] 0).
   intro X2; cut ((a1−a2)[#]0); algebra.
   apply (mu_axap0_aap0 R A (a1−a2) x2); assumption.
  apply (comod_apzero A cm); assumption.
apply (comod_wd A cm (a1.x1 − a2.x2) ); try assumption.
astepr ( a1['](x1[+][--]x2) + (a1−a2)[']x2).
astepr ((a1['](x1[+][--]x2))[+]((a1[+][--]a2)[']x2)).
astepr ((a1['](x1[+][--]x2))[+](a1.x2 + −a2.x2)).
astepr ((a1.x2 + −a2.x2) + (a1['](x1[+][--]x2))).
astepr (a1.x2 + −a2.x2 + (a1['](x1[+][--]x2))).
astepr ((a1.x2) + ([--]a2.x2) + (a1['](x1[+][--]x2))).
simpl in |-*.
astepr (a1.x2 + −a2.x2 + a1.x1 + a1['][--]x2); simpl in |-*.
  astepr ((a1.x2 + −a2.x2 + a1.x1) + a1['][--]x2); simpl in |-*.
  astepr ((a1.x2 + −a2.x2 + a1.x1) + [--](a1.x2)).
  astepr ([--](a1.x2) + (a1.x2 + −a2.x2 + a1.x1)).
  astepr ([--](a1.x2) + (a1.x2 + ([--]a2.x2 + a1.x1))).
  astepr (([--](a1.x2) + a1.x2) + ([--]a2.x2 + a1.x1)).
  astepr (0 + ([--]a2.x2 + a1.x1)).
  astepr ([--]a2.x2 + a1.x1).
  astepr (a1.x1 + −a2.x2).
  astepr (a1.x1 + [--](a2.x2)).
  Step_final (a1.x1 − a2.x2).
astepl ((a1.x2 + −a2.x2) + (a1.x1 + a1['][--]x2)).
apply plus_resp_eq; algebra.
Qed.

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.
Proof.
apply Build_is_RModule; intuition; simpl in |-*; apply eq_quotmod_wd; algebra.
Qed.

Definition quotmod_as_RModule := Build_RModule R quotmod_as_CAbGroup
dmmu_is_bin_fun quotmod_is_RModule.

End QuotMod.

Implicit Arguments quotmod_as_RModule [R].