{R : Ring} {M N : RightModule R} (f : M $-> N) : RightSubmodule N := lm_image (R:=rng_op R) f. Global Instance isleftmodule_quotientabgroup {R : Ring} (M : LeftModule R) (N : LeftSubmodule M) : IsLeftModule R (QuotientAbGroup M N). Proof. snrapply Build_IsLeftModule. - intros r. snrapply quotient_abgroup_rec. + refine (grp_quotient_map $o _). snrapply Build_GroupHomomorphism. * exact (lact r). * intros x y. apply lm_dist_l. + intros n Nn; simpl. apply qglue. apply issubgroup_in_inv_op. 2: apply issubgroup_in_unit. by apply is_left_submodule. - intros r m n; revert m. snrapply Quotient_ind_hprop; [exact _ | intros m; revert n]. snrapply Quotient_ind_hprop; [exact _ | intros n; simpl]. rapply ap. apply lm_dist_l. - intros r s. snrapply Quotient_ind_hprop; [exact _| intros m; simpl]. rapply ap. apply lm_dist_r. - intros r s. snrapply Quotient_ind_hprop; [exact _| intros m; simpl]. rapply ap. apply lm_assoc. - snrapply Quotient_ind_hprop; [exact _| intros m; simpl]. rapply ap. apply lm_unit. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.