Require Import WildCat.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.
(* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
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.

Declare Scope module_scope.

(** * Left modules over a ring. *)

(** TODO: Right modules? We can treat right modules as left modules over the opposite ring. *)

(** ** Definition *)

(** An abelian group [M] is a left [R]-module when equipped with the following data: *) 
Class IsLeftModule (R : Ring) (M : AbGroup) := {
  (** A function [lact] (left-action) that takes an element [r : R] and an element [m : M] and returns an element [lact r m : M]. *)
  lact : R -> M -> M;
  (** Actions distribute on the left over addition in the abelian group. That is [lact r (m + n) = lact r m + lact r n]. *)
  lact_left_dist :: LeftHeteroDistribute lact (+) (+);
  (** Actions distribute on the right over addition in the ring. That is [lact (r + s) m = lact r m + lact s m]. *)
  lact_right_dist :: RightHeteroDistribute lact (+) (+);
  (** Actions are associative. That is [lact (r * s) m = lact r (lact s m)]. *)
  lact_assoc :: HeteroAssociative lact lact lact (.*.);
  (** Actions preserve the multiplicative identity. That is [lact 1 m = m]. *)
  lact_unit :: LeftIdentity lact 1;
}.

(** TODO: notation for action. *)

(** A left R-module is an abelian group equipped with a left R-module structure. *)
Record LeftModule (R : Ring) := {
  lm_carrier :> AbGroup;
  lm_lact :: IsLeftModule R lm_carrier;
}.

Section ModuleAxioms.
  Context {R : Ring} {M : LeftModule R} (r s : R) (m n : M).
  (** Here we state the module axioms in a readable form for direct use. *)

  Definition lm_dist_l : lact r (m + n) = lact r m + lact r n := lact_left_dist r m n.
  Definition lm_dist_r : lact (r + s) m = lact r m + lact s m := lact_right_dist r s m.
  Definition lm_assoc : lact r (lact s m) = lact (r * s) m := lact_assoc r s m.
  Definition lm_unit : lact 1 m = m := lact_unit m.

End ModuleAxioms.

(** ** Facts about left modules *)

Section ModuleFacts.
  Context {R : Ring} {M : LeftModule R} (r : R) (m : M).

  (** Here are some quick facts that hold in modules. *) 

  (** The action of zero is zero. *) 
  Definition lm_zero_l : lact 0 m = 0.
R: Ring
M: LeftModule R
r: R
m: M
lact 0 m = 0
  Proof.
R: Ring
M: LeftModule R
r: R
m: M
lact 0 m = 0
    apply (grp_cancelL1 (z := lact 0 m)).
R: Ring
M: LeftModule R
r: R
m: M
sg_op (lact 0 m) (lact 0 m) = lact 0 m
    lhs_V nrapply lm_dist_r.
R: Ring
M: LeftModule R
r: R
m: M
lact (0 + 0) m = lact 0 m
    f_ap.
R: Ring
M: LeftModule R
r: R
m: M
0 + 0 = 0
    apply rng_plus_zero_r.
  Defined.

  (** The action on zero is zero. *)
  Definition lm_zero_r : lact r (0 : M) = 0.
R: Ring
M: LeftModule R
r: R
m: M
lact r (0 : M) = 0
  Proof.
R: Ring
M: LeftModule R
r: R
m: M
lact r (0 : M) = 0
    apply (grp_cancelL1 (z := lact r 0)).
R: Ring
M: LeftModule R
r: R
m: M
sg_op (lact r 0) (lact r 0) = lact r 0
    lhs_V nrapply lm_dist_l.
R: Ring
M: LeftModule R
r: R
m: M
lact r (0 + 0) = lact r 0
    f_ap.
R: Ring
M: LeftModule R
r: R
m: M
0 + 0 = 0
    apply grp_unit_l.
  Defined.

  (** The action of [-1] is the additive inverse. *)
  Definition lm_minus_one : lact (-1) m = -m.
R: Ring
M: LeftModule R
r: R
m: M
lact (-1) m = - m
  Proof.
R: Ring
M: LeftModule R
r: R
m: M
lact (-1) m = - m
     apply grp_moveL_1V.
R: Ring
M: LeftModule R
r: R
m: M
sg_op (lact (-1) m) m = mon_unit
     lhs nrapply (ap (_ +) (lm_unit m)^).
R: Ring
M: LeftModule R
r: R
m: M
lact (-1) m + lact 1 m = mon_unit
     lhs_V nrapply lm_dist_r.
R: Ring
M: LeftModule R
r: R
m: M
lact (-1 + 1) m = mon_unit
     rhs_V nrapply lm_zero_l.
R: Ring
M: LeftModule R
r: R
m: M
lact (-1 + 1) m = lact 0 m
     f_ap.
R: Ring
M: LeftModule R
r: R
m: M
-1 + 1 = 0
     apply grp_inv_l.
  Defined.

End ModuleFacts.

(** ** Left Submodules *)

(** A subgroup of a left R-module is a left submodule if it is closed under the action of R. *)
Class IsLeftSubmodule {R : Ring} {M : LeftModule R} (N : M -> Type) := {
  ils_issubgroup :: IsSubgroup N;
  is_left_submodule : forall r m, N m -> N (lact r m);
}.

(** A left submodule is a subgroup of the abelian group closed under the action of R. *)
Record LeftSubmodule {R : Ring} (M : LeftModule R) := {
  lsm_carrier :> M -> Type;
  lsm_submodule :: IsLeftSubmodule lsm_carrier;
}.

Definition subgroup_leftsubmodule {R : Ring} {M : LeftModule R}
  : LeftSubmodule M -> Subgroup M
  := fun N => Build_Subgroup M N _.
Coercion subgroup_leftsubmodule : LeftSubmodule >-> Subgroup.

(** Submodules inherit the R-module structure of their parent. *)
Global Instance isleftmodule_leftsubmodule {R : Ring}
  {M : LeftModule R} (N : LeftSubmodule M)
  : IsLeftModule R N.
R: Ring
M: LeftModule R
N: LeftSubmodule M
IsLeftModule R N
Proof.
R: Ring
M: LeftModule R
N: LeftSubmodule M
IsLeftModule R N
  snrapply Build_IsLeftModule.
R: Ring
M: LeftModule R
N: LeftSubmodule M
R -> N -> N
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftHeteroDistribute ?lact plus plus
R: Ring
M: LeftModule R
N: LeftSubmodule M
RightHeteroDistribute ?lact plus plus
R: Ring
M: LeftModule R
N: LeftSubmodule M
HeteroAssociative ?lact ?lact ?lact mult
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftIdentity ?lact 1
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
R -> N -> N intros r [n n_in_N].
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
n_in_N: N n
N
    exists (lact r n).
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
n_in_N: N n
N (lact r n)
    by apply lsm_submodule.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftHeteroDistribute
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2) plus plus intros r [n] [m]; apply path_sigma_hprop.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
proj2: N n
m: M
proj0: N m
(lact r ((n; proj2) + (m; proj0)).1;
let X :=
  fun (M : LeftModule R) (l : LeftSubmodule M) =>
  is_left_submodule in
X M N r ((n; proj2) + (m; proj0)).1
  ((n; proj2) + (m; proj0)).2).1 =
