Theorems · Definition · category theory
CategoryTheory.Functor.diag
(C : Type u₃) → [inst : CategoryTheory.Category.{v₃, u₃} C] → CategoryTheory.Functor C (C × C)The diagonal functor.
- Defined in
- Mathlib.CategoryTheory.Products.Basic
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Functor.idproof · cited by 3,333
- CategoryTheory.Functor.prod'proof · cited by 31
Cited by49
Results whose statement or proof uses this declaration.
- CategoryTheory.StructuredArrow.ofDiagEquivalence.functorstatement and proof · cited by 6
- CategoryTheory.Limits.IsColimit.tensorproof · cited by 6
- CategoryTheory.CostructuredArrow.ofDiagEquivalence.functorstatement and proof · cited by 6
- CategoryTheory.IsSiftedOrEmptyproof · cited by 4
- CategoryTheory.StructuredArrow.ofDiagEquivalence.inversestatement and proof · cited by 4
- CategoryTheory.CostructuredArrow.ofDiagEquivalence.inversestatement and proof · cited by 4
- CategoryTheory.MonoidalCategory.externalProductCompDiagIsostatement and proof · cited by 3
- CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProductsproof · cited by 1
- CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_right_asstatement · cited by 0
- CategoryTheory.IsSifted.casesOnstatement and proof · cited by 0
- CategoryTheory.IsSifted.factorization_prodComparison_colimstatement and proof · cited by 0
- CategoryTheory.IsSifted.recOnstatement and proof · cited by 0