Theorems · Definition · category theory
ModuleCat.smul
{R : Type u} →
[inst : Ring R] →
(M : ModuleCat R) → R →+* CategoryTheory.End ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M)The scalar multiplication on an object of ModuleCat R considered as
a morphism of rings from R to the endomorphisms of the underlying abelian group.
- Defined in
- Mathlib.Algebra.Category.ModuleCat.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 34 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.
Cites13
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
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- RingHomstatement · cited by 10,189
- Ringstatement and proof · cited by 7,463
- AddMonoidHomstatement · cited by 3,230
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.carrierstatement and proof · cited by 997
- AddCommGrpCatstatement · cited by 462
- AddCommGrpCat.carrierstatement · cited by 407
- CategoryTheory.forget₂statement · cited by 260
- CategoryTheory.Endstatement · cited by 169
Cited by18
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Modules.smulproof · cited by 9
- ModuleCat.homMkstatement and proof · cited by 6
- ModuleCat.isoMkstatement and proof · cited by 3
- ModuleCat.HasColimit.coconePointSMulproof · cited by 3
- ModuleCat.smul_naturalitystatement · cited by 2
- ModuleCat.smulNatTransproof · cited by 1
- PresheafOfModules.smul_mapstatement · cited by 1
- ModuleCat.homMk.congr_simpstatement and proof · cited by 0
- ModuleCat.mkOfSMul_smulstatement · cited by 0
- ModuleCat.smul_restrictScalarsstatement · cited by 0
- ModuleCat.smulNatTrans_apply_appstatement · cited by 0
- ModuleCat.isoMk_homstatement and proof · cited by 0