((lact r n;
 let X :=
   fun (M : LeftModule R) (l : LeftSubmodule M) =>
   is_left_submodule in
 X M N r n proj2) +
 (lact r m;
 let X :=
   fun (M : LeftModule R) (l : LeftSubmodule M) =>
   is_left_submodule in
 X M N r m proj0)).1
    apply lact_left_dist.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
RightHeteroDistribute
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2) plus plus intros r s [n]; apply path_sigma_hprop.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
n: M
proj2: N n
(lact (r + s) n;
let X :=
  fun (M : LeftModule R) (l : LeftSubmodule M) =>
  is_left_submodule in
X M N (r + s) n proj2).1 =
((lact r n;
 let X :=
   fun (M : LeftModule R) (l : LeftSubmodule M) =>
   is_left_submodule in
 X M N r n proj2) +
 (lact s n;
 let X :=
   fun (M : LeftModule R) (l : LeftSubmodule M) =>
   is_left_submodule in
 X M N s n proj2)).1
    apply lact_right_dist.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
HeteroAssociative
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2)
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2)
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2) mult intros r s [n]; apply path_sigma_hprop.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
n: M
proj2: N n
(lact r (lact s n);
let X :=
  fun (M : LeftModule R) (l : LeftSubmodule M) =>
  is_left_submodule in
X M N r (lact s n)
  (let X0 :=
     fun (M : LeftModule R) (l : LeftSubmodule M) =>
     is_left_submodule in
   X0 M N s n proj2)).1 =
(lact (r * s) n;
let X :=
  fun (M : LeftModule R) (l : LeftSubmodule M) =>
  is_left_submodule in
X M N (r * s) n proj2).1
    apply lact_assoc.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftIdentity
  (fun (r : R) (X : N) =>
   (fun (n : M) (n_in_N : N n) =>
    (lact r n;
    let X0 :=
      fun (M : LeftModule R) (l : LeftSubmodule M) =>
      is_left_submodule in
    X0 M N r n n_in_N)) X.1 X.2) 1 intros [n]; apply path_sigma_hprop.
R: Ring
M: LeftModule R
N: LeftSubmodule M
n: M
proj2: N n
(lact 1 n;
let X :=
  fun (M : LeftModule R) (l : LeftSubmodule M) =>
  is_left_submodule in
X M N 1 n proj2).1 = (n; proj2).1
    apply lact_unit.
Defined.

(** Any left submodule of a left R-module is a left R-module. *)
Definition leftmodule_leftsubmodule {R : Ring}
  {M : LeftModule R} (N : LeftSubmodule M)
  : LeftModule R
  := Build_LeftModule R N _.
Coercion leftmodule_leftsubmodule : LeftSubmodule >-> LeftModule.

(** The submodule criterion. This is a convenient way to build submodules. *)
Definition Build_IsLeftSubmodule' {R : Ring} {M : LeftModule R} 
  (H : M -> Type) `{forall x, IsHProp (H x)}
  (z : H zero)
  (c : forall r n m, H n -> H m -> H (n + lact r m))
  : IsLeftSubmodule H.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
IsLeftSubmodule H
Proof.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
IsLeftSubmodule H
  snrapply Build_IsLeftSubmodule.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
IsSubgroup H
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall (r : R) (m : M), H m -> H (lact r m)
  -
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
IsSubgroup H snrapply Build_IsSubgroup'.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall x : M, IsHProp (H x)
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
H mon_unit
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall x y : M, H x -> H y -> H (sg_op x (- y))
    +
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall x : M, IsHProp (H x) exact _.
    +
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
H mon_unit exact z.
    +
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall x y : M, H x -> H y -> H (sg_op x (- y)) intros x y hx hy.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
x, y: M
hx: H x
hy: H y
H (sg_op x (- y))
      change (sg_op ?x ?y) with (x + y).
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
x, y: M
hx: H x
hy: H y
H (x - y)
      pose proof (p := c (-1) x y hx hy).
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
x, y: M
hx: H x
hy: H y
p: H (x + lact (-1) y)
H (x - y)
      rewrite lm_minus_one in p.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
x, y: M
hx: H x
hy: H y
p: H (x - y)
H (x - y)
      exact p.
  -
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
forall (r : R) (m : M), H m -> H (lact r m) intros r m hm.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
r: R
m: M
hm: H m
H (lact r m)
    rewrite <- (grp_unit_l).
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
r: R
m: M
hm: H m
H (sg_op mon_unit (lact r m))
    by apply c.
Defined.

Definition Build_LeftSubmodule' {R : Ring} {M : LeftModule R}
  (H : M -> Type) `{forall x, IsHProp (H x)}
  (z : H zero)
  (c : forall r n m, H n -> H m -> H (n + lact r m))
  : LeftSubmodule M.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
