mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules

Open joelriou opened this issue 1 year ago • 2 comments
trafficstars

In this PR, we construct the pseudofunctor ModuleCat.restrictScalarsPseudofunctor : Pseudofunctor (LocallyDiscrete RingCatᵒᵖ) Cat which sends a ring R to its category of modules: the contravariant functoriality is given by the restriction of scalars functors. We also define ModuleCat.extendScalarsPseudofunctor : Pseudofunctor (LocallyDiscrete CommRingCat) Cat: the covariant functoriality is given by the extension of scalars functors.

  • [x] depends on: #18201

Open in Gitpod

joelriou avatar Oct 24 '24 18:10 joelriou