Theorems · Definition · commutative algebra
RingCat.Hom.hom
{R S : RingCat} → R.Hom S → ↑R →+* ↑STurn a morphism in RingCat back into a RingHom.
- Defined in
- Mathlib.Algebra.Category.Ring.Basic
- Cited by
- 85 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHomstatement · cited by 10,189
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- RingCatstatement and proof · cited by 473
- RingCat.carrierstatement · cited by 279
- RingCat.Homstatement and proof · cited by 8
Cited by128
Results whose statement or proof uses this declaration.
- PresheafOfModules.mapstatement · cited by 55
- PresheafOfModules.restrictScalarsproof · cited by 14
- SheafOfModules.pushforwardNatTransproof · cited by 8
- PresheafOfModules.Submodule.toPresheafOfModulesproof · cited by 7
- PresheafOfModules.constFunctorproof · cited by 7
- PresheafOfModules.restrictₛₗstatement · cited by 6
- PresheafOfModules.ModuleColimit.ιRproof · cited by 6
- AlgCat.intEquivalenceproof · cited by 5
- PresheafOfModules.map_smulstatement and proof · cited by 5
- PresheafOfModules.colimitPresheafOfModulesstatement and proof · cited by 4
- PresheafOfModules.forgetToPresheafModuleCatObjObjproof · cited by 4
- RingCat.comp_applyproof · cited by 4