Theorems · Definition · category theory
ModuleCat.Hom.hom
{R : Type u} → [inst : Ring R] → {A B : ModuleCat R} → A.Hom B → ↑A →ₗ[R] ↑BTurn a morphism in ModuleCat back into a LinearMap.
- Defined in
- Mathlib.Algebra.Category.ModuleCat.Basic
- Cited by
- 341 results in Mathlib
- Foundations
- Depth 28 from the axioms, rests on 244 definitions · uses propext, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- ModuleCat.Homstatement and proof · cited by 7
Cited by420
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.moduleCatLeftHomologyDataproof · cited by 106
- ModuleCat.hom_extstatement and proof · cited by 84
- groupCohomology.cocycles₁proof · cited by 57
- groupHomology.cycles₁proof · cited by 56
- groupCohomology.cocycles₂proof · cited by 45
- groupHomology.cycles₂proof · cited by 43
- CategoryTheory.ShortComplex.moduleCatToCyclesstatement and proof · cited by 20
- groupCohomology.coboundaries₁proof · cited by 13
- AlgebraicGeometry.tilde.mapproof · cited by 11
- groupCohomology.coboundaries₂proof · cited by 11
- groupHomology.boundaries₁proof · cited by 11
- groupHomology.boundaries₂proof · cited by 11
Showing the 200 most cited of 420.