LeftSubmodule M
Proof.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
LeftSubmodule M
  pose (p := Build_IsLeftSubmodule' H z c).
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
LeftSubmodule M
  snrapply Build_LeftSubmodule.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
M -> Type
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
IsLeftSubmodule ?lsm_carrier
  1: snrapply (Build_Subgroup _ H).
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
IsSubgroup H
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
IsLeftSubmodule
  {|
    subgroup_pred := H;
    subgroup_issubgroup := ?subgroup_issubgroup
  |}
  2: exact p.
R: Ring
M: LeftModule R
H: M -> Type
H0: forall x : M, IsHProp (H x)
z: H 0
c: forall (r : R) (n m : M),
H n -> H m -> H (n + lact r m)
p:= Build_IsLeftSubmodule' H z c: IsLeftSubmodule H
IsSubgroup H
  rapply ils_issubgroup.
Defined.

(** ** Left R-module homomorphisms *)

(** A left module homomorphism is a group homomorphism that commutes with the action of R. *)
Record LeftModuleHomomorphism {R : Ring} (M N : LeftModule R) := {
  lm_homo_map :> GroupHomomorphism M N;
  lm_homo_lact : forall r m, lm_homo_map (lact r m) = lact r (lm_homo_map m);
}.

Definition lm_homo_id {R : Ring} (M : LeftModule R) : LeftModuleHomomorphism M M.
R: Ring
M: LeftModule R
LeftModuleHomomorphism M M
Proof.
R: Ring
M: LeftModule R
LeftModuleHomomorphism M M
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M: LeftModule R
GroupHomomorphism M M
R: Ring
M: LeftModule R
forall (r : R) (m : M),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M: LeftModule R
GroupHomomorphism M M exact grp_homo_id.
  -
R: Ring
M: LeftModule R
forall (r : R) (m : M),
grp_homo_id (lact r m) = lact r (grp_homo_id m) reflexivity.
Defined.

Definition lm_homo_compose {R : Ring} {M N L : LeftModule R}
  : LeftModuleHomomorphism N L -> LeftModuleHomomorphism M N
  -> LeftModuleHomomorphism M L.
R: Ring
M, N, L: LeftModule R
LeftModuleHomomorphism N L ->
LeftModuleHomomorphism M N ->
LeftModuleHomomorphism M L
Proof.
R: Ring
M, N, L: LeftModule R
LeftModuleHomomorphism N L ->
LeftModuleHomomorphism M N ->
LeftModuleHomomorphism M L
  intros f g.
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
LeftModuleHomomorphism M L
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
GroupHomomorphism M L
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
forall (r : R) (m : M),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
GroupHomomorphism M L exact (grp_homo_compose f g).
  -
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
forall (r : R) (m : M),
grp_homo_compose f g (lact r m) =
lact r (grp_homo_compose f g m) intros r m.
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
r: R
m: M
grp_homo_compose f g (lact r m) =
lact r (grp_homo_compose f g m)
    rhs_V nrapply lm_homo_lact.
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
r: R
m: M
grp_homo_compose f g (lact r m) = f (lact r (g m))
    apply (ap f).
R: Ring
M, N, L: LeftModule R
f: LeftModuleHomomorphism N L
g: LeftModuleHomomorphism M N
r: R
m: M
g (lact r m) = lact r (g m)
    apply lm_homo_lact.
Defined.

(** Smart constructor for building left module homomorphisms from a map. *)
Definition Build_LeftModuleHomomorphism' {R : Ring} {M N : LeftModule R}
  (f : M -> N) (p : forall r x y, f (lact r x + y) = lact r (f x) + f y)
  : LeftModuleHomomorphism M N.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
LeftModuleHomomorphism M N
Proof.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
LeftModuleHomomorphism M N
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
GroupHomomorphism M N
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
forall (r : R) (m : M),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
GroupHomomorphism M N snrapply Build_GroupHomomorphism.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
M -> N
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
IsSemiGroupPreserving ?f
    +
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
M -> N exact f.
    +
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
IsSemiGroupPreserving f intros x y.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
x, y: M
f (sg_op x y) = sg_op (f x) (f y)
      rewrite <- (lm_unit (f x)).
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
x, y: M
f (sg_op x y) = sg_op (lact 1 (f x)) (f y)
      set (lact 1 (f x)).
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
x, y: M
g:= lact 1 (f x): N
f (sg_op x y) = sg_op g (f y)
      rewrite <- (lm_unit x).
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
x, y: M
g:= lact 1 (f x): N
f (sg_op (lact 1 x) y) = sg_op g (f y)
      apply p.
  -
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
forall (r : R) (m : M),
Build_GroupHomomorphism f (lact r m) =
lact r (Build_GroupHomomorphism f m) intros r m.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
Build_GroupHomomorphism f (lact r m) =
lact r (Build_GroupHomomorphism f m)
    simpl.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
f (lact r m) = lact r (f m)
    rewrite <- (grp_unit_r (lact r m)).
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
f (sg_op (lact r m) mon_unit) = lact r (f m)
    rewrite p.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
lact r (f m) + f mon_unit = lact r (f m)
    rhs_V nrapply grp_unit_r.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
lact r (f m) + f mon_unit =
sg_op (lact r (f m)) mon_unit
    apply grp_cancelL.
R: Ring
M, N: LeftModule R
f: M -> N
p: forall (r : R) (x y : M),
f (lact r x + y) = lact r (f x) + f y
r: R
m: M
f mon_unit = mon_unit
    specialize (p 1 0 0).
R: Ring
M, N: LeftModule R
f: M -> N
p: f (lact 1 0 + 0) = lact 1 (f 0) + f 0
r: R
m: M
f mon_unit = mon_unit
    rewrite 2 lm_unit in p.
R: Ring
M, N: LeftModule R
f: M -> N
p: f (0 + 0) = f 0 + f 0
r: R
m: M
f mon_unit = mon_unit
    apply (grp_cancelL1 (z := f 0)).
R: Ring
M, N: LeftModule R
f: M -> N
p: f (0 + 0) = f 0 + f 0
r: R
m: M
sg_op (f 0) (f mon_unit) = f 0
    lhs_V nrapply p.
R: Ring
M, N: LeftModule R
f: M -> N
p: f (0 + 0) = f 0 + f 0
r: R
m: M
f (0 + 0) = f 0
    apply ap.
R: Ring
M, N: LeftModule R
f: M -> N
p: f (0 + 0) = f 0 + f 0
r: R
m: M
0 + 0 = 0
    apply grp_unit_l.
Defined.

Record LeftModuleIsomorphism {R : Ring} (M N : LeftModule R) := {
  lm_iso_map :> LeftModuleHomomorphism M N;
  isequiv_lm_iso_map :: IsEquiv lm_iso_map;
}.

Definition Build_LeftModuleIsomorphism' {R : Ring} (M N : LeftModule R)
  (f : GroupIsomorphism M N) (p : forall r x, f (lact r x) = lact r (f x))
  : LeftModuleIsomorphism M N.
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
LeftModuleIsomorphism M N
Proof.
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
LeftModuleIsomorphism M N
  snrapply Build_LeftModuleIsomorphism.
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
LeftModuleHomomorphism M N
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
IsEquiv ?lm_iso_map
  -
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
LeftModuleHomomorphism M N snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
GroupHomomorphism M N
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
forall (r : R) (m : M),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
    +
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
GroupHomomorphism M N exact f.
    +
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
forall (r : R) (m : M), f (lact r m) = lact r (f m) exact p.
  -
R: Ring
M, N: LeftModule R
f: GroupIsomorphism M N
p: forall (r : R) (x : M),
f (lact r x) = lact r (f x)
IsEquiv {| lm_homo_map := f; lm_homo_lact := p |} exact _.
Defined.

Definition lm_iso_inverse {R : Ring} {M N : LeftModule R}
  : LeftModuleIsomorphism M N -> LeftModuleIsomorphism N M.
R: Ring
M, N: LeftModule R
LeftModuleIsomorphism M N -> LeftModuleIsomorphism N M
Proof.
R: Ring
M, N: LeftModule R
LeftModuleIsomorphism M N -> LeftModuleIsomorphism N M
  intros f.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
LeftModuleIsomorphism N M
  snrapply Build_LeftModuleIsomorphism.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
LeftModuleHomomorphism N M
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
IsEquiv ?lm_iso_map
  -
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
LeftModuleHomomorphism N M snrapply Build_LeftModuleHomomorphism'.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
N -> M
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
forall (r : R) (x y : N),
?f (lact r x + y) = lact r (?f x) + ?f y
    +
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
N -> M exact f^-1.
    +
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
forall (r : R) (x y : N),
f^-1 (lact r x + y) = lact r (f^-1 x) + f^-1 y intros r m n.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
f^-1 (lact r m + n) = lact r (f^-1 m) + f^-1 n
      apply moveR_equiv_V.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
lact r m + n = f (lact r (f^-1 m) + f^-1 n) 
      rhs nrapply grp_homo_op.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
lact r m + n =
sg_op (f (lact r (f^-1 m))) (f (f^-1 n))
      symmetry.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
sg_op (f (lact r (f^-1 m))) (f (f^-1 n)) =
lact r m + n
      f_ap.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
f (lact r (f^-1 m)) = lact r m
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
f (f^-1 n) = n
      2: apply eisretr.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
f (lact r (f^-1 m)) = lact r m
      lhs nrapply lm_homo_lact.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
lact r (f (f^-1 m)) = lact r m
      apply ap.
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
r: R
m, n: N
f (f^-1 m) = m
      apply eisretr.
  -
R: Ring
M, N: LeftModule R
f: LeftModuleIsomorphism M N
IsEquiv
  (Build_LeftModuleHomomorphism' f^-1
     (fun (r : R) (m n : N) =>
      moveR_equiv_V (lact r m + n)
        (lact r (f^-1 m) + f^-1 n)
        ((ap11
            (ap11 1
               (lm_homo_lact M N f r (f^-1 m) @
                ap (lact r) (eisretr f m)))
            (eisretr f n))^ @
         (grp_homo_op f (lact r (f^-1 m)) (f^-1 n))^))) exact _.
Defined.

(** ** Category of left R-modules *)

(** TODO: define as a displayed category over Ring *)

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).
R: Ring
Is1Cat (LeftModule R)
Proof.
R: Ring
Is1Cat (LeftModule R)
  snrapply Build_Is1Cat'.
