Natural transformations out of modules are determined at the ring

Every R-module is the cokernel of a morphism between direct sums of copies of R. Hence a natural transformation α : F ⟶ G between colimit-preserving functors out of ModuleCat R is an isomorphism as soon as its component at R is: its components at direct sums of copies of R are then isomorphisms, and so are its components at their cokernels.

This is the standard way of checking that a comparison map between two right exact constructions on modules is invertible, for instance that the sheaf associated with a tensor product of modules is the tensor product of the associated sheaves.

Main declarations

• TauCeti.ModuleCat.isIso_of_isIso_app_self: a natural transformation between colimit-preserving functors out of ModuleCat R whose component at R is invertible is an isomorphism.

theorem TauCeti.ModuleCat.isIso_of_isIso_app_self {R : Type u} [Ring R] {D : Type v} [CategoryTheory.Category.{w, v} D] {F G : CategoryTheory.Functor (ModuleCat R) D} [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, w, u + 1, v} F] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, w, u + 1, v} G] (α : F ⟶ G) [CategoryTheory.IsIso (α.app ↧R)] : CategoryTheory.IsIso α

A natural transformation between colimit-preserving functors out of ModuleCat R is an isomorphism as soon as its component at R is.