Theorems · Inductive type · category theory

PresheafOfModules

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor Cᵒᵖ RingCat → Type (max (max (max u u₁) (v + 1)) v₁)

A presheaf of modules over R : Cᵒᵖ ⥤ RingCat consists of family of objects obj X : ModuleCat (R.obj X) for all X : Cᵒᵖ together with functorial maps obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (obj Y) for all f : X ⟶ Y in Cᵒᵖ.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

247 results in Mathlib

Foundations

Depth 21 from the axioms, rests on 190 definitions · uses propext, Quot.sound

Assumes

CategoryTheory.Category