Theorems · Theorem · category theory

SheafOfModules.sectionsFunctor_map

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y : SheafOfModules R} (f : X ⟶ Y),
  (SheafOfModules.sectionsFunctor R).map f = TypeCat.ofHom (SheafOfModules.sectionsMap f)

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category