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 : forall (a:R)(x y:A), (mu a (x[+]y))[=]
            ((mu a x)[+](mu a y));
   rm_pl2 : forall (a b:R)(x:A), (mu (a[+]b) x)[=]
            ((mu a x)[+](mu b x));
   rm_mult: forall (a b:R)(x:A), (mu (a[*]b) x)[=]
            (mu a (mu b x));
   rm_one : forall 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.

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).

Lemma mu_plus1 :
forall (a : R) (x y : A), a['](x[+]y) [=] a[']x [+] a[']y.

Lemma mu_plus2 :
forall (a b : R) (x : A), (a[+]b) ['] x [=] a[']x [+] b[']x.

Lemma mu_mult :
forall (a b : R) (x : A), (a[*]b)['] x [=] a[']b[']x.

Lemma mu_one : forall x : A, 1[']x [=] x.

End Module_Axioms.

Facts on Modules

Section Module_Basics.

Variable A : RModule R.

Lemma mu_zerox : forall x : A, 0[']x [=] 0.

Lemma mu_minusonex : forall x:A, [--]1[']x [=] [--]x.

Lemma mu_azero : forall a:R, a['](0:A) [=] 0.

Lemma mu_aminusx : forall (a:R)(x:A), a['][--]x [=] [--] (a[']x).

Lemma mu_minusax : forall (a:R)(x:A), [--]a[']x [=] [--] (a[']x).

Lemma mu_axap0_aap0 : forall (a:R)(x:A), a[']x [#] (0:A) -> a [#] (0:R).

Lemma mu_axap0_xap0 : forall (a:R)(x:A), a[']x [#] (0:A) -> x [#] (0:A).

End Module_Basics.

Rings are Modules

Section Rings.

Lemma R_is_RModule : is_RModule R cr_mult.

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 : forall x y:A, subP x and subP y -> subP (x[+]y);
   smmult : forall (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 : forall x:A, coP x -> x[#]0;
   cmplus : forall x y:A, coP (x[+]y) -> coP x or coP y;
   cmmult : forall (x:A)(a:R), coP (a[']x) -> coP x}.

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

End CoSubModules.

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.

Lemma comod_is_comod : is_comod cm.

Lemma comod_apzero : forall x:A, cm x -> x[#]0.

Lemma comod_nonzero : ~ (cm 0).

Lemma comod_plus : forall x y:A, cm (x[+]y) -> cm x or cm y.

Lemma comod_mult : forall (x:A)(a:R), cm (a[']x) -> cm x.

Lemma comod_wd : forall x y:A, x[=]y -> cm x -> cm y.

End CoSubModule_Axioms.

End Module.