Theorems · Definition · category theory
CategoryTheory.InducedCategory
{C : Type u₁} → (D : Type u₂) → (C → D) → Type u₁InducedCategory D F, where F : C → D, is a typeclass synonym for C,
which provides a category structure so that the morphisms X ⟶ Y are the morphisms
in D from F X to F Y.
- Defined in
- Mathlib.CategoryTheory.InducedCategory
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by93
Results whose statement or proof uses this declaration.
- CategoryTheory.InducedCategory.Hom.homstatement and proof · cited by 850
- CategoryTheory.Skeletonproof · cited by 35
- CategoryTheory.InducedCategory.homMkstatement and proof · cited by 33
- CategoryTheory.InducedCategory.hom_extstatement and proof · cited by 16
- CategoryTheory.inducedFunctorstatement and proof · cited by 14
- CategoryTheory.InducedCategory.Homstatement · cited by 12
- CategoryTheory.FinCategory.ObjAsTypeproof · cited by 6
- CategoryTheory.Equivalence.inducedstatement and proof · cited by 5
- CategoryTheory.InducedCategory.endEquivstatement and proof · cited by 5
- TopCat.Sheaf.restrictHomEquivHomstatement · cited by 4
- CategoryTheory.InducedCategory.isoMkstatement and proof · cited by 3
- CategoryTheory.InducedCategory.homMk_homstatement and proof · cited by 3