Theorems · Inductive type · category theory

SheafOfModules

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      CategoryTheory.Sheaf J RingCat → Type (max (max (max u u₁) (v + 1)) v₁)

A sheaf of modules is a presheaf of modules such that the underlying presheaf of abelian groups is a sheaf.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf

Cited by

188 results in Mathlib

Foundations

Depth 35 from the axioms, rests on 440 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category