Theorems · Theorem · category theory
ModuleCat.mono_iff_injective
∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y),
CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)- Cited by
- 21 results in Mathlib
- Foundations
- Depth 70 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.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- CategoryTheory.Monostatement · cited by 893
- LinearMap.ker_eq_botproof · cited by 92
- ModuleCat.mono_iff_ker_eq_botproof · cited by 1
Cited by21
Results whose statement or proof uses this declaration.
- Rep.mono_iff_injectiveproof · cited by 6
- groupHomology.H1π_eq_zero_iffproof · cited by 4
- CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iffproof · cited by 3
- Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iffproof · cited by 2
- groupHomology.cyclesMk₁_eqproof · cited by 2
- CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_dproof · cited by 2
- groupCohomology.H1π_eq_zero_iffproof · cited by 2
- Module.injective_module_of_injective_objectproof · cited by 2
- ModuleCat.linearIndependent_leftExactproof · cited by 2
- groupHomology.cyclesMk₀_eqproof · cited by 1
- groupHomology.cyclesMk₂_eqproof · cited by 1
- Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iffproof · cited by 1