(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Ring_cat.
Require Export Operation_of_monoid.
(** Title "The category of modules on a ring." *)
Section Def.
Variable R : RING.
Section Module_def.
Variable Mod : abelian_group.
Variable op : operation (ring_monoid R) Mod.

Definition op_lin_left :=
  forall (a b : R) (x : Mod),
  Equal (op (sgroup_law R a b) x) (sgroup_law Mod (op a x) (op b x)).

Definition op_lin_right :=
  forall (a : R) (x y : Mod),
  Equal (op a (sgroup_law Mod x y)) (sgroup_law Mod (op a x) (op a y)).
End Module_def.

Record module_on (M : abelian_group) : Type := 
  {module_op : operation (ring_monoid R) M;
   module_op_lin_left_prf : op_lin_left module_op;
   module_op_lin_right_prf : op_lin_right module_op}.

Record module : Type := 
  {module_carrier :> abelian_group;
   module_on_def :> module_on module_carrier}.
Coercion Build_module : module_on >-> module.

Definition module_mult (B : module) (a : R) (x : B) := module_op B a x.
Section Hom.
Variable E F : module.

Definition module_hom_prop (f : E -> F) :=
  forall (a : R) (x : E), Equal (f (module_mult a x)) (module_mult a (f x)).

Record module_hom : Type := 
  {module_monoid_hom :> monoid_hom E F;
   module_hom_prf : module_hom_prop module_monoid_hom}.
End Hom.

Definition module_hom_comp :
  forall E F Mod : module,
  module_hom F Mod -> module_hom E F -> module_hom E Mod.
(* Goal: forall (E F Mod : module) (_ : module_hom F Mod) (_ : module_hom E F), module_hom E Mod *)
intros E F Mod g f; try assumption.
apply
 (Build_module_hom (E:=E) (F:=Mod) (module_monoid_hom:=monoid_hom_comp g f)).
(* Goal: @module_hom_prop E Mod (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier Mod))) (@monoid_hom_comp (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g) (@module_monoid_hom E F f))))) *)
unfold module_hom_prop in |- *; auto with algebra.
(* Goal: forall (a b c : module) (g : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) b c)) (f : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) a b)), @Equal (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier c)) (module_hom a c) (@module_monoid_hom a c)) (@module_hom_comp a b c g f)) (@comp_hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier b) (module_carrier c)) (module_hom b c) (@module_monoid_hom b c)) g) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier b)) (module_hom a b) (@module_monoid_hom a b)) f)) *)
simpl in |- *.
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@comp_map_fun (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) (@module_mult E a x)) (@module_mult Mod a (@comp_map_fun (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x)) *)
unfold comp_map_fun in |- *.
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) (@module_mult E a x))) (@module_mult Mod a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x))) *)
intros a x; try assumption.
apply
 Trans
  with
    (Ap (sgroup_map (monoid_sgroup_hom (module_monoid_hom g)))
       (module_mult a
          (Ap (sgroup_map (monoid_sgroup_hom (module_monoid_hom f))) x))).
cut
 (Equal
    (Ap (sgroup_map (monoid_sgroup_hom (module_monoid_hom f)))
       (module_mult a x))
    (module_mult a
       (Ap (sgroup_map (monoid_sgroup_hom (module_monoid_hom f))) x))).
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) (@module_mult E a x)) (@module_mult F a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@module_mult F a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x))) (@module_mult Mod a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x))) *)
apply (module_hom_prf f).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@module_mult F a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x))) (@module_mult Mod a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier Mod)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier F))) (group_monoid (abelian_group_group (module_carrier Mod))) (@module_monoid_hom F Mod g))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier E)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier F)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier E))) (group_monoid (abelian_group_group (module_carrier F))) (@module_monoid_hom E F f))) x))) *)
apply (module_hom_prf g).
Defined.

Definition module_id : forall E : module, module_hom E E.
(* Goal: forall E : module, module_hom E E *)
intros E; try assumption.
(* Goal: module_hom E E *)
apply (Build_module_hom (module_monoid_hom:=monoid_id E)).
(* Goal: @Map_eq (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) *)
simpl in |- *; auto with algebra.
Defined.

Definition MODULE : category.
apply
 (subcat (C:=MONOID) (C':=module) (i:=module_carrier)
    (homC':=fun E F : module =>
            Build_subtype_image (E:=Hom (c:=ABELIAN_GROUP) E F)
              (subtype_image_carrier:=module_hom E F)
              (module_monoid_hom (E:=E) (F:=F))) (CompC':=module_hom_comp)
    (idC':=module_id)).
(* Goal: forall (a b c : module) (g : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) b c)) (f : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) a b)), @Equal (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier c)) (module_hom a c) (@module_monoid_hom a c)) (@module_hom_comp a b c g f)) (@comp_hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier b) (module_carrier c)) (module_hom b c) (@module_monoid_hom b c)) g) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier b)) (module_hom a b) (@module_monoid_hom a b)) f)) *)
simpl in |- *.
(* Goal: forall a : module, @Map_eq (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (Id (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))))) (Id (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))))) *)
(* Goal: forall (a b c : module) (g : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) b c)) (f : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) a b)), @Equal (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier c)) (module_hom a c) (@module_monoid_hom a c)) (@module_hom_comp a b c g f)) (@comp_hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier b) (module_carrier c)) (module_hom b c) (@module_monoid_hom b c)) g) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier b)) (module_hom a b) (@module_monoid_hom a b)) f)) *)
intros a; try assumption.
(* Goal: @Map_eq (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) *)
auto with algebra.
(* Goal: forall (a b c : module) (g : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) b c)) (f : Carrier (@subcat_Hom MONOID module (fun m : module => group_monoid (abelian_group_group (module_carrier m))) (fun E F : module => @Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier E) (module_carrier F)) (module_hom E F) (@module_monoid_hom E F)) a b)), @Equal (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier c)) (module_hom a c) (@module_monoid_hom a c)) (@module_hom_comp a b c g f)) (@comp_hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier b) (module_carrier c)) (module_hom b c) (@module_monoid_hom b c)) g) (@subtype_image_inj (@Hom MONOID (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b)))) (@Build_subtype_image (@Hom ABELIAN_GROUP (module_carrier a) (module_carrier b)) (module_hom a b) (@module_monoid_hom a b)) f)) *)
simpl in |- *.
(* Goal: forall (a b c : module) (g : module_hom b c) (f : module_hom a b), @Map_eq (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) *)
intros a b c g f; try assumption.
(* Goal: @Map_eq (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) *)
red in |- *.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@comp_map_map (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier c)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier b))) (group_monoid (abelian_group_group (module_carrier c))) (@module_monoid_hom b c g))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (module_carrier a)))) (monoid_sgroup (group_monoid (abelian_group_group (module_carrier b)))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (module_carrier a))) (group_monoid (abelian_group_group (module_carrier b))) (@module_monoid_hom a b f)))) x) *)
auto with algebra.
Defined.
End Def.