Theorems · Definition · category theory
CategoryTheory.Subfunctor.toFunctor
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{F : CategoryTheory.Functor C (Type w)} → CategoryTheory.Subfunctor F → CategoryTheory.Functor C (Type w)The subfunctor as a functor.
- Defined in
- Mathlib.CategoryTheory.Subfunctor.Basic
- Cited by
- 90 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapproof · cited by 8,698
- Set.Elemproof · cited by 7,166
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- TypeCat.ofHomproof · cited by 389
- CategoryTheory.Subfunctor.objproof · cited by 227
- CategoryTheory.Subfunctorstatement and proof · cited by 112
Cited by113
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.toSSetproof · cited by 315
- CategoryTheory.Subfunctor.ιstatement and proof · cited by 50
- CategoryTheory.Subfunctor.equalizerstatement and proof · cited by 17
- CategoryTheory.Subfunctor.homOfLestatement and proof · cited by 11
- CategoryTheory.Subfunctor.toRangestatement · cited by 10
- CategoryTheory.Sheaf.Ωproof · cited by 9
- CategoryTheory.Subfunctor.liftstatement · cited by 9
- CategoryTheory.Subfunctor.homOfLe_ιstatement and proof · cited by 8
- CategoryTheory.Subfunctor.equalizer.ιstatement and proof · cited by 7
- CategoryTheory.Sheaf.imageproof · cited by 6
- CategoryTheory.Subfunctor.range_ιstatement · cited by 6
- CategoryTheory.Subfunctor.equalizer.liftstatement and proof · cited by 5