(** Authors Anthony Bordg and Floris van Doorn, February-December 2017 *) Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. (** ** Contents - The ring of endomorphisms of an abelian group - Modules (the definition of the small type of R-modules over a ring R) - R-module morphisms - Linearity - [modulefun] - R-module homomorphisms form an R-module - Isomorphisms ([moduleiso]) *) Local Open Scope addmonoid_scope. Import UniMath.Algebra.Monoids.AddNotation. (** ** The ring of endomorphisms of an abelian group *) (** Two binary operations on the set of endomorphisms of an abelian group *) Definition monoidfun_to_isbinopfun {G : abgr} (f : monoidfun G G) : isbinopfun f := pr1 (pr2 f). Definition ringofendabgr_op1 {G: abgr} : binop (monoidfun G G). Proof. intros f g. apply (@monoidfunconstr _ _ (λ x : G, f x + g x)). apply tpair. - intros x x'. rewrite (monoidfun_to_isbinopfun f). rewrite (monoidfun_to_isbinopfun g). apply (abmonoidrer G). - rewrite (monoidfununel f). rewrite (monoidfununel g). rewrite (lunax G). reflexivity. Defined. Definition ringofendabgr_op2 {G : abgr} : binop (monoidfun G G). Proof. intros f g. apply (monoidfuncomp g f). Defined. Declare Scope abgr_scope. Notation "f + g" := (ringofendabgr_op1 f g) : abgr_scope. (** The underlying set of the ring of endomorphisms of an abelian group *) Definition setofendabgr (G : abgr) : hSet := make_hSet (monoidfun G G) (isasetmonoidfun G G). (** A few access functions *) Definition pr1setofendabgr {G : abgr} (f : setofendabgr G) : G -> G := pr1 f. Definition pr2setofendabgr {G : abgr} (f : setofendabgr G) : ismonoidfun (pr1 f) := pr2 f. Definition setofendabgr_to_isbinopfun {G : abgr} (f : setofendabgr G) : isbinopfun (pr1setofendabgr f) := pr1 (pr2 f). Definition setofendabgr_to_unel {G : abgr} (f : setofendabgr G) : pr1setofendabgr f 0 = 0 := pr2 (pr2setofendabgr f). (** We endow setofendabgr with the two binary operations defined above *) Definition setwith2binopofendabgr (G : abgr) : setwith2binop := make_setwith2binop (setofendabgr G) (make_dirprod (ringofendabgr_op1) (ringofendabgr_op2)). (** ringofendabgr_op1 G and ringofendabgr_op2 G are ring operations *) (** ringofendabgr_op1 is a monoid operation *) Local Open Scope abgr_scope. Lemma isassoc_ringofendabgr_op1 {G : abgr} : isassoc (@ringofendabgr_op1 G). Proof. intros f g h. use total2_paths_f. - apply funextfun. intro. apply (pr2 G). - apply isapropismonoidfun. Defined. Lemma setofendabgr_un0 {G: abgr} : monoidfun G G. Proof. apply (@monoidfunconstr _ _ (λ x : G, 0)). apply make_dirprod. - intros x x'. rewrite (lunax G). reflexivity. - reflexivity. Defined. Lemma islunit_setofendabgr_un0 {G : abgr} : islunit (@ringofendabgr_op1 G) setofendabgr_un0. Proof. intro f. use total2_paths_f. - apply funextfun. intro x. apply (lunax G (pr1setofendabgr f x)). - apply isapropismonoidfun. Defined. Lemma isrunit_setofendabgr_un0 {G : abgr} : isrunit (@ringofendabgr_op1 G) setofendabgr_un0. Proof. intros f. use total2_paths_f. - apply funextfun. intro x. apply (runax G (pr1setofendabgr f x)). - apply isapropismonoidfun. Defined. Lemma isunit_setofendabgr_un0 {G : abgr} : isunit (@ringofendabgr_op1 G) setofendabgr_un0. Proof. exact (make_isunit islunit_setofendabgr_un0 isrunit_setofendabgr_un0). Defined. Lemma isunital_ringofendabgr_op1 {G : abgr} : isunital (@ringofendabgr_op1 G). Proof. exact (make_isunital setofendabgr_un0 isunit_setofendabgr_un0). Defined. Lemma ismonoidop_ringofendabgr_op1 {G : abgr} : ismonoidop (@ringofendabgr_op1 G). Proof. exact (make_ismonoidop isassoc_ringofendabgr_op1 isunital_ringofendabgr_op1). Defined. Local Close Scope abgr_scope. (** ringofendabgr_op1 is a group operation *) Definition setofendabgr_inv {G : abgr} : monoidfun G G -> monoidfun G G. Proof. intro f. apply (@monoidfunconstr G G (λ x : G, grinv G (pr1setofendabgr f x))). apply make_dirprod. - intros x x'. rewrite (setofendabgr_to_isbinopfun f). rewrite (grinvop G). apply (commax G). - rewrite (setofendabgr_to_unel f). apply (grinvunel G). Defined. Local Open Scope abgr_scope. Lemma islinv_setofendabgr_inv {G : abgr} : islinv (@ringofendabgr_op1 G) (unel_is (@ismonoidop_ringofendabgr_op1 G)) setofendabgr_inv. Proof. intro f. use total2_paths_f. - apply funextfun. intro x. apply (grlinvax G). - apply isapropismonoidfun. Defined. Lemma isrinv_setofendabgr_inv {G : abgr} : isrinv (@ringofendabgr_op1 G) (unel_is (@ismonoidop_ringofendabgr_op1 G)) setofendabgr_inv. Proof. intro f. use total2_paths_f. - apply funextfun. intro x. apply (grrinvax G). - apply isapropismonoidfun. Defined. Lemma isinv_setofendabgr_inv {G : abgr} : isinv (@ringofendabgr_op1 G) (unel_is (@ismonoidop_ringofendabgr_op1 G)) setofendabgr_inv. Proof. exact (make_isinv islinv_setofendabgr_inv isrinv_setofendabgr_inv). Defined. Definition invstruct_setofendabgr_inv {G : abgr} : invstruct (@ringofendabgr_op1 G) ismonoidop_ringofendabgr_op1. Proof. exact (make_invstruct (@setofendabgr_inv G) (@isinv_setofendabgr_inv G)). Defined. Lemma isgrop_ringofendabgr_op1 {G : abgr} : isgrop (@ringofendabgr_op1 G). Proof. exact (make_isgrop ismonoidop_ringofendabgr_op1 invstruct_setofendabgr_inv). Defined. Lemma iscomm_ringofendabgr_op1 {G : abgr} : iscomm (@ringofendabgr_op1 G). Proof. intros f g. use total2_paths_f. - apply funextfun. intro x. apply (commax G). - apply (isapropismonoidfun). Defined. Lemma isabgrop_ringofendabgr_op1 {G : abgr} : isabgrop (@ringofendabgr_op1 G). Proof. exact (make_isabgrop isgrop_ringofendabgr_op1 iscomm_ringofendabgr_op1). Defined. (** ringofendabgr_op2 is a monoid operation *) Lemma isassoc_ringofendabgr_op2 {G : abgr} : isassoc (@ringofendabgr_op2 G). Proof. intros f g h. use total2_paths_f. - apply funcomp_assoc. - apply isapropismonoidfun. Defined. Definition setofendabgr_un1 {G: abgr} : monoidfun G G. Proof. apply (@monoidfunconstr _ _ (idfun G)). apply make_dirprod. - intros x x'. reflexivity. - reflexivity. Defined. Lemma islunit_setofendabgr_un1 {G : abgr} : islunit (@ringofendabgr_op2 G) setofendabgr_un1. Proof. intro f. use total2_paths_f. - apply funextfun. intro x. reflexivity. - apply isapropismonoidfun. Defined. Lemma isrunit_setofendabgr_un1 {G : abgr} : isrunit (@ringofendabgr_op2 G) setofendabgr_un1. Proof. intros f. use total2_paths_f. - apply funextfun. intro x. reflexivity. - apply isapropismonoidfun. Defined. Lemma isunit_setofendabgr_un1 {G : abgr} : isunit (@ringofendabgr_op2 G) setofendabgr_un1. Proof. exact (make_isunit islunit_setofendabgr_un1 isrunit_setofendabgr_un1). Defined. Lemma isunital_ringofendabgr_op2 {G : abgr} : isunital (@ringofendabgr_op2 G). Proof. exact (make_isunital setofendabgr_un1 isunit_setofendabgr_un1). Defined. Lemma ismonoidop_ringofendabgr_op2 {G : abgr} : ismonoidop (@ringofendabgr_op2 G). Proof. exact (make_ismonoidop isassoc_ringofendabgr_op2 isunital_ringofendabgr_op2). Defined. (** ringofendabgr_op2 is distributive over ringofendabgr_op1 *) Lemma isldistr_setofendabgr_op {G : abgr} : isldistr (@ringofendabgr_op1 G) (@ringofendabgr_op2 G). Proof. intros f g h. use total2_paths_f. - apply funextfun. intro x. apply (setofendabgr_to_isbinopfun h). - apply isapropismonoidfun. Defined. Lemma isrdistr_setofendabgr_op {G : abgr} : isrdistr (@ringofendabgr_op1 G) (@ringofendabgr_op2 G). Proof. intros f g h. use total2_paths_f. - apply funextfun. intro x. reflexivity. - apply isapropismonoidfun. Defined. Lemma isdistr_setofendabgr_op {G : abgr} : isdistr (@ringofendabgr_op1 G) (@ringofendabgr_op2 G). Proof. exact (make_dirprod isldistr_setofendabgr_op isrdistr_setofendabgr_op). Defined. Lemma isringops_setofendabgr_op {G : abgr} : isringops (@ringofendabgr_op1 G) (@ringofendabgr_op2 G). Proof. exact (make_isringops isabgrop_ringofendabgr_op1 ismonoidop_ringofendabgr_op2 isdistr_setofendabgr_op). Defined. (** The set of endomorphisms of an abelian group is a ring *) Definition ringofendabgr (G : abgr) : ring := @make_ring (setwith2binopofendabgr G) (@isringops_setofendabgr_op G). (** ** Modules: the definition of the small type of R-modules over a ring R *) (** A module over R may be defined as a ring homomorphism from R to the ring of endomorphisms of an Abelian group (in other words, a ring action on the abelian group). An equivalence with the more common axiomatic definition is established below. In this development, we concern ourselves with left modules. Recall that a right module is equivalent to a left module over the opposite ring. *) Definition module_struct (R : ring) (G : abgr) : UU := ringfun R (ringofendabgr G). Definition module (R : ring) : UU := ∑ G, module_struct R G. Definition pr1module {R : ring} (M : module R) : abgr := pr1 M. Coercion pr1module : module >-> abgr. Definition pr2module {R : ring} (M : module R) : module_struct R (pr1module M) := pr2 M. Identity Coercion id_module_struct : module_struct >-> ringfun. Definition make_module {R : ring} (G : abgr) (f : module_struct R G) : module R := tpair _ G f. Lemma isasetmodule {R : ring} (M : module R) : isaset M. Proof. exact (pr2 (pr1 (pr1 (pr1 M)))). Defined. (** The ring action gives rise to a notion of multiplication. *) Definition module_mult {R : ring} (M : module R) : R -> M -> M := λ r : R, λ x : M, (pr1setofendabgr (pr2module M r) x). Declare Scope module_scope. Notation "r * x" := (module_mult _ r x) : module_scope. Delimit Scope module_scope with module. Local Open Scope module. Lemma module_mult_0_to_0 {R : ring} {M : module R} (x : M) : ringunel1 * x = @unel M. Proof. unfold module_mult. cbn. assert (pr2module M ringunel1 = @ringunel1 (ringofendabgr M)). - exact (rigfun_to_unel_rigaddmonoid (pr2module M)). - rewrite X. reflexivity. Defined. Local Open Scope addmonoid. Lemma module_mult_is_ldistr {R : ring} {M : module R} (r : R) (x y : M) : r * (x + y) = r * x + r * y. Proof. exact (pr1 (pr2 (pr2module M r)) x y). Defined. Lemma module_mult_is_rdistr {R : ring} {M : module R} (r s : R) (x : M) : (op1 r s) * x = r * x + s * x. Proof. exact (maponpaths (λ r, pr1setofendabgr r x) (pr1 (pr1 (pr2 (pr2module M))) r s)). Defined. Lemma module_mult_assoc {R : ring} {M : module R} (r s : R) (x : M) : (op2 r s) * x = r * (s * x). Proof. exact (maponpaths (λ r, pr1setofendabgr r x) (pr1 (pr2 (pr2 (pr2module M))) r s)). Defined. Lemma module_mult_1 {R : ring} {M : module R} (r : R) : r * unel M = unel M. Proof. exact (pr2 (pr2 (pr2module M r))). Defined. Lemma module_mult_unel2 {R : ring} {M : module R} (m : M) : ringunel2 * m = m. Proof. exact (maponpaths (λ r, pr1setofendabgr r m) (pr2 (pr2 (pr2 (pr2module M))))). Defined. Lemma module_inv_mult {R : ring} {M : module R} (r : R) (x : M) : @grinv _ (r * x) = r * @grinv _ x. Proof. apply grinv_path_from_op_path. now rewrite <- module_mult_is_ldistr, grrinvax, module_mult_1. Defined. Lemma module_mult_neg1 {R : ring} {M : module R} (x : M) : ringminus1 * x = @grinv _ x. Proof. apply pathsinv0. apply grinv_path_from_op_path. refine (maponpaths (λ y, y * ((_ * x)%module))%multmonoid (!(module_mult_unel2 x)) @ _). now rewrite <- module_mult_is_rdistr, ringrinvax1, module_mult_0_to_0. Defined. Lemma module_inv_mult_to_inv1 {R : ring} {M : module R} (r : R) (x : M) : @grinv _ (r * x) = ringinv1 r * x. Proof. apply grinv_path_from_op_path. now rewrite <- module_mult_is_rdistr, ringrinvax1, module_mult_0_to_0. Defined. Lemma module_mult_inv_to_inv1 {R : ring} {M : module R} (r : R) (x : M) : r * @grinv _ x = ringinv1 r * x. Proof. now rewrite <- module_inv_mult_to_inv1, module_inv_mult. Defined. (** To construct a module from a left action satisfying four axioms *) Definition mult_isldistr_wrt_grop {R : ring} {G : abgr} (m : R -> G -> G) : UU := ∏ r : R, ∏ x y : G, m r (x + y) = (m r x) + (m r y). Definition mult_isrdistr_wrt_ringop1 {R : ring} {G : abgr} (m : R -> G -> G) : UU := ∏ r s : R, ∏ x : G, m (op1 r s) x = (m r x) + (m s x). Definition mult_isrdistr_wrt_ringop2 {R : ring} {G : abgr} (m : R -> G -> G) : UU := ∏ r s : R, ∏ x : G, m (op2 r s) x = m r (m s x). Definition mult_unel {R : ring} {G : abgr} (m : R -> G -> G) : UU := ∏ x : G, m ringunel2 x = x. Local Close Scope addmonoid. Definition mult_to_ringofendabgr {R : ring} {G : abgr} {m : R -> G -> G} (ax1 : mult_isldistr_wrt_grop m) (r : R) : ringofendabgr G. Proof. use monoidfunconstr. intro x. exact (m r x). apply make_dirprod. + intros x y. apply ax1. + apply (grlcan G (m r (unel G))). rewrite runax. rewrite <- (ax1 r (unel G) (unel G)). rewrite runax. apply idpath. Defined. Definition mult_to_module_struct {R : ring} {G : abgr} {m : R -> G -> G} (ax1 : mult_isldistr_wrt_grop m) (ax2 : mult_isrdistr_wrt_ringop1 m) (ax3 : mult_isrdistr_wrt_ringop2 m) (ax4 : mult_unel m) : module_struct R G. Proof. split with (λ r : R, mult_to_ringofendabgr ax1 r). apply make_dirprod. - apply make_dirprod. + intros r s. use total2_paths2_f. * apply funextfun. intro x. apply ax2. * apply isapropismonoidfun. + use total2_paths2_f. * apply funextfun. intro x. change (m ringunel1 x = unel G). apply (grlcan G (m (ringunel1) x)). rewrite runax. rewrite <- (ax2 ringunel1 ringunel1 x). rewrite ringrunax1. apply idpath. * apply isapropismonoidfun. - apply make_dirprod. + intros r s. use total2_paths2_f. * apply funextfun. intro x. apply ax3. * apply isapropismonoidfun. + use total2_paths2_f. * apply funextfun. intro x. apply ax4. * apply isapropismonoidfun. Defined. Definition mult_to_module {R : ring} {G : abgr} {m : R -> G -> G} (ax1 : mult_isldistr_wrt_grop m) (ax2 : mult_isrdistr_wrt_ringop1 m) (ax3 : mult_isrdistr_wrt_ringop2 m) (ax4 : mult_unel m) : module R := make_module G (mult_to_module_struct ax1 ax2 ax3 ax4). (** *** R-module morphisms *) (** **** Linearity *) Definition islinear {R : ring} {M N : module R} (f : M -> N) := ∏ r : R, ∏ x : M, f (r * x) = r * (f x). Definition linearfun {R : ring} (M N : module R) : UU := ∑ f : M -> N, islinear f. Definition make_linearfun {R : ring} {M N : module R} (f : M -> N) (is : islinear f) : linearfun M N := tpair _ f is. Definition pr1linearfun {R : ring} {M N : module R} (f : linearfun M N) : M -> N := pr1 f. Coercion pr1linearfun : linearfun >-> Funclass. Definition linearfun_islinear {R} {M N : module R} (f : linearfun M N) : islinear f := pr2 f. Lemma islinearfuncomp {R : ring} {M N P : module R} (f : linearfun M N) (g : linearfun N P) : islinear (funcomp f g). Proof. intros r x; simpl. rewrite (linearfun_islinear f). rewrite (linearfun_islinear g). apply idpath. Defined. Definition linearfuncomp {R : ring} {M N P : module R} (f : linearfun M N) (g : linearfun N P) : linearfun M P := tpair _ (funcomp f g) (islinearfuncomp f g). Lemma isapropislinear {R : ring} {M N : module R} (f : M -> N) : isaprop (islinear f). Proof. apply (impred 1 _). intro r. apply (impred 1 _). intro x. apply (setproperty N). Defined. (** The type of linear functions M -> N is a set. *) Lemma isasetlinearfun {R : ring} (M N : module R) : isaset (linearfun M N). Proof. intros. apply (isasetsubset (@pr1linearfun R M N)). - change (isofhlevel 2 (M -> N)). apply impred. exact (fun x => setproperty N). - refine (isinclpr1 _ _). intro. apply isapropislinear. Defined. (** **** [modulefun] *) Definition ismodulefun {R : ring} {M N : module R} (f : M -> N) : UU := (isbinopfun f) × (islinear f). Definition make_ismodulefun {R : ring} {M N : module R} {f : M -> N} (H1 : isbinopfun f) (H2 : islinear f) : ismodulefun f := tpair _ H1 H2. Lemma isapropismodulefun {R : ring} {M N : module R} (f : M -> N) : isaprop (ismodulefun f). Proof. exact (@isofhleveldirprod 1 (isbinopfun f) (islinear f) (isapropisbinopfun f) (isapropislinear f)). Defined. Definition modulefun {R : ring} (M N : module R) : UU := ∑ f : M -> N, ismodulefun f. Definition make_modulefun {R : ring} {M N : module R} (f : M -> N) (is : ismodulefun f) : modulefun M N := tpair _ f is. Local Notation "R-mod( M , N )" := (modulefun M N) : module_scope. Section accessors. Context {R : ring} {M N : module R} (f : R-mod(M, N)). Definition pr1modulefun : M -> N := pr1 f. Definition modulefun_ismodulefun : ismodulefun pr1modulefun := pr2 f. Definition modulefun_to_isbinopfun : isbinopfun pr1modulefun := pr1 modulefun_ismodulefun. Definition modulefun_to_binopfun : binopfun M N := make_binopfun pr1modulefun modulefun_to_isbinopfun. Definition modulefun_to_islinear : islinear pr1modulefun := pr2 modulefun_ismodulefun. Definition modulefun_to_linearfun : linearfun M N := make_linearfun pr1modulefun modulefun_to_islinear. End accessors. Coercion pr1modulefun : modulefun >-> Funclass. Lemma ismodulefun_comp {R} {M N P : module R} (f : R-mod(M,N)) (g : R-mod(N,P)) : ismodulefun (g ∘ f)%functions. Proof. exact (make_dirprod (isbinopfuncomp (modulefun_to_binopfun f) (modulefun_to_binopfun g)) (islinearfuncomp (modulefun_to_linearfun f) (modulefun_to_linearfun g))). Defined. Definition modulefun_comp {R} {M N P : module R} (f : R-mod(M, N)) (g : R-mod(N,P)) : R-mod(M,P) := (funcomp f g,, ismodulefun_comp f g). Lemma modulefun_unel {R : ring} {M N : module R} (f : R-mod(M, N)) : f (unel M) = unel N. Proof. rewrite <- (module_mult_0_to_0 (unel M)). rewrite ((modulefun_to_islinear f) ringunel1 (unel M)). rewrite (module_mult_0_to_0 _). reflexivity. Defined. Definition moduletomonoid {R : ring} (M : module R) : abmonoid := abgrtoabmonoid (pr1module M). Definition modulefun_to_monoidfun {R : ring} {M N : module R} (f : R-mod(M, N)) : monoidfun (moduletomonoid M) (moduletomonoid N) := tpair _ (pr1 f) (tpair _ (pr1 (pr2 f)) (modulefun_unel f)). Definition modulefun_from_monoidfun {R : ring} {M N : module R} (f : R-mod(M, N)) (H : islinear (pr1 f)) : R-mod(M, N) := make_modulefun (pr1 f) (make_ismodulefun (pr1 (pr2 f)) H). Lemma modulefun_paths {R : ring} {M N : module R} {f g : R-mod(M, N)} (p : pr1 f = pr1 g) : f = g. Proof. use total2_paths_f. - exact p. - use proofirrelevance. use isapropismodulefun. Defined. Lemma modulefun_paths2 {R : ring} {M N : module R} {f g : modulefun M N} (p : pr1 f ~ pr1 g) : f = g. Proof. exact (modulefun_paths (funextfun _ _ p)). Defined. Lemma isasetmodulefun {R : ring} (M N : module R) : isaset (R-mod(M, N)). Proof. intros. apply (isasetsubset (@pr1modulefun R M N)). - change (isofhlevel 2 (M -> N)). apply impred. intro. apply (setproperty N). - refine (isinclpr1 _ _). intro. apply isapropismodulefun. Defined. (* module structure of morphisms between modules *) Lemma modulehombinop_ismodulefun {R : ring} {M N : module R} (f g : R-mod(M, N)) : @ismodulefun R M N (λ x : pr1 M, (pr1 f x * pr1 g x)%multmonoid). Proof. use make_ismodulefun. - exact (pr1 (abmonoidshombinop_ismonoidfun (modulefun_to_monoidfun f) (modulefun_to_monoidfun g))). - intros r m. rewrite (modulefun_to_islinear f). rewrite (modulefun_to_islinear g). rewrite <- module_mult_is_ldistr. reflexivity. Defined. Definition modulehombinop {R : ring} {M N : module R} : binop (R-mod(M, N)) := (λ f g, make_modulefun _ (modulehombinop_ismodulefun f g)). Lemma unelmodulefun_ismodulefun {R : ring} (M N : module R) : ismodulefun (λ x : M, (unel N)). Proof. use make_ismodulefun. - use make_isbinopfun. intros m m'. use pathsinv0. use lunax. - intros r m. rewrite module_mult_1. reflexivity. Qed. Definition unelmodulefun {R : ring} (M N : module R) : R-mod(M, N) := make_modulefun _ (unelmodulefun_ismodulefun M N). Lemma modulebinop_runax {R : ring} {M N : module R} (f : R-mod(M, N)) : modulehombinop f (unelmodulefun M N) = f. Proof. use modulefun_paths2. intros x. use (runax N). Qed. Lemma modulebinop_lunax {R : ring} {M N : module R} (f : R-mod(M, N)) : modulehombinop (unelmodulefun M N) f = f. Proof. use modulefun_paths2. intros x. use (lunax N). Qed. Lemma modulehombinop_assoc {R : ring} {M N : module R} (f g h : R-mod(M, N)) : modulehombinop (modulehombinop f g) h = modulehombinop f (modulehombinop g h). Proof. use modulefun_paths2. intros x. use assocax. Qed. Lemma modulehombinop_comm {R : ring} {M N : module R} (f g : R-mod(M, N)) : modulehombinop f g = modulehombinop g f. Proof. use modulefun_paths2. intros x. use (commax N). Qed. Lemma modulehomabmodule_ismoduleop {R : ring} {M N : module R} : ismonoidop (λ f g : R-mod(M, N), modulehombinop f g). Proof. use make_ismonoidop. - intros f g h. exact (modulehombinop_assoc f g h). - use make_isunital. + exact (unelmodulefun M N). + use make_isunit. * intros f. exact (modulebinop_lunax f). * intros f. exact (modulebinop_runax f). Defined. Lemma modulehombinop_inv_ismodulefun {R : ring} {M N : module R} (f : R-mod(M, N)) : ismodulefun (λ m : M, grinv N (pr1 f m)). Proof. use tpair. - use make_isbinopfun. intros x x'. cbn. rewrite (pr1 (pr2 f)). rewrite (pr2 (pr2 (pr1module N))). use (grinvop N). - intros r m. rewrite <- module_inv_mult. apply maponpaths. apply (pr2 f). Qed. Definition modulehombinop_inv {R : ring} {M N : module R} (f : R-mod(M, N)) : R-mod(M, N) := tpair _ _ (modulehombinop_inv_ismodulefun f). Lemma modulehombinop_linvax {R : ring} {M N : module R} (f : R-mod(M, N)) : modulehombinop (modulehombinop_inv f) f = unelmodulefun M N. Proof. use modulefun_paths2. intros x. use (@grlinvax N). Qed. Lemma modulehombinop_rinvax {R : ring} {M N : module R} (f : R-mod(M, N)) : modulehombinop f (modulehombinop_inv f) = unelmodulefun M N. Proof. use modulefun_paths2. intros x. use (grrinvax N). Qed. Lemma modulehomabgr_isabgrop {R : ring} (M N : module R) : isabgrop (λ f g : R-mod(M, N), modulehombinop f g). Proof. use make_isabgrop. use make_isgrop. - use modulehomabmodule_ismoduleop. - use make_invstruct. + intros f. exact (modulehombinop_inv f). + use make_isinv. * intros f. exact (modulehombinop_linvax f). * intros f. exact (modulehombinop_rinvax f). - intros f g. exact (modulehombinop_comm f g). Defined. Definition modulehomabgr {R : ring} (M N : module R) : abgr. Proof. use make_abgr. use make_setwithbinop. use make_hSet. - exact (R-mod(M, N)). - exact (isasetmodulefun M N). - exact (@modulehombinop R M N). - exact (modulehomabgr_isabgrop M N). Defined. Definition modulehombinop_scalar_ismodulefun {R : commring} {M N : module R} (r : R) (f : R-mod(M, N)) : ismodulefun (λ m : M, r * (pr1 f m)). Proof. use tpair. - use make_isbinopfun. intros x x'. cbn. rewrite (pr1 (pr2 f)). rewrite module_mult_is_ldistr. reflexivity. - intros r0 m. rewrite (modulefun_to_islinear f). do 2 rewrite <- module_mult_assoc. rewrite ringcomm2. reflexivity. Qed. Definition modulehombinop_smul {R : commring} {M N : module R} (r : R) (f : R-mod(M, N)) : modulefun M N := make_modulefun _ (modulehombinop_scalar_ismodulefun r f). Definition modulehommodule {R : commring} (M N : module R) : module R. Proof. use make_module. use (modulehomabgr M N). use mult_to_module_struct. exact modulehombinop_smul. - intros r f g. use modulefun_paths2. intros x. apply module_mult_is_ldistr. - intros r r0 f. use modulefun_paths2. intros x. apply module_mult_is_rdistr. - intros r r0 f. use modulefun_paths2. intros x. apply module_mult_assoc. - intros f. use modulefun_paths2. intros x. cbn. apply module_mult_unel2. Defined. (** **** Isomorphisms ([moduleiso]) *) Definition moduleiso {R : ring} (M N : module R) : UU := ∑ w : pr1module M ≃ pr1module N, ismodulefun w. Section accessors_moduleiso. Context {R : ring} {M N : module R} (f : moduleiso M N). Definition moduleiso_to_weq : (pr1module M) ≃ (pr1module N) := pr1 f. Definition moduleiso_ismodulefun : ismodulefun moduleiso_to_weq := pr2 f. Definition moduleiso_to_modulefun : R-mod(M, N) := (tpair _ (pr1weq moduleiso_to_weq) (pr2 f)). End accessors_moduleiso. Coercion moduleiso_to_weq : moduleiso >-> weq. Coercion moduleiso_to_modulefun : moduleiso >-> modulefun. Definition make_moduleiso {R} {M N : module R} f is : moduleiso M N := tpair _ f is. Lemma isbinopfuninvmap {R} {M N : module R} (f : moduleiso M N) : isbinopfun (invmap f). Proof. intros x y. apply (invmaponpathsweq f). rewrite (homotweqinvweq f (op x y)). apply pathsinv0. transitivity (op ((moduleiso_to_weq f) (invmap f x)) ((moduleiso_to_weq f) (invmap f y))). apply (modulefun_to_isbinopfun f (invmap f x) (invmap f y)). rewrite 2 (homotweqinvweq f). apply idpath. Defined. Lemma islinearinvmap {R} {M N : module R} (f : moduleiso M N) : islinear (invmap f). Proof. intros r x. apply (invmaponpathsweq f). transitivity (module_mult N r x). exact (homotweqinvweq f (module_mult N r x)). transitivity (module_mult N r (moduleiso_to_weq f (invmap (moduleiso_to_weq f) x))). rewrite (homotweqinvweq (moduleiso_to_weq f) x). apply idpath. apply pathsinv0. apply (pr2 (moduleiso_ismodulefun f) r (invmap f x)). Defined. Definition invmoduleiso {R} {M N : module R} (f : moduleiso M N) : moduleiso N M. Proof. use make_moduleiso. - exact (invweq f). - apply make_dirprod. + exact (isbinopfuninvmap f). + exact (islinearinvmap f). Defined. Definition moduleiso' {R} (M N : module R) : UU := ∑ w : monoidiso (pr1module M) (pr1module N), islinear w. Lemma moduleiso_to_moduleiso' {R} (M N : module R) : moduleiso M N -> moduleiso' M N. Proof. intro w. use tpair. - use tpair. + exact w. + use tpair. * exact (modulefun_to_isbinopfun w). * apply (modulefun_unel w). - exact (modulefun_to_islinear w). Defined. Lemma moduleiso'_to_moduleiso {R} (M N : module R) : moduleiso' M N -> moduleiso M N. Proof. intro w. use tpair. - exact (pr1 w). - apply make_dirprod. + exact (pr1 (pr2 (pr1 w))). + exact (pr2 w). Defined. Lemma moduleiso'_to_moduleisweq_iso {R} (M N : module R) : isweq (moduleiso'_to_moduleiso M N). Proof. use (isweq_iso _ (moduleiso_to_moduleiso' M N)). - intro w. unfold moduleiso'_to_moduleiso, moduleiso_to_moduleiso'. cbn. induction w as [w1 w2]; cbn. use total2_paths_f; cbn. * use total2_paths_f; cbn. + reflexivity. + apply isapropismonoidfun. * apply isapropislinear. - reflexivity. Defined. Definition moduleiso'_to_moduleweq_iso {R} (M N : module R) : (moduleiso' M N) ≃ (moduleiso M N) := make_weq (moduleiso'_to_moduleiso M N) (moduleiso'_to_moduleisweq_iso M N).