Theorems · Theorem · category theory

ModuleCat.free_hom_ext

∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} {f g : (ModuleCat.free R).obj X ⟶ M},
  (∀ (x : X),
      (CategoryTheory.ConcreteCategory.hom f) (ModuleCat.freeMk x) =
        (CategoryTheory.ConcreteCategory.hom g) (ModuleCat.freeMk x)) →
    f = g

Defined in: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Cited by: 1 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
Ringstatement and proof · cited by 7,463
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
ModuleCatstatement and proof · cited by 1,429
ModuleCat.carrierstatement · cited by 997
LinearMap.ext_ringproof · cited by 152
ModuleCat.hom_extproof · cited by 84
Finsupp.lhom_ext'proof · cited by 59

Cited by1

Results whose statement or proof uses this declaration.

ModuleCat.free_hom_ext_iffproof · cited by 0