CoRN.old.CModules

Require Export CRings.

Modules

Definition of the notion of an R-Module

Let R be a ring.

Section Module_Definition.

Variable R : CRing.

Record is_RModule (A : CAbGroup) (mu : CSetoid_bin_fun R A A) : Prop :=
  {rm_pl1 : ∀ (a:R)(x y:A), (mu a (x+y))[=]
            ((mu a x)[+](mu a y));
   rm_pl2 : ∀ (a b:R)(x:A), (mu (a+b) x)[=]
            ((mu a x)[+](mu b x));
   rm_mult: ∀ (a b:R)(x:A), (mu (a×b) x)[=]
            (mu a (mu b x));
   rm_one : ∀ x:A, (mu 1 x)[=]x}.

Record RModule : Type :=
  {rm_crr :> CAbGroup;
   rm_mu : CSetoid_bin_fun R rm_crr rm_crr;
   rm_proof: is_RModule rm_crr rm_mu}.

End Module_Definition.

Implicit Arguments is_RModule [R].
Implicit Arguments rm_crr [R].
Implicit Arguments rm_mu [R].
Implicit Arguments rm_pl1 [R].
Implicit Arguments rm_pl2 [R].
Implicit Arguments rm_mult[R].
Implicit Arguments rm_one [R].
Implicit Arguments rm_proof[R].

Notation "a ['] x" := (rm_mu _ a x) (at level 20, right associativity).

Let R be a ring, let A be an R-Module.

Lemmas on Modules

Section Module.

Variable R : CRing.

Axioms on Modules

Section Module_Axioms.

Variable A : RModule R.

Lemma RModule_is_RModule : is_RModule (rm_crr A) (rm_mu A).
Proof.
elim A; intuition.
Qed.

