mathlib3 documentation

algebra.category.fgModule.basic

The category of finitely generated modules over a ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This introduces fgModule R, the category of finitely generated modules over a ring R. It is implemented as a full subcategory on a subtype of Module R.

When K is a field, fgModule K is the category of finite dimensional vector spaces over K.

We first create the instance as a preadditive category. When R is commutative we then give the structure as an R-linear monoidal category. When R is a field we give it the structure of a closed monoidal category and then as a right-rigid monoidal category.

Future work #

Show that fgModule R is abelian when R is (left)-noetherian.

@[protected, instance]

def fgModule.concrete_category (R : Type u) [ring R] :

category_theory.concrete_category (fgModule R)

def fgModule (R : Type u) [ring R] :

Type (u+1)

Define fgModule as the subtype of Module.{u} R of finitely generated modules.

Equations

fgModule R = category_theory.full_subcategory (λ (V : Module R), module.finite R ↥V)

Instances for fgModule

@[protected, instance]

def fgModule.preadditive (R : Type u) [ring R] :

category_theory.preadditive (fgModule R)

@[protected, instance]

def fgModule.large_category (R : Type u) [ring R] :

category_theory.large_category (fgModule R)

@[protected, instance]

def fgModule.finite (R : Type u) [ring R] (V : fgModule R) :

module.finite R ↥(V.obj)

@[protected, instance]

def fgModule.inhabited (R : Type u) [ring R] :

inhabited (fgModule R)

Equations

fgModule.inhabited R = {default := {obj := Module.of R R semiring.to_module, property := _}}

def fgModule.of (R : Type u) [ring R] (V : Type u) [add_comm_group V] [module R V] [module.finite R V] :

Lift an unbundled finitely generated module to fgModule R.

Equations

fgModule.of R V = {obj := Module.of R V _inst_3, property := _}

@[protected, instance]

def fgModule.obj.module.finite (R : Type u) [ring R] (V : fgModule R) :

module.finite R ↥(V.obj)

@[protected, instance]

def fgModule.Module.category_theory.has_forget₂ (R : Type u) [ring R] :

category_theory.has_forget₂ (fgModule R) (Module R)

Equations

fgModule.Module.category_theory.has_forget₂ R = id (category_theory.full_subcategory.has_forget₂ (λ (V : Module R), module.finite R ↥V))

@[protected, instance]

def fgModule.category_theory.forget₂.category_theory.full (R : Type u) [ring R] :

category_theory.full (category_theory.forget₂ (fgModule R) (Module R))

Equations

