Library UniMath.Algebra.Modules.Quotient
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Algebra.Monoids_and_Groups.
Require Import UniMath.Algebra.Modules.Core.
Require Import UniMath.Algebra.Modules.Submodule.
Preliminaries: notion of an equivalence relation on a module that is closed under the module
structure
Section quotmod_rel.
Context {R : ring}
(M : module R).
Local Open Scope module_scope.
Definition isactionhrel (E : hrel M) : UU :=
∏ r a b, E a b → E (r × a) (r × b).
Definition module_eqrel : UU :=
∑ E : eqrel M, isbinophrel E × isactionhrel E.
Definition hrelmodule_eqrel (E : module_eqrel) : eqrel M := pr1 E.
Coercion hrelmodule_eqrel : module_eqrel >-> eqrel.
Definition binophrelmodule_eqrel (E : module_eqrel) : binopeqrel M := binopeqrelpair E (pr1 (pr2 E)).
Coercion binophrelmodule_eqrel : module_eqrel >-> binopeqrel.
Definition isactionhrelmodule_eqrel (E : module_eqrel) : isactionhrel E := pr2 (pr2 E).
Coercion isactionhrelmodule_eqrel : module_eqrel >-> isactionhrel.
Definition mk_module_eqrel (E : eqrel M) : isbinophrel E → isactionhrel E → module_eqrel :=
λ H0 H1, (E,,(H0,,H1)).
End quotmod_rel.
Context {R : ring}
(M : module R).
Local Open Scope module_scope.
Definition isactionhrel (E : hrel M) : UU :=
∏ r a b, E a b → E (r × a) (r × b).
Definition module_eqrel : UU :=
∑ E : eqrel M, isbinophrel E × isactionhrel E.
Definition hrelmodule_eqrel (E : module_eqrel) : eqrel M := pr1 E.
Coercion hrelmodule_eqrel : module_eqrel >-> eqrel.
Definition binophrelmodule_eqrel (E : module_eqrel) : binopeqrel M := binopeqrelpair E (pr1 (pr2 E)).
Coercion binophrelmodule_eqrel : module_eqrel >-> binopeqrel.
Definition isactionhrelmodule_eqrel (E : module_eqrel) : isactionhrel E := pr2 (pr2 E).
Coercion isactionhrelmodule_eqrel : module_eqrel >-> isactionhrel.
Definition mk_module_eqrel (E : eqrel M) : isbinophrel E → isactionhrel E → module_eqrel :=
λ H0 H1, (E,,(H0,,H1)).
End quotmod_rel.
Section quotmod_submodule.
Context {R : ring}
(M : module R)
(A : submodule M).
Local Notation "x + y" := (@op _ x y).
Local Notation "x - y" := (@op _ x (grinv _ y)).
Local Notation " - y" := (grinv _ y).
Local Notation "0" := (unel _).
Local Open Scope module_scope.
Definition eqrelsubmodule : eqrel M.
Proof.
use eqrelconstr.
- exact (λ m m', A (m - m')).
- intros x y z xy yz.
assert (K := submoduleadd A (x - y) (y - z) xy yz).
rewrite (assocax M) in K.
rewrite <- (assocax M (grinv _ y) y) in K.
rewrite grlinvax in K.
rewrite lunax in K.
exact K.
- intros x.
rewrite (grrinvax M x).
exact (submodule0 A).
- intros x y axy.
assert (K := submoduleinv A (x - y) axy).
rewrite grinvop in K.
rewrite grinvinv in K.
exact K.
Defined.
Definition module_eqrelsubmodule : module_eqrel M.
Proof.
use mk_module_eqrel.
- exact eqrelsubmodule.
- split.
+ intros a b c.
assert (H : a - b = c + a - (c + b)).
{
etrans; [|eapply (maponpaths (λ z, z - (c + b))); apply (commax M)];
rewrite assocax.
apply maponpaths.
now rewrite grinvop, commax, assocax, grlinvax, runax.
}
simpl in ×.
now rewrite H.
+ intros a b c.
assert (H : a - b = a + c - (b + c)).
{
rewrite assocax.
apply maponpaths.
now rewrite grinvop, <- (assocax M), grrinvax, lunax.
}
simpl in ×.
now rewrite H.
- intros r m m'.
assert (H : (r × m) - (r × m') = r × (m - m')) by
now rewrite module_inv_mult, module_mult_is_ldistr.
generalize (submodulemult A r (m - m')).
simpl in ×.
now rewrite H.
Defined.
End quotmod_submodule.
Context {R : ring}
(M : module R)
(A : submodule M).
Local Notation "x + y" := (@op _ x y).
Local Notation "x - y" := (@op _ x (grinv _ y)).
Local Notation " - y" := (grinv _ y).
Local Notation "0" := (unel _).
Local Open Scope module_scope.
Definition eqrelsubmodule : eqrel M.
Proof.
use eqrelconstr.
- exact (λ m m', A (m - m')).
- intros x y z xy yz.
assert (K := submoduleadd A (x - y) (y - z) xy yz).
rewrite (assocax M) in K.
rewrite <- (assocax M (grinv _ y) y) in K.
rewrite grlinvax in K.
rewrite lunax in K.
exact K.
- intros x.
rewrite (grrinvax M x).
exact (submodule0 A).
- intros x y axy.
assert (K := submoduleinv A (x - y) axy).
rewrite grinvop in K.
rewrite grinvinv in K.
exact K.
Defined.
Definition module_eqrelsubmodule : module_eqrel M.
Proof.
use mk_module_eqrel.
- exact eqrelsubmodule.
- split.
+ intros a b c.
assert (H : a - b = c + a - (c + b)).
{
etrans; [|eapply (maponpaths (λ z, z - (c + b))); apply (commax M)];
rewrite assocax.
apply maponpaths.
now rewrite grinvop, commax, assocax, grlinvax, runax.
}
simpl in ×.
now rewrite H.
+ intros a b c.
assert (H : a - b = a + c - (b + c)).
{
rewrite assocax.
apply maponpaths.
now rewrite grinvop, <- (assocax M), grrinvax, lunax.
}
simpl in ×.
now rewrite H.
- intros r m m'.
assert (H : (r × m) - (r × m') = r × (m - m')) by
now rewrite module_inv_mult, module_mult_is_ldistr.
generalize (submodulemult A r (m - m')).
simpl in ×.
now rewrite H.
Defined.
End quotmod_submodule.
Section quotmod_def.
Context {R : ring}
(M : module R)
(E : module_eqrel M).
Local Notation "x + y" := (@op _ x y).
Local Notation "x - y" := (@op _ x (grinv _ y)).
Local Open Scope module_scope.
Definition quotmod_abgr : abgr := abgrquot E.
Definition quotmod_ringact (r : R) : quotmod_abgr → quotmod_abgr.
Proof.
use setquotuniv.
- intros m.
exact (setquotpr E (r × m)).
- intros m m' Hmm'.
apply weqpathsinsetquot.
now apply isactionhrelmodule_eqrel.
Defined.
Definition quotmod_ringmap : R → ringofendabgr quotmod_abgr.
Proof.
intros r. use tpair.
+ exact (quotmod_ringact r).
+ use mk_ismonoidfun.
× use mk_isbinopfun.
use (setquotuniv2prop E (λ a b, hProppair _ _)); [use isasetsetquot|].
intros m m'.
unfold quotmod_ringact, setquotfun2;
rewrite (setquotunivcomm E), (setquotunivcomm E);
simpl; unfold setquotfun2;
rewrite (setquotuniv2comm E), (setquotuniv2comm E), (setquotunivcomm E).
apply weqpathsinsetquot.
assert (H : r × (m + m') = r × m + r × m') by use module_mult_is_ldistr.
simpl in H; rewrite H.
use eqrelrefl.
× unfold unel, quotmod_ringact; simpl; rewrite (setquotunivcomm E).
apply maponpaths.
apply module_mult_1.
Defined.
Definition quotmod_ringfun : ringfun R (ringofendabgr quotmod_abgr).
Proof.
unfold ringfun, rigfun.
use rigfunconstr.
- exact quotmod_ringmap.
- use mk_isrigfun.
all: use mk_ismonoidfun;
[ use mk_isbinopfun; intros r r' | ].
all: use monoidfun_paths; use funextfun.
all: use (setquotunivprop E (λ m, hProppair _ _)); [use isasetsetquot|].
all: intros m; simpl; unfold unel, quotmod_ringact, funcomp.
all: [> do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E)
| do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E)].
all: use maponpaths; simpl.
+ use module_mult_is_rdistr.
+ use module_mult_0_to_0.
+ use module_mult_assoc.
+ use module_mult_unel2.
Defined.
Definition quotmod_mod_struct : module_struct R quotmod_abgr := quotmod_ringfun.
Definition quotmod : module R.
Proof.
use modulepair.
- exact quotmod_abgr.
- exact quotmod_mod_struct.
Defined.
Notation "M / A" := (quotmod M (module_eqrelsubmodule M A)) : module_scope.
Notation "R-mod( M , N )" := (modulefun M N) : module_scope.
Definition quotmod_quotmap : R-mod(M, quotmod).
Proof.
use modulefunpair.
- exact (setquotpr E).
- now use (ismodulefunpair (mk_isbinopfun _)).
Defined.
Definition quotmoduniv
(N : module R)
(f : R-mod(M, N))
(is : iscomprelfun E f) :
R-mod(quotmod, N).
Proof.
use modulefunpair.
- now use (setquotuniv E _ f).
- use ismodulefunpair.
+ use mk_isbinopfun.
use (setquotuniv2prop E (λ m n, hProppair _ _)); [use isasetmodule|].
intros m m'.
simpl.
unfold op, setquotfun2.
rewrite setquotuniv2comm.
do 3 rewrite (setquotunivcomm E).
apply modulefun_to_isbinopfun.
+ intros r.
use (setquotunivprop E (λ m, hProppair _ _)); [use isasetmodule|].
intros m.
assert (H : r × quotmod_quotmap m = quotmod_quotmap (r × m)) by
use (! modulefun_to_islinear _ _ _).
simpl in H. simpl.
rewrite H.
do 2 rewrite (setquotunivcomm E).
apply modulefun_to_islinear.
Defined.
End quotmod_def.
Context {R : ring}
(M : module R)
(E : module_eqrel M).
Local Notation "x + y" := (@op _ x y).
Local Notation "x - y" := (@op _ x (grinv _ y)).
Local Open Scope module_scope.
Definition quotmod_abgr : abgr := abgrquot E.
Definition quotmod_ringact (r : R) : quotmod_abgr → quotmod_abgr.
Proof.
use setquotuniv.
- intros m.
exact (setquotpr E (r × m)).
- intros m m' Hmm'.
apply weqpathsinsetquot.
now apply isactionhrelmodule_eqrel.
Defined.
Definition quotmod_ringmap : R → ringofendabgr quotmod_abgr.
Proof.
intros r. use tpair.
+ exact (quotmod_ringact r).
+ use mk_ismonoidfun.
× use mk_isbinopfun.
use (setquotuniv2prop E (λ a b, hProppair _ _)); [use isasetsetquot|].
intros m m'.
unfold quotmod_ringact, setquotfun2;
rewrite (setquotunivcomm E), (setquotunivcomm E);
simpl; unfold setquotfun2;
rewrite (setquotuniv2comm E), (setquotuniv2comm E), (setquotunivcomm E).
apply weqpathsinsetquot.
assert (H : r × (m + m') = r × m + r × m') by use module_mult_is_ldistr.
simpl in H; rewrite H.
use eqrelrefl.
× unfold unel, quotmod_ringact; simpl; rewrite (setquotunivcomm E).
apply maponpaths.
apply module_mult_1.
Defined.
Definition quotmod_ringfun : ringfun R (ringofendabgr quotmod_abgr).
Proof.
unfold ringfun, rigfun.
use rigfunconstr.
- exact quotmod_ringmap.
- use mk_isrigfun.
all: use mk_ismonoidfun;
[ use mk_isbinopfun; intros r r' | ].
all: use monoidfun_paths; use funextfun.
all: use (setquotunivprop E (λ m, hProppair _ _)); [use isasetsetquot|].
all: intros m; simpl; unfold unel, quotmod_ringact, funcomp.
all: [> do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E)
| do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E)].
all: use maponpaths; simpl.
+ use module_mult_is_rdistr.
+ use module_mult_0_to_0.
+ use module_mult_assoc.
+ use module_mult_unel2.
Defined.
Definition quotmod_mod_struct : module_struct R quotmod_abgr := quotmod_ringfun.
Definition quotmod : module R.
Proof.
use modulepair.
- exact quotmod_abgr.
- exact quotmod_mod_struct.
Defined.
Notation "M / A" := (quotmod M (module_eqrelsubmodule M A)) : module_scope.
Notation "R-mod( M , N )" := (modulefun M N) : module_scope.
Definition quotmod_quotmap : R-mod(M, quotmod).
Proof.
use modulefunpair.
- exact (setquotpr E).
- now use (ismodulefunpair (mk_isbinopfun _)).
Defined.
Definition quotmoduniv
(N : module R)
(f : R-mod(M, N))
(is : iscomprelfun E f) :
R-mod(quotmod, N).
Proof.
use modulefunpair.
- now use (setquotuniv E _ f).
- use ismodulefunpair.
+ use mk_isbinopfun.
use (setquotuniv2prop E (λ m n, hProppair _ _)); [use isasetmodule|].
intros m m'.
simpl.
unfold op, setquotfun2.
rewrite setquotuniv2comm.
do 3 rewrite (setquotunivcomm E).
apply modulefun_to_isbinopfun.
+ intros r.
use (setquotunivprop E (λ m, hProppair _ _)); [use isasetmodule|].
intros m.
assert (H : r × quotmod_quotmap m = quotmod_quotmap (r × m)) by
use (! modulefun_to_islinear _ _ _).
simpl in H. simpl.
rewrite H.
do 2 rewrite (setquotunivcomm E).
apply modulefun_to_islinear.
Defined.
End quotmod_def.
Section from_submodule.
Context {R : ring}
(M : module R)
(A : submodule M).
Notation "R-mod( M , N )" := (modulefun M N) : module_scope.
Local Open Scope module_scope.
Definition quotmoduniv_submodule
(N : module R)
(f : R-mod(M, N))
(is : iscomprelfun (module_eqrelsubmodule M A) f) :
R-mod(quotmod M (module_eqrelsubmodule M A), N) :=
quotmoduniv M (module_eqrelsubmodule M A) N f is.
End from_submodule.
Context {R : ring}
(M : module R)
(A : submodule M).
Notation "R-mod( M , N )" := (modulefun M N) : module_scope.
Local Open Scope module_scope.
Definition quotmoduniv_submodule
(N : module R)
(f : R-mod(M, N))
(is : iscomprelfun (module_eqrelsubmodule M A) f) :
R-mod(quotmod M (module_eqrelsubmodule M A), N) :=
quotmoduniv M (module_eqrelsubmodule M A) N f is.
End from_submodule.