Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Functor.preimage

{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] → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)

The choice of a preimage of a morphism under a full functor.

Defined in
Mathlib.CategoryTheory.Functor.FullyFaithful
Cited by
55 results in Mathlib
Foundations
Depth 9 from the axioms · uses Classical.choice
Assumes
CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.Full
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Functor.map_preimage · cited by 64Functor.map_preimageCategoryTheory.Functor.relativelyRepresentable.fst' · cited by 43relativelyRepresentable.f…CategoryTheory.Functor.inv · cited by 27Functor.invCategoryTheory.Functor.FullyFaithful.ofFullyFaithful · cited by 21FullyFaithful.ofFullyFait…AlgebraicGeometry.Spec.preimage · cited by 14Spec.preimageCategoryTheory.Functor.preimageIso · cited by 14Functor.preimageIsoCategoryTheory.Abelian.LeftResolution.chainComplex · cited by 11LeftResolution.chainCompl…CategoryTheory.Localization.liftNatTrans · cited by 11Localization.liftNatTransCategoryTheory.Triangulated.AbelianSubcategory.ιK · cited by 9AbelianSubcategory.ιKCategoryTheory.Triangulated.AbelianSubcategory.πQ · cited by 9AbelianSubcategory.πQCategoryTheory.isIso_of_fully_faithful · cited by 7CategoryTheory.isIso_of_f…CategoryTheory.Functor.relativelyRepresentable.lift · cited by 7relativelyRepresentable.l…CategoryTheory.Abelian.LeftResolution.chainComplexXIso · cited by 6LeftResolution.chainCompl…AlgebraicTopology.DoldKan.Γ₂N₂.natTrans · cited by 6Γ₂N₂.natTransCategoryTheory.Functor.IsCoverDense.sheafHom · cited by 5IsCoverDense.sheafHomCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorCategoryTheory.Functor.Full · cited by 341Functor.FullCategoryTheory.Functor.map_surjective · cited by 29Functor.map_surjectiveFunctor.preimageCITED BYCITES

Cites6

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

Cited by86

Results whose statement or proof uses this declaration.