fgModule.category_theory.forget₂.category_theory.full R = {preimage := λ (X Y : fgModule R) (f : (category_theory.forget₂ (fgModule R) (Module R)).obj X ⟶ (category_theory.forget₂ (fgModule R) (Module R)).obj Y), f, witness' := _}

def fgModule.iso_to_linear_equiv {R : Type u} [ring R] {V W : fgModule R} (i : V ≅ W) :

↥(V.obj) ≃ₗ[R] ↥(W.obj)

Converts and isomorphism in the category fgModule R to a linear_equiv between the underlying modules.

Equations

fgModule.iso_to_linear_equiv i = ((category_theory.forget₂ (fgModule R) (Module R)).map_iso i).to_linear_equiv

def linear_equiv.to_fgModule_iso {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :

fgModule.of R V ≅ fgModule.of R W

Converts a linear_equiv to an isomorphism in the category fgModule R.

Equations

e.to_fgModule_iso = {hom := e.to_linear_map, inv := e.symm.to_linear_map, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem linear_equiv.to_fgModule_iso_inv {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :

e.to_fgModule_iso.inv = e.symm.to_linear_map

@[simp]

theorem linear_equiv.to_fgModule_iso_hom {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :

e.to_fgModule_iso.hom = e.to_linear_map

@[protected, instance]

def fgModule.category_theory.linear (R : Type u) [comm_ring R] :

category_theory.linear R (fgModule R)

Equations

fgModule.category_theory.linear R = category_theory.linear.full_subcategory (λ (V : Module R), module.finite R ↥V)

@[protected, instance]

def fgModule.monoidal_predicate_module_finite (R : Type u) [comm_ring R] :

category_theory.monoidal_category.monoidal_predicate (λ (V : Module R), module.finite R ↥V)

@[protected, instance]

def fgModule.category_theory.monoidal_category (R : Type u) [comm_ring R] :

category_theory.monoidal_category (fgModule R)

Equations

fgModule.category_theory.monoidal_category R = category_theory.monoidal_category.full_monoidal_subcategory (λ (V : Module R), module.finite R ↥V)

@[protected, instance]

def fgModule.category_theory.symmetric_category (R : Type u) [comm_ring R] :

category_theory.symmetric_category (fgModule R)

Equations

fgModule.category_theory.symmetric_category R = category_theory.monoidal_category.full_symmetric_subcategory (λ (V : Module R), module.finite R ↥V)

@[protected, instance]

def fgModule.category_theory.monoidal_preadditive (R : Type u) [comm_ring R] :

category_theory.monoidal_preadditive (fgModule R)

@[protected, instance]

def fgModule.category_theory.monoidal_linear (R : Type u) [comm_ring R] :

category_theory.monoidal_linear R (fgModule R)

def fgModule.forget₂_monoidal (R : Type u) [comm_ring R] :

category_theory.monoidal_functor (fgModule R) (Module R)

The forgetful functor fgModule R ⥤ Module R as a monoidal functor.

Equations

fgModule.forget₂_monoidal R = category_theory.monoidal_category.full_monoidal_subcategory_inclusion (λ (V : Module R), module.finite R ↥V)

@[protected, instance]

def fgModule.forget₂_monoidal_faithful (R : Type u) [comm_ring R] :

category_theory.faithful (fgModule.forget₂_monoidal R).to_lax_monoidal_functor.to_functor

@[protected, instance]

def fgModule.forget₂_monoidal_additive (R : Type u) [comm_ring R] :

(fgModule.forget₂_monoidal R).to_lax_monoidal_functor.to_functor.additive

@[protected, instance]

def fgModule.forget₂_monoidal_linear (R : Type u) [comm_ring R] :

category_theory.functor.linear R (fgModule.forget₂_monoidal R).to_lax_monoidal_functor.to_functor

theorem fgModule.iso.conj_eq_conj (R : Type u) [comm_ring R] {V W : fgModule R} (i : V ≅ W) (f : category_theory.End V) :

⇑(i.conj) f = ⇑((fgModule.iso_to_linear_equiv i).conj) f

@[protected, instance]

def fgModule.quiver.hom.module.finite (K : Type u) [field K] (V W : fgModule K) :

module.finite K (V ⟶ W)

@[protected, instance]

def fgModule.closed_predicate_module_finite (K : Type u) [field K] :

category_theory.monoidal_category.closed_predicate (λ (V : Module K), module.finite K ↥V)

@[protected, instance]

def fgModule.category_theory.monoidal_closed (K : Type u) [field K] :

category_theory.monoidal_closed (fgModule K)

Equations

fgModule.category_theory.monoidal_closed K = category_theory.monoidal_category.full_monoidal_closed_subcategory (λ (V : Module K), module.finite K ↥V)

@[simp]

theorem fgModule.ihom_obj (K : Type u) [field K] (V W : fgModule K) :

(category_theory.ihom V).obj W = fgModule.of K (↥(V.obj) →ₗ[K] ↥(W.obj))

def fgModule.fgModule_dual (K : Type u) [field K] (V : fgModule K) :

The dual module is the dual in the rigid monoidal category fgModule K.

Equations

fgModule.fgModule_dual K V = {obj := Module.of K (module.dual K ↥(V.obj)) linear_map.module, property := _}

Instances for fgModule.fgModule_dual

fgModule.exact_pairing

noncomputable def fgModule.fgModule_coevaluation (K : Type u) [field K] (V : fgModule K) :

𝟙_ (fgModule K) ⟶ V ⊗ fgModule.fgModule_dual K V

The coevaluation map is defined in linear_algebra.coevaluation.

Equations

fgModule.fgModule_coevaluation K V = coevaluation K ↥(V.obj)

theorem fgModule.fgModule_coevaluation_apply_one (K : Type u) [field K] (V : fgModule K) :

⇑(fgModule.fgModule_coevaluation K V) 1 = finset.univ.sum (λ (i : ↥(basis.of_vector_space_index K ↥(V.obj))), ⇑(basis.of_vector_space K ↥(V.obj)) i ⊗ₜ[K] (basis.of_vector_space K ↥(V.obj)).coord i)

def fgModule.fgModule_evaluation (K : Type u) [field K] (V : fgModule K) :

fgModule.fgModule_dual K V ⊗ V ⟶ 𝟙_ (fgModule K)

The evaluation morphism is given by the contraction map.

Equations

fgModule.fgModule_evaluation K V = contract_left K ↥(V.obj)

@[simp]

theorem fgModule.fgModule_evaluation_apply (K : Type u) [field K] (V : fgModule K) (f : ↥((fgModule.fgModule_dual K V).obj)) (x : ↥(V.obj)) :

⇑(fgModule.fgModule_evaluation K V) (f ⊗ₜ[K] x) = f.to_fun x

@[protected, instance]

noncomputable def fgModule.exact_pairing (K : Type u) [field K] (V : fgModule K) :

category_theory.exact_pairing V (fgModule.fgModule_dual K V)

Equations

fgModule.exact_pairing K V = {coevaluation := fgModule.fgModule_coevaluation K V, evaluation := fgModule.fgModule_evaluation K V, coevaluation_evaluation' := _, evaluation_coevaluation' := _}

@[protected, instance]

noncomputable def fgModule.right_dual (K : Type u) [field K] (V : fgModule K) :

category_theory.has_right_dual V

Equations

fgModule.right_dual K V = category_theory.has_right_dual.mk (fgModule.fgModule_dual K V)

@[protected, instance]

noncomputable def fgModule.right_rigid_category (K : Type u) [field K] :

category_theory.right_rigid_category (fgModule K)

Equations

fgModule.right_rigid_category K = category_theory.right_rigid_category.mk