R: Ring
forall a b : LeftModule R, Is01Cat (a $-> b)
R: Ring
forall a b : LeftModule R, Is0Gpd (a $-> b)
R: Ring
forall (a b c : LeftModule R) (g : b $-> c),
Is0Functor (cat_postcomp a g)
R: Ring
forall (a b c : LeftModule R) (f : a $-> b),
Is0Functor (cat_precomp c f)
R: Ring
forall (a b c d : LeftModule R) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
Id b $o f $== f
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
f $o Id a $== f
  -
R: Ring
forall a b : LeftModule R, Is01Cat (a $-> b) intros M N; rapply is01cat_induced.
  -
R: Ring
forall a b : LeftModule R, Is0Gpd (a $-> b) intros M N; rapply is0gpd_induced.
  -
R: Ring
forall (a b c : LeftModule R) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros M N L h.
R: Ring
M, N, L: LeftModule R
h: N $-> L
Is0Functor (cat_postcomp M h)
    snrapply Build_Is0Functor.
R: Ring
M, N, L: LeftModule R
h: N $-> L
forall a b : M $-> N,
(a $-> b) -> cat_postcomp M h a $-> cat_postcomp M h b
    intros f g p m.
R: Ring
M, N, L: LeftModule R
h: N $-> L
f, g: M $-> N
p: f $-> g
m: M
cat_postcomp M h f m = cat_postcomp M h g m
    exact (ap h (p m)).
  -
R: Ring
forall (a b c : LeftModule R) (f : a $-> b),
Is0Functor (cat_precomp c f) intros M N L f.
R: Ring
M, N, L: LeftModule R
f: M $-> N
Is0Functor (cat_precomp L f)
    snrapply Build_Is0Functor.
R: Ring
M, N, L: LeftModule R
f: M $-> N
forall a b : N $-> L,
(a $-> b) -> cat_precomp L f a $-> cat_precomp L f b
    intros g h p m.
R: Ring
M, N, L: LeftModule R
f: M $-> N
g, h: N $-> L
p: g $-> h
m: M
cat_precomp L f g m = cat_precomp L f h m
    exact (p (f m)).
  -
