Library UniMath.Algebra.Modules.Multimodules
Authors Langston Barrett (@siddharthist), November-December 2017
Require Import UniMath.Algebra.Modules.Core.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.Sets.
Contents
- Definitions
- Propositions
- Multimodule morphisms
- Multilinearity
- Multimodule morphisms
Definitions
Definition arecompatibleactions {R S G}
(mr : module_struct R G) (ms : module_struct S G) :=
let m1 := module_mult (G,, mr) in
let m2 := module_mult (G,, ms)
in ∏ (r1 : R) (r2 : S), (m1 r1 ∘ m2 r2 = m2 r2 ∘ m1 r1)%functions.
Definition multimodule_struct {I : UU} {rings : I → ring} {G : abgr}
(structs : ∏ i : I, module_struct (rings i) G) :=
∏ (i1 i2 : I) (ne : (i1 = i2) → hfalse),
arecompatibleactions (structs i1) (structs i2).
Definition multimodule {I : UU} (rings : I → ring) : UU
:= ∑ G (ms : ∏ i : I, module_struct (rings i) G), multimodule_struct ms.
(mr : module_struct R G) (ms : module_struct S G) :=
let m1 := module_mult (G,, mr) in
let m2 := module_mult (G,, ms)
in ∏ (r1 : R) (r2 : S), (m1 r1 ∘ m2 r2 = m2 r2 ∘ m1 r1)%functions.
Definition multimodule_struct {I : UU} {rings : I → ring} {G : abgr}
(structs : ∏ i : I, module_struct (rings i) G) :=
∏ (i1 i2 : I) (ne : (i1 = i2) → hfalse),
arecompatibleactions (structs i1) (structs i2).
Definition multimodule {I : UU} (rings : I → ring) : UU
:= ∑ G (ms : ∏ i : I, module_struct (rings i) G), multimodule_struct ms.
We define a few things in the same way for multimodules as we did for modules
Definition pr1multimodule {I : UU} {rings : I → ring} (MM : multimodule rings) : abgr
:= pr1 MM.
Coercion pr1multimodule : multimodule >-> abgr.
Definition pr2multimodule {I : UU} {rings : I → ring} (MM : multimodule rings)
: ∏ i : I, module_struct (rings i) (pr1multimodule MM) := (pr1 (pr2 MM)).
Definition pr3bimodule {I : UU} {rings : I → ring} (MM : multimodule rings)
: multimodule_struct (pr2multimodule MM) := (pr2 (pr2 MM)).
Definition ith_module {I : UU} {rings : I → ring} (MM : multimodule rings) (i : I)
: module (rings i) := (pr1multimodule MM,, pr2multimodule MM i).
Lemma isaproparecompatibleactions
{R S G} (mr : module_struct R G) (ms : module_struct S G) :
isaprop (arecompatibleactions mr ms).
Proof.
apply (impredtwice 1); intros r s.
apply (isofhlevelweqb 1
(Y := (module_mult (G,, mr) r ∘ module_mult (G,, ms) s ¬
module_mult (G,, ms) s ∘ module_mult (G,, mr) r))).
apply invweq.
apply weqfunextsec.
apply (impred 1); intros x.
apply (pr2 (pr1 (pr1 G))).
Defined.
Lemma isapropmultimodule_struct {I : UU} {rings : I → ring} {G : abgr}
(structs : ∏ i : I, module_struct (rings i) G) :
isaprop (multimodule_struct structs).
Proof.
apply (impredtwice 1); intros i1 i2.
apply impredfun.
apply isaproparecompatibleactions.
Defined.
Multimodule morphisms
Multilinearity
Definition ismultilinear {I : UU} {rings : I → ring} {MM NN : multimodule rings} (f : MM → NN)
:= ∏ i : I, @islinear (rings i) (ith_module MM i) (ith_module NN i) f.
Definition multilinearfun {I : UU} {rings : I → ring} (MM NN : multimodule rings)
: UU := ∑ f : MM → NN, ismultilinear f.
Definition make_multilinearfun {I : UU} {rings : I → ring} {MM NN : multimodule rings}
(f : MM → NN) (is : ismultilinear f) : multilinearfun MM NN
:= tpair _ f is.
Definition pr1multilinearfun {I : UU} {rings : I → ring} {MM NN : multimodule rings}
(f : multilinearfun MM NN) : MM → NN := pr1 f.
Coercion pr1multilinearfun : multilinearfun >-> Funclass.
Definition ith_linearfun {I : UU} {rings : I → ring} {MM NN : multimodule rings}
(f : multilinearfun MM NN) (i : I) :
linearfun (ith_module MM i) (ith_module NN i) :=
(pr1 f,, pr2 f i).
Definition ismultilinearfuncomp {I : UU} {rings : I → ring}
{MM NN PP : multimodule rings} (f : multilinearfun MM NN)
(g : multilinearfun NN PP) : ismultilinear (pr1 g ∘ pr1 f)%functions :=
(fun i ⇒ islinearfuncomp (ith_linearfun f i) (ith_linearfun g i)).
Definition multilinearfuncomp {I : UU} {rings : I → ring}
{MM NN PP : multimodule rings} (f : multilinearfun MM NN)
(g : multilinearfun NN PP) : multilinearfun MM PP :=
(funcomp f g,, ismultilinearfuncomp f g).
Definition ismultimodulefun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : MM → NN) : UU :=
(isbinopfun f) × (ismultilinear f).
Lemma isapropismultimodulefun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : MM → NN) : isaprop (ismultimodulefun f).
Proof.
refine (@isofhleveldirprod 1 (isbinopfun f) (ismultilinear f)
(isapropisbinopfun f) _).
do 3 (apply (impred 1 _); intros ?).
apply setproperty.
Defined.
Definition multimodulefun {I : UU} {rings : I → ring}
(MM NN : multimodule rings) : UU := ∑ f : MM → NN, ismultimodulefun f.
Definition make_multimodulefun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : MM → NN) (is : ismultimodulefun f) :
multimodulefun MM NN := tpair _ f is.
Definition pr1multimodulefun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) : MM → NN := pr1 f.
Coercion pr1multimodulefun : multimodulefun >-> Funclass.
Definition ith_modulefun {I : UU} {rings : I → ring} {MM NN : multimodule rings}
(f : multimodulefun MM NN) (i : I) :
modulefun (ith_module MM i) (ith_module NN i) :=
(pr1 f,, (make_dirprod (pr1 (pr2 f)) (pr2 (pr2 f) i))).
Definition multimodulefun_to_isbinopfun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) :
isbinopfun (pr1multimodulefun f) := pr1 (pr2 f).
Definition multimodulefun_to_binopfun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) :
binopfun MM NN := make_binopfun (pr1multimodulefun f)
(multimodulefun_to_isbinopfun f).
Definition multimodulefun_to_ith_islinear {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) (i : I) :
islinear (ith_modulefun f i) := pr2 (pr2 (ith_modulefun f i)).
Definition multimodulefun_to_ith_linearfun {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) (i : I) :
linearfun (ith_module MM i) (ith_module NN i) :=
make_linearfun (ith_modulefun f i) (multimodulefun_to_ith_islinear f i).
Properties of the ring actions
Definition multimodule_ith_mult {I : UU} {rings : I → ring}
(MM : multimodule rings) (i : I) : (rings i) → MM → MM :=
@module_mult (rings i) (ith_module MM i).
If you take the underlying group of the ith module, its the same as the
underlying group of the multimodule.
Lemma multimodule_same_abgrp {I : UU} {rings : I → ring}
(MM : multimodule rings) (i : I) : @paths abgr MM (ith_module MM i).
Proof.
reflexivity.
Defined.
(MM : multimodule rings) (i : I) : @paths abgr MM (ith_module MM i).
Proof.
reflexivity.
Defined.
Multiplying something by 0 always gives you the identity.
Equationally, 0R * x = 0G for all x.
Definition multimodule_ith_mult_0_to_0 {I : UU} {rings : I → ring}
{MM : multimodule rings} (i : I) (x : MM) :
multimodule_ith_mult MM i (@ringunel1 (rings i)) x = @unel MM :=
@module_mult_0_to_0 (rings i) (ith_module MM i) x.
Definition multimodulefun_unel {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) :
f (unel MM) = unel NN.
Abort.
{MM : multimodule rings} (i : I) (x : MM) :
multimodule_ith_mult MM i (@ringunel1 (rings i)) x = @unel MM :=
@module_mult_0_to_0 (rings i) (ith_module MM i) x.
Definition multimodulefun_unel {I : UU} {rings : I → ring}
{MM NN : multimodule rings} (f : multimodulefun MM NN) :
f (unel MM) = unel NN.
Abort.