Theorems · Definition · category theory
CategoryTheory.Functor.corepresentableBy
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
(F : CategoryTheory.Functor C (Type v)) → [hF : F.IsCorepresentable] → F.CorepresentableBy F.coreprXA chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.
- Defined in
- Mathlib.CategoryTheory.Yoneda
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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 and proof · cited by 16,252
- Nonempty.someproof · cited by 340
- CategoryTheory.Functor.CorepresentableBystatement · cited by 27
- CategoryTheory.Functor.IsCorepresentablestatement and proof · cited by 12
- CategoryTheory.Functor.coreprXstatement · cited by 3
Cited by11
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.partialLeftAdjointHomEquivproof · cited by 7
- CategoryTheory.Functor.partialLeftAdjointHomEquiv_compproof · cited by 2
- CategoryTheory.Functor.coreprxproof · cited by 2
- CategoryTheory.Functor.uliftCoyonedaCoreprXIsoproof · cited by 1
- CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_topproof · cited by 1
- CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_compproof · cited by 1
- CategoryTheory.Functor.coreprWproof · cited by 1
- CategoryTheory.Functor.uliftCoyonedaCoreprXIso_hom_appproof · cited by 0
- CategoryTheory.Functor.CorepresentableBy.isoCoreprXproof · cited by 0
- CategoryTheory.Functor.coreprW_hom_appproof · cited by 0
- CategoryTheory.corepresentable_of_natIsoproof · cited by 0