mathlib3 documentation

algebra.category.fgModule.limits

forget₂ (fgModule K) (Module K) creates all finite limits. #

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

And hence fgModule K has all finite limits.

Future work #

After generalising fgModule to allow the ring and the module to live in different universes, generalize this construction so we can take limits over smaller diagrams, as is done for the other algebraic categories.

Analogous constructions for Noetherian modules.

@[protected, instance]
def fgModule.category_theory.limits.pi_obj.finite_dimensional {k : Type v} [field k] {J : Type} [fintype J] (Z : J Module k) [ (j : J), finite_dimensional k (Z j)] :
finite_dimensional k ( λ (j : J), Z j)
@[protected, instance]

Finite limits of finite dimensional vectors spaces are finite dimensional, because we can realise them as subobjects of a finite product.