R: Ring
forall (a b c d : LeftModule R) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f) simpl; reflexivity.
  -
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
Id b $o f $== f simpl; reflexivity.
  -
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
f $o Id a $== f simpl; reflexivity.
Defined.

Global Instance hasequivs_leftmodule {R : Ring} : HasEquivs (LeftModule R).
R: Ring
HasEquivs (LeftModule R)
Proof.
R: Ring
HasEquivs (LeftModule R)
  snrapply Build_HasEquivs.
R: Ring
LeftModule R -> LeftModule R -> Type
R: Ring
forall a b : LeftModule R, (a $-> b) -> Type
R: Ring
forall a b : LeftModule R, ?CatEquiv' a b -> a $-> b
R: Ring
forall (a b : LeftModule R) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
R: Ring
forall (a b : LeftModule R) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
R: Ring
forall a b : LeftModule R, ?CatEquiv' a b -> b $-> a
R: Ring
forall (a b : LeftModule R) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
R: Ring
forall (a b : LeftModule R) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
R: Ring
forall (a b : LeftModule R) (f : a $-> b)
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  -
R: Ring
LeftModule R -> LeftModule R -> Type exact LeftModuleIsomorphism.
  -
R: Ring
forall a b : LeftModule R, (a $-> b) -> Type intros M N; exact IsEquiv.
  -
R: Ring
forall a b : LeftModule R,
LeftModuleIsomorphism a b -> a $-> b intros M N f; exact f.
  -
R: Ring
forall (a b : LeftModule R)
(f : LeftModuleIsomorphism a b),
(fun (M N : LeftModule R) (f0 : M $-> N) => IsEquiv f0)
  a b
  ((fun (M N : LeftModule R)
      (f0 : LeftModuleIsomorphism M N) =>
    lm_iso_map M N f0) a b f) simpl; exact _.
  -
R: Ring
forall (a b : LeftModule R) (f : a $-> b),
(fun (M N : LeftModule R) (f0 : M $-> N) => IsEquiv f0)
  a b f -> LeftModuleIsomorphism a b apply Build_LeftModuleIsomorphism.
  -
R: Ring
forall (a b : LeftModule R) (f : a $-> b)
(fe : (fun (M N : LeftModule R) (f0 : M $-> N) =>
       IsEquiv f0) a b f),
(fun (M N : LeftModule R)
   (f0 : LeftModuleIsomorphism M N) =>
 lm_iso_map M N f0) a b
  {| lm_iso_map := f; isequiv_lm_iso_map := fe |} $==
f reflexivity.
  -
R: Ring
forall a b : LeftModule R,
LeftModuleIsomorphism a b -> b $-> a intros M N; apply lm_iso_inverse.
  -
R: Ring
forall (a b : LeftModule R)
(f : LeftModuleIsomorphism a b),
(fun M N : LeftModule R =>
 let X :=
   fun H : LeftModuleIsomorphism M N =>
   lm_iso_map N M (lm_iso_inverse H) in
 X) a b f $o
(fun (M N : LeftModule R)
   (f0 : LeftModuleIsomorphism M N) =>
 lm_iso_map M N f0) a b f $== Id a intros M N f; apply eissect.
  -
R: Ring
forall (a b : LeftModule R)
(f : LeftModuleIsomorphism a b),
(fun (M N : LeftModule R)
   (f0 : LeftModuleIsomorphism M N) =>
 lm_iso_map M N f0) a b f $o
(fun M N : LeftModule R =>
 let X :=
   fun H : LeftModuleIsomorphism M N =>
   lm_iso_map N M (lm_iso_inverse H) in
 X) a b f $== Id b intros M N f; apply eisretr.
  -
R: Ring
forall (a b : LeftModule R) (f : a $-> b)
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (M N : LeftModule R) (f0 : M $-> N) => IsEquiv f0)
  a b f intros M N f g fg gf.
R: Ring
M, N: LeftModule R
f: M $-> N
g: N $-> M
fg: f $o g $== Id N
gf: g $o f $== Id M
(fun (M N : LeftModule R) (f : M $-> N) => IsEquiv f)
  M N f
    exact (isequiv_adjointify f g fg gf).
Defined.

(** ** Kernel of module homomorphism *)

Global Instance isleftsubmodule_grp_kernel {R : Ring}
  {M N : LeftModule R} (f : M $-> N)
  : IsLeftSubmodule (grp_kernel f).
R: Ring
M, N: LeftModule R
f: M $-> N
IsLeftSubmodule (grp_kernel f)
Proof.
R: Ring
M, N: LeftModule R
f: M $-> N
IsLeftSubmodule (grp_kernel f)
  srapply Build_IsLeftSubmodule.
R: Ring
M, N: LeftModule R
f: M $-> N
forall (r : R) (m : M),
grp_kernel f m -> grp_kernel f (lact r m)
  intros r m n.
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
n: grp_kernel f m
grp_kernel f (lact r m)
  lhs nrapply lm_homo_lact.
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
n: grp_kernel f m
lact r (f m) = group_unit
  rhs_V nrapply (lm_zero_r r).
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
n: grp_kernel f m
lact r (f m) = lact r 0
  apply ap.
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
n: grp_kernel f m
f m = 0
  exact n.
Defined.

Definition lm_kernel {R : Ring} {M N : LeftModule R} (f : M $-> N)
  : LeftSubmodule M
  := Build_LeftSubmodule _ _ (grp_kernel f) _.

(** ** Image of module homomorphism *)

Global Instance isleftsubmodule_grp_image {R : Ring}
  {M N : LeftModule R} (f : M $-> N)
  : IsLeftSubmodule (grp_image f).
R: Ring
M, N: LeftModule R
f: M $-> N
IsLeftSubmodule (grp_image f)
Proof.
R: Ring
M, N: LeftModule R
f: M $-> N
IsLeftSubmodule (grp_image f)
  srapply Build_IsLeftSubmodule.
