Theorems · Theorem · category theory

PresheafOfModules.hom_ext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {f g : M₁ ⟶ M₂}, (∀ (X : Cᵒᵖ), f.app X = g.app X) → f = g

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category