Theorems · Theorem · category theory

CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I Z : C}
  (p : I ⟶ Z),
  CategoryTheory.Limits.IsZero Z →
    (CategoryTheory.Injective I ↔ (CategoryTheory.MorphismProperty.monomorphisms C).rlp p)

Defined in: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Cited by: 1 results in Mathlib
Foundations: Depth 12 from the axioms · uses propext, Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.Monoproof · cited by 893
CategoryTheory.Limits.comp_zeroproof · cited by 365
CategoryTheory.Limits.IsZerostatement and proof · cited by 306
CategoryTheory.CommSqproof · cited by 158
CategoryTheory.Injectivestatement and proof · cited by 70
CategoryTheory.MorphismProperty.rlpstatement and proof · cited by 53
CategoryTheory.HasLiftingPropertyproof · cited by 50
CategoryTheory.Limits.IsZero.eq_of_tgtproof · cited by 46
CategoryTheory.MorphismProperty.monomorphismsstatement and proof · cited by 39

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.injective_iff_rlp_monomorphisms_zeroproof · cited by 0