R: Ring
M, N: LeftModule R
f: M $-> N
forall (r : R) (m : N),
grp_image f m -> grp_image f (lact r m)
  intros r m; apply Trunc_functor; intros [n p].
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: N
n: M
p: f n = m
{a : M & f a = lact r m}
  exists (lact r n).
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: N
n: M
p: f n = m
f (lact r n) = lact r m
  lhs nrapply lm_homo_lact.
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: N
n: M
p: f n = m
lact r (f n) = lact r m
  apply ap.
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: N
n: M
p: f n = m
f n = m
  exact p.
Defined.

Definition lm_image {R : Ring} {M N : LeftModule R} (f : M $-> N)
  : LeftSubmodule N
  := Build_LeftSubmodule _ _ (grp_image f) _.

(** ** Quotient Modules *)

(** The quotient abelian group of a module and a submodule has a natural ring action. *)
Global Instance isleftmodule_quotientabgroup {R : Ring}
  (M : LeftModule R) (N : LeftSubmodule M)
  : IsLeftModule R (QuotientAbGroup M N).
R: Ring
M: LeftModule R
N: LeftSubmodule M
IsLeftModule R (QuotientAbGroup M N)
Proof.
R: Ring
M: LeftModule R
N: LeftSubmodule M
IsLeftModule R (QuotientAbGroup M N)
  snrapply Build_IsLeftModule.
R: Ring
M: LeftModule R
N: LeftSubmodule M
R -> QuotientAbGroup M N -> QuotientAbGroup M N
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftHeteroDistribute ?lact plus plus
R: Ring
M: LeftModule R
N: LeftSubmodule M
RightHeteroDistribute ?lact plus plus
R: Ring
M: LeftModule R
N: LeftSubmodule M
HeteroAssociative ?lact ?lact ?lact mult
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftIdentity ?lact 1
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
R -> QuotientAbGroup M N -> QuotientAbGroup M N intros r.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
QuotientAbGroup M N -> QuotientAbGroup M N
    snrapply quotient_abgroup_rec.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
GroupHomomorphism M (QuotientAbGroup M N)
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
forall n : M, N n -> ?f n = mon_unit
    +
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
GroupHomomorphism M (QuotientAbGroup M N) refine (grp_quotient_map $o _).
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
M $-> M 
      snrapply Build_GroupHomomorphism.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
M -> M
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
IsSemiGroupPreserving ?f
      *
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
M -> M exact (lact r).
      *
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
IsSemiGroupPreserving (lact r) intros x y.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
x, y: M
lact r (sg_op x y) = sg_op (lact r x) (lact r y)
        apply lm_dist_l.
    +
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
forall n : M,
N n ->
(grp_quotient_map $o Build_GroupHomomorphism (lact r))
  n = mon_unit intros n Nn; simpl.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
Nn: N n
class_of (fun x y : M => N (sg_op (- x) y)) (lact r n) =
mon_unit
      apply qglue.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
Nn: N n
N (sg_op (- lact r n) mon_unit)
      apply issubgroup_in_inv_op.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
Nn: N n
N (lact r n)
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
Nn: N n
N mon_unit
      2: apply issubgroup_in_unit.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: M
Nn: N n
N (lact r n)
      by apply is_left_submodule.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftHeteroDistribute
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  plus plus intros r m n; revert m.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
n: QuotientAbGroup M N
forall m : QuotientAbGroup M N,
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact r))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact r n) mon_unit
        (is_left_submodule r n Nn) issubgroup_in_unit))
  (m + n) =
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact r))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact r n) mon_unit
        (is_left_submodule r n Nn) issubgroup_in_unit))
  m +
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact r))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact r n) mon_unit
        (is_left_submodule r n Nn) issubgroup_in_unit))
  n
    snrapply Quotient_ind_hprop; [exact _ | intros m; revert n].
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
m: M
forall n : QuotientAbGroup M N,
(fun
   q : M /
       in_cosetL
         {|
           normalsubgroup_subgroup := N;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup M N
         |} =>
 quotient_abgroup_rec N (QuotientAbGroup M N)
   (grp_quotient_map $o
    Build_GroupHomomorphism (lact r))
   (fun (n0 : M) (Nn : N n0) =>
    qglue
      (issubgroup_in_inv_op (lact r n0) mon_unit
         (is_left_submodule r n0 Nn)
         issubgroup_in_unit)) (q + n) =
 quotient_abgroup_rec N (QuotientAbGroup M N)
   (grp_quotient_map $o
    Build_GroupHomomorphism (lact r))
   (fun (n0 : M) (Nn : N n0) =>
    qglue
      (issubgroup_in_inv_op (lact r n0) mon_unit
         (is_left_submodule r n0 Nn)
         issubgroup_in_unit)) q +
 quotient_abgroup_rec N (QuotientAbGroup M N)
   (grp_quotient_map $o
    Build_GroupHomomorphism (lact r))
   (fun (n0 : M) (Nn : N n0) =>
    qglue
      (issubgroup_in_inv_op (lact r n0) mon_unit
         (is_left_submodule r n0 Nn)
         issubgroup_in_unit)) n)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := N;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup M N
        |}) m)
    snrapply Quotient_ind_hprop; [exact _ | intros n; simpl].
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
m, n: M
class_of (fun x y : M => N (sg_op (- x) y))
  (lact r (sg_op m n)) =
class_of (fun x y : M => N (sg_op (- x) y)) (lact r m) +
class_of (fun x y : M => N (sg_op (- x) y)) (lact r n)
    rapply ap.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r: R
m, n: M
lact r (sg_op m n) = sg_op (lact r m) (lact r n)
    apply lm_dist_l.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
RightHeteroDistribute
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  plus plus intros r s.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
forall c : QuotientAbGroup M N,
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact (r + s)))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact (r + s) n) mon_unit
        (is_left_submodule (r + s) n Nn)
        issubgroup_in_unit)) c =
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact r))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact r n) mon_unit
        (is_left_submodule r n Nn) issubgroup_in_unit))
  c +
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact s))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact s n) mon_unit
        (is_left_submodule s n Nn) issubgroup_in_unit))
  c
    snrapply Quotient_ind_hprop; [exact _| intros m; simpl].
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
m: M
class_of (fun x y : M => N (sg_op (- x) y))
  (lact (r + s) m) =
