The category of R
-modules #
Module.{v} R
is the category of bundled R
-modules with carrier in the universe v
. We show
that it is preadditive and show that being an isomorphism, monomorphism and epimorphism is
equivalent to being a linear equivalence, an injective linear map and a surjective linear map,
respectively.
Implementation details #
To construct an object in the category of R
-modules from a type M
with an instance of the
module
typeclass, write of R M
. There is a coercion in the other direction.
Similarly, there is a coercion from morphisms in Module R
to linear maps.
Unfortunately, Lean is not smart enough to see that, given an object M : Module R
, the expression
of R M
, where we coerce M
to the carrier type, is definitionally equal to M
itself.
This means that to go the other direction, i.e., from linear maps/equivalences to (iso)morphisms
in the category of R
-modules, we have to take care not to inadvertently end up with an
of R M
where M
is already an object. Hence, given f : M →ₗ[R] N
,
- if
M N : Module R
, simply usef
; - if
M : Module R
andN
is an unbundledR
-module, use↿f
oras_hom_left f
; - if
M
is an unbundledR
-module andN : Module R
, use↾f
oras_hom_right f
; - if
M
andN
are unbundledR
-modules, use↟f
oras_hom f
.
Similarly, given f : M ≃ₗ[R] N
, use to_Module_iso
, to_Module_iso'_left
, to_Module_iso'_right
or to_Module_iso'
, respectively.
The arrow notations are localized, so you may have to open_locale Module
to use them. Note that
the notation for as_hom_left
clashes with the notation used to promote functions between types to
morphisms in the category Type
, so to avoid confusion, it is probably a good idea to avoid having
the locales Module
and category_theory.Type
open at the same time.
If you get an error when trying to apply a theorem and the convert
tactic produces goals of the
form M = of R M
, then you probably used an incorrect variant of as_hom
or to_Module_iso
.
Equations
- Module.has_coe_to_sort R = {S := Type v, coe := Module.carrier _inst_1}
Equations
- Module.has_forget_to_AddCommGroup R = {forget₂ := {obj := λ (M : Module R), AddCommGroup.of ↥M, map := λ (M₁ M₂ : Module R) (f : M₁ ⟶ M₂), linear_map.to_add_monoid_hom f, map_id' := _, map_comp' := _}, forget_comp := _}
Equations
- Module.has_zero R = {zero := Module.of R punit (punit.semimodule R)}
Equations
- Module.inhabited R = {default := 0}
Forgetting to the underlying type and then building the bundled object returns the original module.
Equations
- M.of_self_iso = {hom := 𝟙 M, inv := 𝟙 M, hom_inv_id' := _, inv_hom_id' := _}
Equations
- Module.category_theory.limits.has_zero_object = {zero := 0, unique_to := λ (X : Module R), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : Module R), {to_inhabited := {default := 0}, uniq := _}}
Reinterpreting a linear map in the category of R
-modules.
Equations
Reinterpreting a linear map in the category of R
-modules.
Equations
Reinterpreting a linear map in the category of R
-modules.
Equations
Build an isomorphism in the category Module R
from a linear_equiv
between module
s.
Equations
- e.to_Module_iso = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category Module R
from a linear_equiv
between module
s.
This version is better than linear_equiv_to_Module_iso
when applicable, because Lean can't see
Module.of R M
is defeq to M
when M : Module R
.
Equations
- i.to_Module_iso' = {hom := ↑i, inv := ↑(i.symm), hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category Module R
from a linear_equiv
between module
s.
This version is better than linear_equiv_to_Module_iso
when applicable, because Lean can't see
Module.of R M
is defeq to M
when M : Module R
.
Equations
- e.to_Module_iso'_left = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category Module R
from a linear_equiv
between module
s.
This version is better than linear_equiv_to_Module_iso
when applicable, because Lean can't see
Module.of R M
is defeq to M
when M : Module R
.
Equations
- e.to_Module_iso'_right = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
Build a linear_equiv
from an isomorphism in the category Module R
.
linear equivalences between module
s are the same as (isomorphic to) isomorphisms
in Module
Equations
- linear_equiv_iso_Module_iso = {hom := λ (e : X ≃ₗ[R] Y), e.to_Module_iso, inv := λ (i : Module.of R X ≅ Module.of R Y), i.to_linear_equiv, hom_inv_id' := _, inv_hom_id' := _}
Equations
- Module.category_theory.preadditive = {hom_group := λ (P Q : Module R), linear_map.add_comm_group, add_comp' := _, comp_add' := _}