Theorems · Definition · category theory

SheafOfModules.Hom.val

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → {X Y : SheafOfModules R} → X.Hom Y → (X.val ⟶ Y.val)

a morphism between the underlying presheaves of modules

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf

Cited by

39 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category