Theorems · Theorem · category theory

SheafOfModules.Hom.ext

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {x y : X.Hom Y}, x.val = y.val → x = y

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf

Cited by

2 results in Mathlib

Foundations

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