Require Export monoid.
Require Export group.
Require Export ring.
Require cool.
Implicit Arguments On.
Modules |
Module Module.
Module r := Ring.
Export Misc.
Section Module.
Variable R : r.Ring.
Record Module_Data : Type := {
module_carrier :> Type;
add : module_carrier->module_carrier->module_carrier;
zero : module_carrier;
opp : module_carrier->module_carrier;
mul : R->module_carrier->module_carrier
}.
Implicits zero [1].
Record Module_Theory [A:Module_Data] : Prop := {
assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z);
commut : (x,y:A) (add x y)==(add y x);
zero_sx : (x:A) (add zero x)==x;
opp_sx : (x:A) (add (opp x) x)==x;
mul_assoc : (x,y:R; z:A) (mul x (mul y z))==(mul (r.mul x y) z);
one_sx : (x:A) (mul r.one x)==x;
distrib_dx : (x:R; y,z:A) (mul x (add y z))==(add (mul x y) (mul x z));
distrib_sx : (x,y:R; z:A) (mul (r.add x y) z)==(add (mul x z) (mul y z))
}.
Record Module : Type := {
module_data :> Module_Data;
module_theory :> (Module_Theory module_data)
}.
Definition Obj : Type := Module.
Coercion Module_of_Obj [x:Obj] : Module := x.
Record Morph_Theory [A,B:Obj; f:A->B] : Prop := {
morph_add : (x,y:A) (f (add x y))==(add (f x) (f y));
morph_opp : (x:A) (f (opp x))==(opp (f x));
morph_mul : (x:R; y:A) (f (mul x y))==(mul x (f y))
}.
Record Module_Morph [A,B:Obj] : Type := {
morph_data :> A->B;
morph_theory :> (Morph_Theory morph_data)
}.
Definition Morph := Module_Morph.
Lemma morph_extens : (A,B:Module; f,g:(Morph A B))
((x:A)(f x)==(g x)) -> f==g.
Proof.
NewDestruct f; NewDestruct g; Simpl; Intros.
Assert U : morph_data0 == morph_data1.
Apply nondep_extensionality; Assumption.
NewDestruct U.
Assert U : morph_theory0 == morph_theory1.
Apply proof_irrelevance.
NewDestruct U.
Reflexivity.
Qed.
Section morph_comp.
Variable A,B,C:Obj.
Variable f:(Morph B C); g:(Morph A B).
Local h [x:A] : C := (f (g x)).
Remark h_th : (Morph_Theory h).
Proof.
Unfold h; Split; Intros.
Rewrite (morph_add g).
Rewrite (morph_add f).
Reflexivity.
Rewrite (morph_opp g).
Rewrite (morph_opp f).
Reflexivity.
Rewrite (morph_mul g).
Rewrite (morph_mul f).
Reflexivity.
Qed.
Definition morph_comp : (Morph A C).
Proof.
Split with h;
Apply h_th.
Defined.
End morph_comp.
Definition morph_id [A:Obj] : (Morph A A).
Proof.
Intros.
Split with [x:A]x.
Abstract Split; Auto.
Defined.
Implicits morph_id [1].
Lemma morph_comp_assoc : (A,B,C,D:Obj)
(h:(Morph C D); g:(Morph B C); f:(Morph A B))
(morph_comp h (morph_comp g f))==(morph_comp (morph_comp h g) f).
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
Lemma morph_id_sx : (A,B:Obj; f:(Morph A B))
(morph_comp morph_id f)==f.
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
Lemma morph_id_dx : (A,B:Obj; f:(Morph A B))
(morph_comp f morph_id)==f.
Proof.
Intros; Apply morph_extens; Trivial.
Qed.
End Module.
End Module.
Category of modules |
Signature for a module with a single ring |
Module Type Coeff_Sig.
End Coeff_Sig.
Modules over a ring as a Coq functor |
Module Module_Cat [r:Coeff_Sig] <: Cat_Sig.
Definition Obj : Type := (Module.Obj r.R).
Definition Morph [A,B:Obj] : Type := (Module.Morph A B).
Section morph_comp.
Variable A,B,C:Obj.
Variable f:(Morph B C); g:(Morph A B).
Definition morph_comp : (Morph A C) :=
(Module.morph_comp f g).
End morph_comp.
Definition morph_id [A:Obj] : (Morph A A) :=
(!Module.morph_id r.R A).
Implicits morph_id [1].
Lemma morph_comp_assoc : (A,B,C,D:Obj)
(h:(Morph C D); g:(Morph B C); f:(Morph A B))
(morph_comp h (morph_comp g f))==(morph_comp (morph_comp h g) f).
Proof.
Unfold Obj Morph morph_comp morph_id.
Apply !Module.morph_comp_assoc.
Qed.
Lemma morph_id_sx : (A,B:Obj; f:(Morph A B))
(morph_comp morph_id f)==f.
Proof.
Unfold Obj Morph morph_comp morph_id.
Apply !Module.morph_id_sx.
Qed.
Lemma morph_id_dx : (A,B:Obj; f:(Morph A B))
(morph_comp f morph_id)==f.
Proof.
Unfold Obj Morph morph_comp morph_id.
Apply !Module.morph_id_dx.
Qed.
End Module_Cat.