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.

Equations

• x.repr = ((Fin x.n → R) ⧸ x.S)

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

Equations

• FGModuleRepr.instCoeSortType R = { coe := FGModuleRepr.repr }

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

Equations

• FGModuleRepr.instAddCommGroupRepr R x = id inferInstance

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

Equations

• FGModuleRepr.instModuleRepr R x = id inferInstance

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$$).

Equations

• FGModuleRepr.ofFinite R M = { n := ⋯.choose, S := ⋯.choose }

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.

Equations

• FGModuleRepr.ofFiniteEquiv R M = Classical.choice ⋯

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

Equations

• FGModuleRepr.instCategory R = CategoryTheory.InducedCategory.category fun (x : FGModuleRepr R) => FGModuleCat.of R x.repr

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

Equations

• FGModuleRepr.instSmallCategory R = { toCategoryStruct := (FGModuleRepr.instCategory R).toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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.

Equations

• FGModuleRepr.embed R = (CategoryTheory.inducedFunctor fun (x : FGModuleRepr R) => FGModuleCat.of R x.repr).comp (FGModuleCat.ulift 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