Theorems · Inductive type · category theory

PresheafOfModules.Submodule

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

A family of submodules N X of M.obj X, for a presheaf of modules M, stable under the restriction maps of M. This defines a subobject of M in PresheafOfModules R.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Cited by

21 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category