Library UniMath.Algebra.Modules.Submodule

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.Modules.Core.

Definition issubsetwithsmul {R : hSet} {M : hSet} (smul : R → M → M) (A : hsubtype M) : UU :=
  ∏ r m, A m → A (smul r m).

Definition issubmodule {R : ring} {M : module R} (A : hsubtype M) : UU :=
  issubgr A × issubsetwithsmul (module_mult M) A.

Definition make_issubmodule {R : ring} {M : module R} {A : hsubtype M}
           (H1 : issubgr A) (H2 : issubsetwithsmul (module_mult M) A) : issubmodule A :=
  make_dirprod H1 H2.

Definition issubmodule_is {R : ring} {M : module R} (A : hsubtype M) : UU :=
  issubgr A × issubsetwithsmul (module_mult M) A.

Lemma isapropissubmodule {R : ring} {M : module R} (A : hsubtype M) : isaprop (issubmodule A).
Proof.
  intros. apply (isofhleveldirprod 1).
  - apply isapropissubgr.
  - apply impred. intro x.
    apply impred. intro m.
    apply impred. intro a.
    apply (pr2 (A _)).
Defined.


Definition submodule {R : ring} (M : module R) : UU := total2 (λ A : hsubtype M, issubmodule A).

Definition make_submodule {R : ring} {M : module R} :
  ∏ (t : hsubtype M), (λ A : hsubtype M, issubmodule A) t → ∑ A : hsubtype M, issubmodule A :=
  tpair (λ A : hsubtype M, issubmodule A).

Definition submoduletosubabgr {R : ring} {M : module R} : submodule M → @subabgr M :=
  λ A : _, make_subgr (pr1 A) (pr1 (pr2 A)).
Coercion submoduletosubabgr : submodule >-> subabgr.

Definition submodule_to_issubsetwithsmul {R : ring} {M : module R} (A : submodule M) :
  issubsetwithsmul (module_mult M) A :=
  pr2 (pr2 A).

Local Open Scope module_scope.

Definition submodule_smul {R : ring} {M : module R} {A : submodule M} (r : R) (m : A) : A.
Proof.
  use tpair.
  - exact (r × pr1 m).
  - exact (submodule_to_issubsetwithsmul A r (pr1 m) (pr2 m)).
Defined.

Definition carrierofasubmodule {R : ring} {M : module R} (A : submodule M) : module R.
Proof.
  use mult_to_module.
  - exact (carrierofasubabgr A).
  - exact (submodule_smul).
  - intros r a b. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_is_ldistr.
  - intros r s a. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_is_rdistr.
  - intros r s a. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_assoc.
  - intros f. apply (invmaponpathsincl _ (isinclpr1carrier A)). apply module_mult_unel2.
Defined.

Coercion carrierofasubmodule : submodule >-> module.
Lemma intersection_submodule {R : ring} {M : module R} {I : UU} (S : I → hsubtype M)
      (each_is_submodule : ∏ i : I, issubmodule (S i)) :
  issubmodule (subtype_intersection S).
Proof.
  intros.
  use make_issubmodule.
  - exact (intersection_subgr S (λ i, (pr1 (each_is_submodule i)))).
  - intros r m a i. exact (pr2 (each_is_submodule i) r m (a i)).
Qed.

Lemma ismodulefun_pr1 {R : ring} {M : module R} (A : submodule M) : @ismodulefun R A M pr1.
Proof.
  use make_ismodulefun.
  exact (pr1 (ismonoidfun_pr1 A)).
  intros r a. reflexivity.
Defined.

Definition submodule_incl {R : ring} {M : module R} (A : submodule M) : modulefun A M :=
  make_modulefun _ (ismodulefun_pr1 A).

Lemma issubmodule_kernel {R : ring} {A B : module R} (f : modulefun A B) :
  issubmodule (abgr_kernel_hsubtype (modulefun_to_monoidfun f)).
Proof.
  split.
  - apply abgr_Kernel_subabgr_issubgr.
  - intros r x p.
    cbn.
    rewrite (modulefun_to_islinear f).
    rewrite <- (module_mult_1 r), <- p.
    reflexivity.
Defined.

Definition module_kernel {R : ring} {A B : module R} (f : modulefun A B) : submodule A :=
  make_submodule _ (issubmodule_kernel f).

Definition module_kernel_eq {R : ring} {A B : module R} (f : modulefun A B) x :
  f (submodule_incl (module_kernel f) x) = unel B := (pr2 x).

Lemma issubmodule_image {R : ring} {A B : module R} (f : modulefun A B) :
  issubmodule (abgr_image_hsubtype (modulefun_to_monoidfun f)).
Proof.
  split.
  - apply abgr_image_issubgr.
  - intros r x. apply hinhfun. cbn. intro ap. induction ap as [a p].
    split with (r × a). now rewrite (modulefun_to_islinear f), <- p.
Defined.

Definition module_image {R : ring} {A B : module R} (f : modulefun A B) : submodule B :=
  make_submodule _ (issubmodule_image f).

Section submodule_helpers.

  Context {R : ring}
          {M : module R}
          (A : submodule M).

  Local Notation "x + y" := (@op _ x y).
  Local Notation "x - y" := (@op _ x (grinv _ y)).

  Definition submoduleadd (x y : M) : A x → A y → A (x + y).
  Proof.
    intros ax ay.
    exact (pr1 (pr1 (pr1 (pr2 A))) (make_carrier A x ax) (make_carrier A y ay)).
  Defined.

  Definition submodule0 : A (unel M) := pr2 (pr1 (pr1 (pr2 A))).

  Definition submoduleinv (x : M) : A x → A (grinv _ x) := λ ax, (pr2 (pr1 (pr2 A)) x ax).

  Local Open Scope module.

  Definition submodulemult (r : R) (m : M) : A m → A (r × m) := (pr2 (pr2 A) r m).

End submodule_helpers.