Theorems · Theorem · category theory
CategoryTheory.Functor.map_preimage
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D) [inst_2 : F.Full] {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (F.preimage f) = f- Cited by
- 64 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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.Functor.objstatement and proof · 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.preimagestatement · cited by 55
- CategoryTheory.Functor.map_surjectiveproof · cited by 29
Cited by64
Results whose statement or proof uses this declaration.
- CategoryTheory.Localization.liftNatTrans_appproof · cited by 20
- AlgebraicGeometry.Spec.map_preimageproof · cited by 11
- CategoryTheory.isIso_of_fully_faithfulproof · cited by 7
- CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιKproof · cited by 5
- CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQproof · cited by 4
- CategoryTheory.Functor.relativelyRepresentable.lift'_fstproof · cited by 4
- CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithfulproof · cited by 3
- CategoryTheory.Functor.relativelyRepresentable.hom_ext'proof · cited by 3
- CategoryTheory.Functor.reflects_precoherentproof · cited by 3
- CategoryTheory.Functor.reflects_preregularproof · cited by 3
- CategoryTheory.Functor.relativelyRepresentable.lift_fstproof · cited by 3
- CategoryTheory.Functor.relativelyRepresentable.lift_sndproof · cited by 3