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
.
- carrier : Type ?
- is_add_comm_group : add_comm_group self.carrier
- is_module : module R self.carrier
The category of R-modules and their morphisms.
Note that in the case of R = ℤ
, we can not
impose here that the ℤ
-multiplication field from the module structure is defeq to the one coming
from the is_add_comm_group
structure (contrary to what we do for all module structures in
mathlib), which creates some difficulties down the road.
Instances for Module
- Module.has_sizeof_inst
- Module.has_coe_to_sort
- Module.Module_category
- Module.Module_concrete_category
- Module.has_forget_to_AddCommGroup
- Module.inhabited
- Module.category_theory.limits.has_zero_object
- Module.category_theory.preadditive
- Module.category_theory.linear
- Module.has_coe
- Algebra.has_forget_to_Module
- Module.has_limits_of_size
- Module.has_limits
- Module.category_theory.abelian
- Module.monoidal_category
- Module.symmetric_category
- Module.category_theory.monoidal_preadditive
- Module.category_theory.monoidal_linear
- Module.category_theory.monoidal_closed
- FinVect.Module.category_theory.has_forget₂
- Module.well_powered_Module
- Module.category_theory.limits.has_binary_biproducts
- Module.category_theory.limits.has_finite_biproducts
- Module.colimits.has_colimits_Module
- Module.colimits.has_colimits_Module'
- Module.colimits.has_colimits_Module''
- Module.Module_enough_projectives
Equations
- Module.has_coe_to_sort R = {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.linear_map_class R M N = {coe := λ (f : M ⟶ N), ⇑f, coe_injective' := _, map_add := _, map_smulₛₗ := _}
The object in the category of R-modules associated to an R-module
Instances for Module.of
Instances for ↥Module.of
Typecheck a linear_map
as a morphism in Module R
.
Equations
- Module.of_hom f = f
Equations
- Module.inhabited R = {default := Module.of R punit punit.module}
Equations
- Module.of_unique R = i
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' := _}
Reinterpreting a linear map in the category of R
-modules.
Equations
Reinterpreting a linear map in the category of R
-modules.
Equations
Instances for Module.as_hom_right
Reinterpreting a linear map in the category of R
-modules.
Equations
Instances for Module.as_hom_left
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' := _}
Equations
- Module.category_theory.linear = {hom_module := λ (X Y : Module S), linear_map.module, smul_comp' := _, comp_smul' := _}