Theorems · Theorem · category theory
CategoryTheory.Functor.map_injective
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
{X Y : C} (F : CategoryTheory.Functor C D) [F.Faithful], Function.Injective F.map- Cited by
- 91 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapstatement · cited by 8,698
- CategoryTheory.Functor.Faithfulstatement and proof · cited by 313
- CategoryTheory.Functor.Faithful.map_injectiveproof · cited by 3
Cited by93
Results whose statement or proof uses this declaration.
- CategoryTheory.isIso_of_fully_faithfulproof · cited by 7
- CategoryTheory.Triangulated.TStructure.zeroproof · cited by 7
- CategoryTheory.Functor.final_iff_of_isFilteredproof · cited by 6
- CategoryTheory.Functor.Faithful.of_compproof · cited by 6
- CategoryTheory.locallySmall_of_faithfulproof · cited by 5
- CategoryTheory.ChosenPullbacksAlong.hom_extproof · cited by 5
- CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_posproof · cited by 4
- ModuleCat.ExtendScalars.hom_extproof · cited by 4
- CategoryTheory.Functor.relativelyRepresentable.lift'_fstproof · cited by 4
- AlgebraicGeometry.Spec.map_injproof · cited by 3
- CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQproof · cited by 3
- CategoryTheory.ShortComplex.exact_map_iff_of_faithfulproof · cited by 3