Library UniMath.CategoryTheory.categories.modules
Authors:
- Anthony Bordg, March-April 2017
- Langston Barrett (@siddharthist), November-December 2017
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.Algebra.Modules.
Require Import UniMath.Algebra.Modules.Examples.
Require Import UniMath.CategoryTheory.limits.zero.
Contents:
- The category of (left) R-modules (mod_category)
- Mod is a univalent category (is_univalent_mod)
- Abelian structure
- Zero object and zero arrow
- Preadditive structure
- Additive structure
The category of (left) R-modules (mod_category)
Definition mod_precategory_ob_mor : precategory_ob_mor :=
make_precategory_ob_mor (module R) (λ M N, modulefun M N).
Definition mod_precategory_data : precategory_data :=
make_precategory_data
mod_precategory_ob_mor (λ (M : module R), (idfun M,, id_modulefun M))
(fun M N P ⇒ @modulefun_comp R M N P).
Lemma is_precategory_mod_precategory_data :
is_precategory (mod_precategory_data).
Proof.
apply is_precategory_one_assoc_to_two.
apply make_dirprod.
- apply make_dirprod.
+ intros M N f.
use total2_paths_f.
× apply funextfun. intro x. apply idpath.
× apply isapropismodulefun.
+ intros M N f.
use total2_paths_f.
× apply funextfun. intro x. apply idpath.
× apply isapropismodulefun.
- intros M N P Q f g h.
use total2_paths_f.
+ apply funextfun. intro x.
unfold compose. cbn.
rewrite funcomp_assoc.
apply idpath.
+ apply isapropismodulefun.
Defined.
Definition mod_precategory : precategory :=
make_precategory (mod_precategory_data) (is_precategory_mod_precategory_data).
Definition has_homsets_mod : has_homsets mod_precategory := isasetmodulefun.
Definition mod_category : category := make_category mod_precategory has_homsets_mod.
Definition mor_to_modulefun {M N : ob mod_category} : mod_category⟦M, N⟧ → modulefun M N := idfun _.
Mod is a univalent category (Mod_is_univalent)
Definition modules_univalence_weq (M N : mod_precategory) : (M ╝ N) ≃ (moduleiso' M N).
Proof.
use weqbandf.
- apply abgr_univalence.
- intro e.
use invweq.
induction M. induction N. cbn in e. induction e.
use weqimplimpl.
+ intro i.
use total2_paths2_f.
× use funextfun. intro r.
use total2_paths2_f.
apply funextfun. intro x. exact (i r x).
apply isapropismonoidfun.
× apply isapropisrigfun.
+ intro i. cbn.
intros r x.
unfold idmonoidiso. cbn in i.
induction i.
apply idpath.
+ apply isapropislinear.
+ apply isasetrigfun.
Defined.
Definition modules_univalence_map (M N : mod_precategory) : (M = N) → (moduleiso M N).
Proof.
intro p.
induction p.
exact (idmoduleiso M).
Defined.
Definition modules_univalence_map_isweq (M N : mod_precategory) : isweq (modules_univalence_map M N).
Proof.
use isweqhomot.
- exact (weqcomp (weqcomp (total2_paths_equiv _ M N) (modules_univalence_weq M N)) (moduleiso'_to_moduleweq_iso M N)).
- intro p.
induction p.
apply (pathscomp0 weqcomp_to_funcomp_app).
apply idpath.
- apply weqproperty.
Defined.
Definition modules_univalence (M N : mod_precategory) : (M = N) ≃ (moduleiso M N).
Proof.
use make_weq.
- exact (modules_univalence_map M N).
- exact (modules_univalence_map_isweq M N).
Defined.
Equivalence between isomorphisms and moduleiso in Mod R
Lemma moduleisweq_iso {M N : ob mod_precategory} (f : iso M N) :
isweq (pr1modulefun (morphism_from_iso f)).
Proof.
use (isweq_iso (pr1modulefun (morphism_from_iso f))).
- exact (pr1modulefun (inv_from_iso f)).
- intro; set (T:= iso_inv_after_iso f).
apply subtypeInjectivity in T.
+ apply (toforallpaths _ _ _ T).
+ intro; apply isapropismodulefun.
- intro; set (T:= iso_after_iso_inv f).
apply subtypeInjectivity in T.
+ apply (toforallpaths _ _ _ T).
+ intro; apply isapropismodulefun.
Defined.
Lemma iso_moduleiso (M N : ob mod_precategory) : iso M N → moduleiso M N.
Proof.
intro f.
use make_moduleiso.
- use make_weq.
+ exact (pr1modulefun (morphism_from_iso f)).
+ exact (moduleisweq_iso f).
- exact (modulefun_ismodulefun (morphism_from_iso f)).
Defined.
Lemma moduleiso_is_iso {M N : ob mod_precategory} (f : moduleiso M N) :
@is_iso _ M N (moduleiso_to_modulefun f).
Proof.
apply (is_iso_qinv (C:= mod_precategory) _ (make_modulefun (invmoduleiso f) (pr2 (invmoduleiso f)))).
split; use total2_paths_f.
+ apply funextfun. intro.
unfold funcomp, idfun.
apply homotinvweqweq.
+ apply isapropismodulefun.
+ apply funextfun. intro.
apply homotweqinvweq.
+ apply isapropismodulefun.
Defined.
Lemma moduleiso_iso (M N : ob mod_precategory) : moduleiso M N → iso M N.
Proof.
intro f.
use make_iso.
- exact (moduleiso_to_modulefun f).
- exact (moduleiso_is_iso f).
Defined.
Lemma moduleiso_isweq_iso (M N : ob mod_precategory) : isweq (@moduleiso_iso M N).
Proof.
apply (isweq_iso _ (iso_moduleiso M N)).
- intro.
apply subtypePath.
+ intro; apply isapropismodulefun.
+ unfold moduleiso_iso, iso_moduleiso.
use total2_paths_f.
× apply idpath.
× apply isapropisweq.
- intro; unfold iso_moduleiso, moduleiso_iso.
use total2_paths_f.
+ apply idpath.
+ apply isaprop_is_iso.
Defined.
Definition moduleiso_weq_iso (M N : mod_precategory) : (moduleiso M N) ≃ (iso M N) :=
make_weq (moduleiso_iso M N) (moduleiso_isweq_iso M N).
Definition mod_precategory_idtoisweq_iso :
∏ M N : mod_precategory, isweq (fun p : M = N ⇒ idtoiso p).
Proof.
intros M N.
use (isweqhomot (weqcomp (modules_univalence M N) (moduleiso_weq_iso M N)) _).
- intro p.
induction p.
use (pathscomp0 weqcomp_to_funcomp_app). cbn.
use total2_paths_f.
+ apply idpath.
+ apply isaprop_is_iso.
- apply weqproperty.
Defined.
Definition is_univalent_mod : is_univalent mod_precategory :=
make_is_univalent mod_precategory_idtoisweq_iso has_homsets_mod.
Definition univalent_category_mod_precategory : univalent_category
:= make_univalent_category mod_precategory is_univalent_mod.
Abelian structure
Zero object and zero arrow
- The zero object (0) is the zero abelian group, considered as a module.
- The type (hSet) Hom(0, M) is contractible, the center is the zero map.
- The type (hSet) Hom(M, 0) is contractible, the center is the zero map.
Zero in abelian category
Lemma iscontrfromzero_module (M : mod_category) : iscontr (mod_category⟦zero_module R, M⟧).
Proof.
refine (unelmodulefun _ _,, _).
intros f; apply modulefun_paths.
apply funextfun; intro x.
unfold unelmodulefun; cbn.
refine (!maponpaths (fun z ⇒ (pr1 f) z)
(isProofIrrelevantUnit (@unel (zero_module R)) _ ) @ _).
apply (monoidfununel (modulefun_to_monoidfun f)).
Defined.
Proof.
refine (unelmodulefun _ _,, _).
intros f; apply modulefun_paths.
apply funextfun; intro x.
unfold unelmodulefun; cbn.
refine (!maponpaths (fun z ⇒ (pr1 f) z)
(isProofIrrelevantUnit (@unel (zero_module R)) _ ) @ _).
apply (monoidfununel (modulefun_to_monoidfun f)).
Defined.
The set of maps M -> 0 is contractible, it only contains the zero morphism.
Lemma iscontrtozero_module (M : mod_category) : iscontr (mod_category⟦M, zero_module R⟧).
Proof.
refine (unelmodulefun _ _,, _).
intros f; apply modulefun_paths.
apply funextfun.
exact (fun x ⇒ isProofIrrelevantUnit _ _).
Defined.
Lemma isZero_zero_module : @isZero mod_category (zero_module R).
Proof.
exact (@make_isZero mod_category (zero_module _)
iscontrfromzero_module iscontrtozero_module).
Defined.
Definition mod_category_Zero : Zero mod_category :=
@make_Zero mod_category (zero_module _) isZero_zero_module.
Proof.
refine (unelmodulefun _ _,, _).
intros f; apply modulefun_paths.
apply funextfun.
exact (fun x ⇒ isProofIrrelevantUnit _ _).
Defined.
Lemma isZero_zero_module : @isZero mod_category (zero_module R).
Proof.
exact (@make_isZero mod_category (zero_module _)
iscontrfromzero_module iscontrtozero_module).
Defined.
Definition mod_category_Zero : Zero mod_category :=
@make_Zero mod_category (zero_module _) isZero_zero_module.