Theorems · Theorem · category theory

ModuleCat.freeDesc_apply

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

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.

Cites17

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 · 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
one_smulproof · cited by 1,374
TypeCat.Funstatement · cited by 1,307
ModuleCat.carrierstatement and proof · cited by 997
zero_smulproof · cited by 716

Cited by1

Results whose statement or proof uses this declaration.

PresheafOfModules.freeYonedaEquiv_symm_appproof · cited by 1