{R : Ring} {M N : RightModule R} : RightModuleIsomorphism M N -> RightModuleIsomorphism N M := lm_iso_inverse (R:=rng_op R). Global Instance isgraph_leftmodule {R : Ring} : IsGraph (LeftModule R) := Build_IsGraph _ LeftModuleHomomorphism. Global Instance is01cat_leftmodule {R : Ring} : Is01Cat (LeftModule R) := Build_Is01Cat _ _ lm_homo_id (@lm_homo_compose R). Global Instance is2graph_leftmodule {R : Ring} : Is2Graph (LeftModule R) := fun M N => isgraph_induced (@lm_homo_map R M N). Global Instance is1cat_leftmodule {R : Ring} : Is1Cat (LeftModule R). Proof. snrapply Build_Is1Cat'. - intros M N; rapply is01cat_induced. - intros M N; rapply is0gpd_induced. - intros M N L h. snrapply Build_Is0Functor. intros f g p m. exact (ap h (p m)). - intros M N L f. snrapply Build_Is0Functor. intros g h p m. exact (p (f m)). - simpl; reflexivity. - simpl; reflexivity. - simpl; reflexivity. 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.