Theorems · Definition · category theory
ModuleCat.freeMk
{R : Type u} → [inst : Ring R] → {X : Type u} → X → ↑((ModuleCat.free R).obj X)Constructor for elements in the module (free R).obj X.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement · cited by 19,642
- Ringstatement and proof · cited by 7,463
- ModuleCatstatement · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- Finsupp.singleproof · cited by 943
- ModuleCat.freestatement · cited by 19
Cited by22
Results whose statement or proof uses this declaration.
- PresheafOfModules.freeObjproof · cited by 7
- PresheafOfModules.freeAdjunctionUnitproof · cited by 3
- ModuleCat.freeHomEquivproof · cited by 3
- PresheafOfModules.Elements.fromFreeYoneda_app_applystatement · cited by 1
- PresheafOfModules.freeYonedaCoproductMkproof · cited by 1
- PresheafOfModules.freeYonedaEquiv_symm_appstatement · cited by 1
- ModuleCat.free_hom_extstatement and proof · cited by 1
- ModuleCat.freeDesc_applystatement and proof · cited by 1
- ModuleCat.FreeMonoidal.εIso_inv_freeMkstatement · cited by 1
- ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMkstatement · cited by 1
- ModuleCat.FreeMonoidal.μIso_inv_freeMkstatement · cited by 1
- ModuleCat.free_ε_onestatement · cited by 0