Theorems · Theorem · category theory
CategoryTheory.Functor.map_surjective
∀ {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.Full], Function.Surjective F.map- Cited by
- 29 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.Fullstatement and proof · cited by 341
- CategoryTheory.Functor.Full.map_surjectiveproof · cited by 3
Cited by30
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.map_preimageproof · cited by 64
- CategoryTheory.Functor.preimageproof · cited by 55
- CategoryTheory.Localization.exists_leftFractionproof · cited by 14
- HomotopyCategory.inverseImage_quotient_isomorphismsproof · cited by 2
- CochainComplex.HomComplex.CohomologyClass.toHom_bijectiveproof · cited by 2
- DerivedCategory.right_facproof · cited by 1
- CochainComplex.isKProjective_iff_leftOrthogonalproof · cited by 1
- CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eqproof · cited by 1
- CategoryTheory.Functor.relativelyRepresentable.mapproof · cited by 1
- CategoryTheory.Cat.FreeRefl.hom_inductionproof · cited by 1
- CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopyproof · cited by 1
- HomologicalComplex.isIso_quotient_map_iff_homotopyEquivalencesproof · cited by 1