Theorems · Definition · category theory
CategoryTheory.isInjective
(C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty CThe ObjectProperty C corresponding to the notion of injective objects in C.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- CategoryTheory.ObjectPropertystatement · cited by 798
- CategoryTheory.Injectiveproof · cited by 70
Cited by12
Results whose statement or proof uses this declaration.
- CategoryTheory.InjectiveObjectproof · cited by 6
- CategoryTheory.InjectiveObject.ιstatement and proof · cited by 5
- CochainComplex.Plus.localizerMorphismstatement · cited by 1
- CochainComplex.Plus.exists_quasiIso_injectivestatement and proof · cited by 1
- HomotopyCategory.Plus.localizerMorphismstatement · cited by 1
- HomotopyCategory.Plus.localizerMorphism_derivesstatement · cited by 0
- CochainComplex.Plus.localizerMorphism_functorstatement · cited by 0
- DerivedCategory.Plus.exists_injective_nonempty_isostatement · cited by 0
- CochainComplex.Plus.fibrantObjectEquivalencestatement and proof · cited by 0
- CochainComplex.Plus.fibrantObjectLocalizerMorphismstatement · cited by 0
- HomotopyCategory.Plus.inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectιstatement · cited by 0
- HomotopyCategory.Plus.isIso_quotient_map_iffstatement · cited by 0