The category of R
-modules #
ModuleCat.{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.
The roundtrip ↑(of R M)
is definitionally equal to M
itself (when M
is a type with Module
instance), and so is of R ↑M
(when M : ModuleCat R M
).
The morphisms are given their own type, not identified with LinearMap
.
There is a cast from morphisms in Module R
to linear maps, written f.hom
(ModuleCat.Hom.hom
).
To go from linear maps to morphisms in Module R
, use ModuleCat.ofHom
.
Similarly, given an isomorphism f : M ≅ N
use f.toLinearEquiv
and given a linear equiv
f : M ≃ₗ[R] N
, use f.toModuleIso
.
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 isAddCommGroup
structure (contrary to what we do for all module structures in
mathlib), which creates some difficulties down the road.
- carrier : Type v
the underlying type of an object in
ModuleCat R
- isAddCommGroup : AddCommGroup ↑self
- isModule : Module R ↑self
Instances For
An alias for ModuleCat.{max u₁ u₂}
, to deal around unification issues.
Since the universe the ring lives in can be inferred, we put that last.
Equations
- ModuleCatMax R = ModuleCat R
Instances For
Equations
- ModuleCat.instCoeSortType R = { coe := ModuleCat.carrier }
The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of ModuleCat R
.
Equations
- ModuleCat.of R X = ModuleCat.mk✝ X
Instances For
Equations
Convenience shortcut for ModuleCat.hom_bijective.injective
.
Convenience shortcut for ModuleCat.hom_bijective.surjective
.
Typecheck a LinearMap
as a morphism in ModuleCat R
.
Equations
- ModuleCat.ofHom f = { hom := f }
Instances For
Alias of ModuleCat.ofHom
.
Typecheck a LinearMap
as a morphism in ModuleCat R
.
Equations
Instances For
Equations
- ModuleCat.instInhabited R = { default := ModuleCat.of R R }
Equations
- One or more equations did not get rendered due to their size.
Equations
- ModuleCat.instAddCommGroupObjForget R = inferInstance
Equations
- ModuleCat.instModuleObjForget R = inferInstance
Equations
- One or more equations did not get rendered due to their size.
Equations
- ModuleCat.instInhabited_1 R = { default := ModuleCat.of R PUnit.{?u.15 + 1} }
Forgetting to the underlying type and then building the bundled object returns the original module.
Equations
- M.ofSelfIso = { hom := CategoryTheory.CategoryStruct.id M, inv := CategoryTheory.CategoryStruct.id M, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Reinterpreting a linear map in the category of R
-modules
Equations
- ModuleCat.«term↟_» = Lean.ParserDescr.node `ModuleCat.«term↟_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↟") (Lean.ParserDescr.cat `term 1024))
Instances For
Alias of ModuleCat.ofHom_apply
.
Alias of ModuleCat.ofHom
.
Typecheck a LinearMap
as a morphism in ModuleCat R
.
Equations
Instances For
Alias of ModuleCat.ofHom
.
Typecheck a LinearMap
as a morphism in ModuleCat R
.
Equations
Instances For
Reinterpreting a linear map in the category of R
-modules.
This notation is deprecated: use ↟
instead.
Equations
- ModuleCat.«term↾_» = Lean.ParserDescr.node `ModuleCat.«term↾_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 1024))
Instances For
Reinterpreting a linear map in the category of R
-modules.
This notation is deprecated: use ↟
instead.
Equations
- ModuleCat.«term↿_» = Lean.ParserDescr.node `ModuleCat.«term↿_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1024))
Instances For
Build an isomorphism in the category Module R
from a LinearEquiv
between Module
s.
Equations
- e.toModuleIso = { hom := ModuleCat.ofHom ↑e, inv := ModuleCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Build an isomorphism in the category ModuleCat R
from a LinearEquiv
between Module
s.
Equations
- e.toModuleIso'Left = e.toModuleIso
Instances For
Build an isomorphism in the category ModuleCat R
from a LinearEquiv
between Module
s.
Equations
- e.toModuleIso'Right = e.toModuleIso
Instances For
Build a LinearEquiv
from an isomorphism in the category ModuleCat R
.
Equations
- i.toLinearEquiv = LinearEquiv.ofLinear i.hom.hom i.inv.hom ⋯ ⋯
Instances For
linear equivalences between Module
s are the same as (isomorphic to) isomorphisms
in ModuleCat
Equations
- linearEquivIsoModuleIso = { hom := fun (e : X ≃ₗ[R] Y) => e.toModuleIso, inv := fun (i : ModuleCat.of R X ≅ ModuleCat.of R Y) => i.toLinearEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Equations
- ModuleCat.instAddCommGroupHom = Function.Injective.addCommGroup ModuleCat.Hom.hom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ModuleCat.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
Equations
- ModuleCat.Hom.instModule = Function.Injective.module S { toFun := ModuleCat.Hom.hom, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
ModuleCat.Hom.hom
bundled as a linear equivalence.
Equations
- ModuleCat.homLinearEquiv = { toFun := ModuleCat.homAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := ModuleCat.homAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- ModuleCat.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }
ModuleCat.Hom.hom
as an isomorphism of monoids.
Equations
- M.endMulEquiv = { toFun := ModuleCat.Hom.hom, invFun := ModuleCat.ofHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
The scalar multiplication on an object of ModuleCat R
considered as
a morphism of rings from R
to the endomorphisms of the underlying abelian group.
Equations
Instances For
The scalar multiplication on ModuleCat R
considered as a morphism of rings
to the endomorphisms of the forgetful functor to AddCommGrp)
.
Equations
- ModuleCat.smulNatTrans R = { toFun := fun (r : R) => { app := fun (M : ModuleCat R) => M.smul r, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Given A : AddCommGrp
and a ring morphism R →+* End A
, this is a type synonym
for A
, on which we shall define a structure of R
-module.
Equations
- ModuleCat.mkOfSMul' x = A
Instances For
Equations
- ModuleCat.instAddCommGroupαMkOfSMul' φ = id inferInstance
Equations
- ModuleCat.instSMulαAddCommGroupMkOfSMul' φ = { smul := fun (r : R) (x : ↑A) => (let_fun this := φ r; this) x }
Equations
Given A : AddCommGrp
and a ring morphism R →+* End A
, this is an object in
ModuleCat R
, whose underlying abelian group is A
and whose scalar multiplication is
given by R
.
Equations
Instances For
Constructor for morphisms in ModuleCat R
which takes as inputs
a morphism between the underlying objects in AddCommGrp
and the compatibility
with the scalar multiplication.
Equations
- ModuleCat.homMk φ hφ = { hom := { toFun := ⇑φ, map_add' := ⋯, map_smul' := ⋯ } }
Instances For
Turn a bilinear map into a homomorphism.
Equations
- ModuleCat.ofHom₂ f = ModuleCat.ofHom (↑ModuleCat.homLinearEquiv.symm ∘ₗ f)
Instances For
Turn a homomorphism into a bilinear map.
Equations
- f.hom₂ = (⋯.mpr (CategoryTheory.CategoryStruct.comp f (ModuleCat.ofHom ↑ModuleCat.homLinearEquiv))).hom
Instances For
@[simp]
lemmas for LinearMap.comp
and categorical identities.