The category of finitely generated modules over a ring is essentially small

This file proves that FGModuleCat R, the category of finitely generated modules over a ring R, is essentially small, by providing an explicit small model. However, for applications, it is recommended to use the standard CategoryTheory.SmallModel (FGModuleCat R) instead.

structure FGModuleRepr (R : Type u) [CommRing R] : Type u

A (category-theoretically) small version of FGModuleCat R. This is used to prove that FGModuleCat R is essentially small. For actual use, it might be recommended to use the canonical CategoryTheory.SmallModel instead of this construction.

• n : ℕ

  The natural number n that defines the module as a quotient of Fin n → R (i.e. R^n).

• S : Submodule R (Fin self.n → R)

  The kernel of the surjective map from Fin n → R (i.e. R^n) to the module represented.

def FGModuleRepr.repr {R : Type u} [CommRing R] (x : FGModuleRepr R) : Type u

The finite module represented by an object of the type FGModuleRepr R, which is the quotient of Fin n → R (i.e. $$R^n$$) by the submodule S provided.

instance FGModuleRepr.instCoeSortType (R : Type u) [CommRing R] : CoeSort (FGModuleRepr R) (Type u)

instance FGModuleRepr.instAddCommGroupRepr (R : Type u) [CommRing R] (x : FGModuleRepr R) : AddCommGroup x.repr

instance FGModuleRepr.instModuleRepr (R : Type u) [CommRing R] (x : FGModuleRepr R) : Module R x.repr

instance FGModuleRepr.instFiniteRepr (R : Type u) [CommRing R] (x : FGModuleRepr R) : Module.Finite R x.repr

noncomputable def FGModuleRepr.ofFinite (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : FGModuleRepr R

A non-canonical representation of a finite module (as a quotient of $$R^n$$).

noncomputable def FGModuleRepr.ofFiniteEquiv (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : (ofFinite R M).repr ≃ₗ[R] M

The non-canonical representation ofFinite of a finite module is actually isomorphic to the given module.

instance FGModuleRepr.instCategory (R : Type u) [CommRing R] : CategoryTheory.Category.{u, u} (FGModuleRepr R)

instance FGModuleRepr.instSmallCategory (R : Type u) [CommRing R] : CategoryTheory.SmallCategory (FGModuleRepr R)

def FGModuleRepr.embed (R : Type u) [CommRing R] : CategoryTheory.Functor (FGModuleRepr R) (FGModuleCat R)

The canonical embedding of this small category to the canonical (large) category FGModuleCat R.

instance FGModuleRepr.instIsEquivalenceFGModuleCatEmbed (R : Type u) [CommRing R] : (embed R).IsEquivalence

instance instEssentiallySmallFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.EssentiallySmall.{u, v, max (v + 1) u} (FGModuleCat R)

instance instIsEquivalenceFGModuleCatUlift (R : Type u) [CommRing R] : (FGModuleCat.ulift R).IsEquivalence