Structures · Category theory
CategoryTheory.Functor.IsRepresentable
A functor F : Cᵒᵖ ⥤ Type v is representable if there is an object Y with a structure
F.RepresentableBy Y, i.e. there is a natural bijection (X ⟶ Y) ≃ F.obj (op X),
which may also be rephrased as a natural isomorphism yoneda.obj X ≅ F when Category.{v} C.
- Defined in
- Mathlib.CategoryTheory.Yoneda
- Shape
- One type argument · adds has_representation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- CategoryTheory.Functor.representableBy
- CategoryTheory.Functor.reprX
- CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
- CategoryTheory.Functor.reprx
- CategoryTheory.Functor.uliftYonedaReprXIso
- CategoryTheory.Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable
- CategoryTheory.Sheaf.isSheaf_of_isRepresentable
- CategoryTheory.Functor.IsRepresentedBy.of_isRepresentable
- CategoryTheory.Functor.reprW
- CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi
- CategoryTheory.CategoryOfElements.instHasInitialElementsOppositeOfIsRepresentable
- CategoryTheory.Functor.reprW_hom_app
- CategoryTheory.Functor.uliftYonedaReprXIso_hom_app
- CategoryTheory.Functor.IsRepresentable.has_representation
- CategoryTheory.Functor.RepresentableBy.isoReprX
- CategoryTheory.Functor.instPreservesLimitsOfSizeOpposite
- CategoryTheory.isRepresentable_of_natIso
- CategoryTheory.Functor.instIsRepresentableCompOppositeUliftFunctor
Ancestors0
No ancestors.