class_of (fun x y : M => N (sg_op (- x) y)) (lact r m) +
class_of (fun x y : M => N (sg_op (- x) y)) (lact s m)
    rapply ap.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
m: M
lact (r + s) m = sg_op (lact r m) (lact s m)
    apply lm_dist_r.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
HeteroAssociative
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  mult intros r s.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
forall z : QuotientAbGroup M N,
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact r))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact r n) mon_unit
        (is_left_submodule r n Nn) issubgroup_in_unit))
  (quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact s))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact s n) mon_unit
           (is_left_submodule s n Nn)
           issubgroup_in_unit)) z) =
quotient_abgroup_rec N (QuotientAbGroup M N)
  (grp_quotient_map $o
   Build_GroupHomomorphism (lact (r * s)))
  (fun (n : M) (Nn : N n) =>
   qglue
     (issubgroup_in_inv_op (lact (r * s) n) mon_unit
        (is_left_submodule (r * s) n Nn)
        issubgroup_in_unit)) z
    snrapply Quotient_ind_hprop; [exact _| intros m; simpl].
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
m: M
class_of (fun x y : M => N (sg_op (- x) y))
  (lact r (lact s m)) =
class_of (fun x y : M => N (sg_op (- x) y))
  (lact (r * s) m)
    rapply ap.
R: Ring
M: LeftModule R
N: LeftSubmodule M
r, s: R
m: M
lact r (lact s m) = lact (r * s) m
    apply lm_assoc.
  -
R: Ring
M: LeftModule R
N: LeftSubmodule M
LeftIdentity
  (fun r : R =>
   quotient_abgroup_rec N (QuotientAbGroup M N)
     (grp_quotient_map $o
      Build_GroupHomomorphism (lact r))
     (fun (n : M) (Nn : N n) =>
      qglue
        (issubgroup_in_inv_op (lact r n) mon_unit
           (is_left_submodule r n Nn)
           issubgroup_in_unit)
      :
      (grp_quotient_map $o
       Build_GroupHomomorphism (lact r)) n = mon_unit))
  1 snrapply Quotient_ind_hprop; [exact _| intros m; simpl].
R: Ring
M: LeftModule R
N: LeftSubmodule M
m: M
class_of (fun x y : M => N (sg_op (- x) y)) (lact 1 m) =
class_of (fun x y : M => N (sg_op (- x) y)) m
    rapply ap.
R: Ring
M: LeftModule R
N: LeftSubmodule M
m: M
lact 1 m = m
    apply lm_unit.
Defined.

(** We can therefore form the quotient module of a module by its submodule. *)
Definition QuotientLeftModule {R : Ring} (M : LeftModule R) (N : LeftSubmodule M)
  : LeftModule R
  := Build_LeftModule R (QuotientAbGroup M N) _.

Infix "/" := QuotientLeftModule : module_scope.

(** ** First Isomorphism Theorem *)

Local Open Scope module_scope.
Local Open Scope wc_iso_scope.