Lemma mu_plus1 :
∀ (a : R) (x y : A), a['](x+y) ≡ a.x + a.y.
Proof.
elim RModule_is_RModule; intuition.
Qed.

Lemma mu_plus2 :
∀ (a b : R) (x : A), (a+b) . x ≡ a.x + b.x.
Proof.
elim RModule_is_RModule; intuition.
Qed.

Lemma mu_mult :
∀ (a b : R) (x : A), (a×b)['] x ≡ a.b.x.
Proof.
elim RModule_is_RModule; intuition.
Qed.

Lemma mu_one : ∀ x : A, 1.x ≡ x.
Proof.
elim RModule_is_RModule; intuition.
Qed.

End Module_Axioms.

Hint Resolve mu_plus1 mu_plus2 mu_mult mu_one : algebra.

Facts on Modules

Section Module_Basics.

Variable A : RModule R.

Lemma mu_zerox : ∀ x : A, 0.x ≡ 0.
Proof.
intro x; apply eq_symmetric.
apply (cg_cancel_lft _ (0.x)); algebra.
astepl (0.x); algebra.
Qed.

Hint Resolve mu_zerox : algebra.

Lemma mu_minusonex : ∀ x:A, −1.x ≡ −x.
Proof.
intro x; apply (cg_cancel_rht A x ([--]1.x) −x).
astepr (0:A).
astepl ([--]1.x + 1.x).
astepl (([--]1+1)['] x).
astepl (0.x); algebra.
Qed.

Hint Resolve mu_minusonex : algebra.

Lemma mu_azero : ∀ a:R, a['](0:A) ≡ 0.
Proof.
intro a; apply (cg_cancel_rht A (a['](0:A))).
astepr (a['](0:A)).
astepl (a[']((0:A)[+](0:A))).
Step_final (a['](0:A)).
Qed.

Lemma mu_aminusx : ∀ (a:R)(x:A), a['][--]x ≡ − (a.x).
Proof.
intros a x; apply (cg_cancel_rht A (a.x)).
astepr (0:A).
astepl (a[']([--]x+x)).
astepl (a['](0:A)).
apply mu_azero.
Qed.

Lemma mu_minusax : ∀ (a:R)(x:A), −a.x ≡ − (a.x).
Proof.
intros a x; apply (cg_cancel_rht A (a.x)).
astepr (0:A).
astepl (([--]a+a)[']x).
astepl ((0:R)[']x).
apply mu_zerox.
Qed.

Hint Resolve mu_azero mu_aminusx mu_minusax: algebra.

Lemma mu_axap0_aap0 : ∀ (a:R)(x:A), a.x [#] (0:A) → a [#] (0:R).
Proof.
intros a x X; apply (cg_ap_cancel_rht R a (0:R) a).
astepr a.
cut (a+a[#]a or x[#]x); intuition.
  assert False; try apply (ap_irreflexive_unfolded A x); try assumption.
  elim H.
apply mu_strext.
astepl ((a.x)[+](a.x)).
astepr ((0:A)[+](a.x)).
apply op_rht_resp_ap; assumption.
Qed.

Lemma mu_axap0_xap0 : ∀ (a:R)(x:A), a.x [#] (0:A) → x [#] (0:A).
Proof.
intros a x X; apply (cg_ap_cancel_rht A x (0:A) x).
astepr x.
cut (a[#]a or x+x[#]x); intuition.
  assert False; try apply (ap_irreflexive_unfolded R a); try assumption.
  elim H.
apply mu_strext.
astepl ((a.x)[+](a.x)).
astepr ((0:A)[+](a.x)).
apply op_rht_resp_ap; assumption.
Qed.

Hint Resolve mu_strext mu_axap0_aap0 mu_axap0_xap0 : algebra.

End Module_Basics.

Rings are Modules

Section Rings.

Lemma R_is_RModule : is_RModule R cr_mult.
Proof.
apply Build_is_RModule; intuition.
Qed.

Definition R_as_RModule := Build_RModule R R cr_mult R_is_RModule.

End Rings.

Definition of sub- and comodules

Section CoSubModules.

Variable A : RModule R.

Record is_submod (subP : wd_pred A) : CProp :=
  {smzero : subP 0;
   smplus : ∀ x y:A, subP x and subP y → subP (x+y);
   smmult : ∀ (x:A)(a:R), subP x → subP(a.x)}.

Record submod : Type :=
  {smpred :> wd_pred A;
   smproof: is_submod smpred}.

Record is_comod (coP : wd_pred A) : CProp :=
  {cmapzero : ∀ x:A, coP x → x[#]0;
   cmplus : ∀ x y:A, coP (x+y) → coP x or coP y;
   cmmult : ∀ (x:A)(a:R), coP (a.x) → coP x}.

Record comod : Type :=
  {cmpred :> wd_pred A;
   cmproof: is_comod cmpred}.

End CoSubModules.

Implicit Arguments is_submod [A].
Implicit Arguments is_comod [A].

Axioms on sub- and comodules

Let sm be a submodule, let cm be a comodule.

Section CoSubModule_Axioms.

Variable A : RModule R.
Variable sm : submod A.
Variable cm : comod A.

Lemma submod_is_submod : is_submod sm.
Proof.
elim sm; auto.
Qed.

Lemma comod_is_comod : is_comod cm.
Proof.
elim cm; auto.
Qed.

Lemma comod_apzero : ∀ x:A, cm x → x[#]0.
Proof.
elim cm. intuition elim cmproof0.
Qed.

Lemma comod_nonzero : Not (cm 0).
Proof.
intro.
cut ((0:A)[#](0:A)); try apply comod_apzero; try assumption.
apply ap_irreflexive.
Qed.

Lemma comod_plus : ∀ x y:A, cm (x+y) → cm x or cm y.
Proof.
elim cm. intuition elim cmproof0.
Qed.

Lemma comod_mult : ∀ (x:A)(a:R), cm (a.x) → cm x.
Proof.
elim cm. intuition elim cmproof0.
Qed.

Lemma comod_wd : ∀ x y:A, x≡y → cm x → cm y.
Proof.
elim cm.
simpl in |-*.
intro.
elim cmpred0.
intros.
apply (wdp_well_def x y); auto.
Qed.

End CoSubModule_Axioms.

End Module.

Implicit Arguments comod_plus [R].
Implicit Arguments comod_mult [R].
Implicit Arguments comod_wd [R].
Implicit Arguments comod_apzero [R].
Implicit Arguments comod_nonzero [R].
Implicit Arguments is_submod [R].
Implicit Arguments submod [R].
Implicit Arguments is_comod [R].
Implicit Arguments comod [R].
Implicit Arguments cmpred [R].
Implicit Arguments cmproof [R].

Hint Resolve mu_plus1 mu_plus2 mu_mult mu_one : algebra.
Hint Resolve mu0help mu0help2 mu_zerox mu_minusonex: algebra.
Hint Resolve mu_azero mu_aminusx mu_minusax: algebra.
Hint Resolve mu_strext mu_axap0_aap0 mu_axap0_xap0 : algebra.
Hint Resolve comod_apzero comod_nonzero : algebra.
Hint Resolve comod_plus comod_mult comod_wd : algebra.