Theorems · Theorem · category theory
SemimoduleCat.hom_ext
∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {f g : M ⟶ N},
SemimoduleCat.Hom.hom f = SemimoduleCat.Hom.hom g → f = g- Defined in
- Mathlib.Algebra.Category.ModuleCat.Semi
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement · cited by 10,215
- SemimoduleCatstatement and proof · cited by 108
- SemimoduleCat.carrierstatement · cited by 87
- SemimoduleCat.Hom.homstatement and proof · cited by 45
- SemimoduleCat.Hom.extproof · cited by 2
Cited by15
Results whose statement or proof uses this declaration.
- SemimoduleCat.MonoidalCategory.braiding_naturalityproof · cited by 2
- SemimoduleCat.isZero_of_subsingletonproof · cited by 1
- SemimoduleCat.MonoidalCategory.tensor_ext₃'proof · cited by 1
- SemimoduleCat.hom_ext_iffproof · cited by 0
- SemimoduleCat.MonoidalCategory.leftUnitor_naturalityproof · cited by 0
- SemimoduleCat.MonoidalCategory.pentagonproof · cited by 0
- SemimoduleCat.MonoidalCategory.triangleproof · cited by 0
- SemimoduleCat.MonoidalCategory.rightUnitor_naturalityproof · cited by 0
- SemimoduleCat.MonoidalCategory.tensorHom_comp_tensorHomproof · cited by 0
- SemimoduleCat.MonoidalCategory.tensor_extproof · cited by 0
- SemimoduleCat.MonoidalCategory.associator_naturalityproof · cited by 0
- SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorCommproof · cited by 0