Definition rng_first_iso `{Funext} {R : Ring} {M N : LeftModule R} (f : M $-> N)
  : M / lm_kernel f ≅ lm_image f.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
M / lm_kernel f ≅ lm_image f
Proof.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
M / lm_kernel f ≅ lm_image f
  snrapply Build_LeftModuleIsomorphism'.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
GroupIsomorphism (M / lm_kernel f) (lm_image f)
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
forall (r : R) (x : M / lm_kernel f),
?f (lact r x) = lact r (?f x)
  1: rapply abgroup_first_iso.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
forall (r : R) (x : M / lm_kernel f),
abgroup_first_iso f (lact r x) =
lact r (abgroup_first_iso f x)
  intros r.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
forall x : M / lm_kernel f,
abgroup_first_iso f (lact r x) =
lact r (abgroup_first_iso f x)
  srapply Quotient_ind_hprop; intros m.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := lm_kernel f;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup M (lm_kernel f)
            |}) =>
 abgroup_first_iso f (lact r q) =
 lact r (abgroup_first_iso f q))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := lm_kernel f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup M (lm_kernel f)
        |}) m)
  apply path_sigma_hprop; simpl.
H: Funext
R: Ring
M, N: LeftModule R
f: M $-> N
r: R
m: M
f (lact r m) = lact r (f m)
  apply lm_homo_lact.
Defined.

(** ** Direct products *)

(** TODO: generalise to biproducts *)
(** The direct product of modules *)
Definition lm_prod {R : Ring} : LeftModule R -> LeftModule R -> LeftModule R.
R: Ring
LeftModule R -> LeftModule R -> LeftModule R
Proof.
R: Ring
LeftModule R -> LeftModule R -> LeftModule R
  intros M N.
R: Ring
M, N: LeftModule R
LeftModule R
  snrapply (Build_LeftModule R (ab_biprod M N)).
R: Ring
M, N: LeftModule R
IsLeftModule R (ab_biprod M N)
  snrapply Build_IsLeftModule.
R: Ring
M, N: LeftModule R
R -> ab_biprod M N -> ab_biprod M N
R: Ring
M, N: LeftModule R
LeftHeteroDistribute ?lact plus plus
R: Ring
M, N: LeftModule R
RightHeteroDistribute ?lact plus plus
R: Ring
M, N: LeftModule R
HeteroAssociative ?lact ?lact ?lact mult
R: Ring
M, N: LeftModule R
LeftIdentity ?lact 1
  -
R: Ring
M, N: LeftModule R
R -> ab_biprod M N -> ab_biprod M N intros r.
R: Ring
M, N: LeftModule R
r: R
ab_biprod M N -> ab_biprod M N
    apply functor_prod; exact (lact r).
  -
R: Ring
M, N: LeftModule R
LeftHeteroDistribute
  (fun r : R => functor_prod (lact r) (lact r)) plus
  plus intros r m n.
R: Ring
M, N: LeftModule R
r: R
m, n: ab_biprod M N
functor_prod (lact r) (lact r) (m + n) =
functor_prod (lact r) (lact r) m +
functor_prod (lact r) (lact r) n
    apply path_prod; apply lm_dist_l.
  -
R: Ring
M, N: LeftModule R
RightHeteroDistribute
  (fun r : R => functor_prod (lact r) (lact r)) plus
  plus intros r m n.
R: Ring
M, N: LeftModule R
r, m: R
n: ab_biprod M N
functor_prod (lact (r + m)) (lact (r + m)) n =
functor_prod (lact r) (lact r) n +
functor_prod (lact m) (lact m) n
    apply path_prod; apply lm_dist_r.
  -
R: Ring
M, N: LeftModule R
HeteroAssociative
  (fun r : R => functor_prod (lact r) (lact r))
  (fun r : R => functor_prod (lact r) (lact r))
  (fun r : R => functor_prod (lact r) (lact r)) mult intros r s m.
R: Ring
M, N: LeftModule R
r, s: R
m: ab_biprod M N
functor_prod (lact r) (lact r)
  (functor_prod (lact s) (lact s) m) =
functor_prod (lact (r * s)) (lact (r * s)) m
    apply path_prod; apply lm_assoc.
  -
R: Ring
M, N: LeftModule R
LeftIdentity
  (fun r : R => functor_prod (lact r) (lact r)) 1 intros r.
R: Ring
M, N: LeftModule R
r: ab_biprod M N
functor_prod (lact 1) (lact 1) r = r
    apply path_prod; apply lm_unit.
Defined.

Definition lm_prod_fst {R : Ring} {M N : LeftModule R} : lm_prod M N $-> M.
R: Ring
M, N: LeftModule R
lm_prod M N $-> M
Proof.
R: Ring
M, N: LeftModule R
lm_prod M N $-> M
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N: LeftModule R
GroupHomomorphism (lm_prod M N) M
R: Ring
M, N: LeftModule R
forall (r : R) (m : lm_prod M N),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M, N: LeftModule R
GroupHomomorphism (lm_prod M N) M apply grp_prod_pr1.
  -
R: Ring
M, N: LeftModule R
forall (r : R) (m : lm_prod M N),
grp_prod_pr1 (lact r m) = lact r (grp_prod_pr1 m) reflexivity.
Defined.

Definition lm_prod_snd {R : Ring} {M N : LeftModule R} : lm_prod M N $-> N.
R: Ring
M, N: LeftModule R
lm_prod M N $-> N
Proof.
R: Ring
M, N: LeftModule R
lm_prod M N $-> N
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N: LeftModule R
GroupHomomorphism (lm_prod M N) N
R: Ring
M, N: LeftModule R
forall (r : R) (m : lm_prod M N),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M, N: LeftModule R
GroupHomomorphism (lm_prod M N) N apply grp_prod_pr2.
  -
R: Ring
M, N: LeftModule R
forall (r : R) (m : lm_prod M N),
grp_prod_pr2 (lact r m) = lact r (grp_prod_pr2 m) reflexivity.
Defined.

Definition lm_prod_corec {R : Ring} {M N : LeftModule R} (L : LeftModule R)
  (f : L $-> M) (g : L $-> N)
  : L $-> lm_prod M N.
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
L $-> lm_prod M N
Proof.
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
L $-> lm_prod M N
  snrapply Build_LeftModuleHomomorphism.
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
GroupHomomorphism L (lm_prod M N)
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
forall (r : R) (m : L),
?lm_homo_map (lact r m) = lact r (?lm_homo_map m)
  -
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
GroupHomomorphism L (lm_prod M N) apply (grp_prod_corec f g).
  -
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
forall (r : R) (m : L),
grp_prod_corec f g (lact r m) =
lact r (grp_prod_corec f g m) intros r l.
R: Ring
M, N, L: LeftModule R
f: L $-> M
g: L $-> N
r: R
l: L
grp_prod_corec f g (lact r l) =
lact r (grp_prod_corec f g l)
    apply path_prod; apply lm_homo_lact.
Defined.

Global Instance hasbinaryproducts_leftmodule {R : Ring}
  : HasBinaryProducts (LeftModule R).
R: Ring
HasBinaryProducts (LeftModule R)
Proof.
R: Ring
HasBinaryProducts (LeftModule R)
  intros M N.
R: Ring
M, N: LeftModule R
BinaryProduct M N
  snrapply Build_BinaryProduct.
R: Ring
M, N: LeftModule R
LeftModule R
R: Ring
M, N: LeftModule R
?cat_binprod $-> M
R: Ring
M, N: LeftModule R
?cat_binprod $-> N
R: Ring
M, N: LeftModule R
forall z : LeftModule R,
(z $-> M) -> (z $-> N) -> z $-> ?cat_binprod
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f : z $-> M) (g : z $-> N),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f : z $-> M) (g : z $-> N),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f g : z $-> ?cat_binprod),
?cat_pr1 $o f $== ?cat_pr1 $o g ->
?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
  -
R: Ring
M, N: LeftModule R
LeftModule R exact (lm_prod M N).
  -
R: Ring
M, N: LeftModule R
lm_prod M N $-> M exact lm_prod_fst.
  -
R: Ring
M, N: LeftModule R
lm_prod M N $-> N exact lm_prod_snd.
  -
R: Ring
M, N: LeftModule R
forall z : LeftModule R,
(z $-> M) -> (z $-> N) -> z $-> lm_prod M N exact lm_prod_corec.
  -
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f : z $-> M) (g : z $-> N),
lm_prod_fst $o lm_prod_corec z f g $== f cbn; reflexivity.
  -
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f : z $-> M) (g : z $-> N),
lm_prod_snd $o lm_prod_corec z f g $== g cbn; reflexivity.
  -
R: Ring
M, N: LeftModule R
forall (z : LeftModule R) (f g : z $-> lm_prod M N),
lm_prod_fst $o f $== lm_prod_fst $o g ->
lm_prod_snd $o f $== lm_prod_snd $o g -> f $== g intros L f g p q a.
R: Ring
M, N, L: LeftModule R
f, g: L $-> lm_prod M N
p: lm_prod_fst $o f $== lm_prod_fst $o g
q: lm_prod_snd $o f $== lm_prod_snd $o g
a: L
f a = g a
    exact (path_prod' (p a) (q a)).
Defined.