RepresentedBy

📁 Source: Mathlib/CategoryTheory/RepresentedBy.lean

Statistics

Metric	Count
Definitions IsRepresentedBy, representableBy, uliftYonedaIso	3
Theorems iff_exists_isRepresentedBy, iff_exists_representableBy, iff_isIso_uliftYonedaEquiv, iff_natIso, iff_of_isoObj, map_bijective, of_isRepresentable, of_isoObj, of_natIso, representableBy_homEquiv_apply, uliftYonedaIso_hom, isRepresentedBy, isRepresentedBy_iff	13
Total	16

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsRepresentedBy 📖	CompData	8 math math: IsRepresentedBy.of_isRepresentable, isRepresentedBy_iff, IsRepresentable.iff_exists_isRepresentedBy, RepresentableBy.isRepresentedBy, IsRepresentedBy.iff_isIso_uliftYonedaEquiv, IsRepresentedBy.iff_of_isoObj, IsRepresentedBy.iff_natIso, IsRepresentedBy.iff_exists_representableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRepresentedBy_iff 📖	mathematical	—	IsRepresentedBy Function.Bijective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op map Quiver.Hom.op	—	—

CategoryTheory.Functor.IsRepresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_isRepresentedBy 📖	mathematical	—	CategoryTheory.Functor.IsRepresentable CategoryTheory.Functor.IsRepresentedBy	—	CategoryTheory.Functor.IsRepresentedBy.of_isRepresentable CategoryTheory.Functor.RepresentableBy.isRepresentable

CategoryTheory.Functor.IsRepresentedBy

Definitions

Name	Category	Theorems
representableBy 📖	CompOp	1 math math: representableBy_homEquiv_apply
uliftYonedaIso 📖	CompOp	1 math math: uliftYonedaIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_representableBy 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.RepresentableBy.homEquiv CategoryTheory.CategoryStruct.id	—	CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.Functor.RepresentableBy.isRepresentedBy
iff_isIso_uliftYonedaEquiv 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy CategoryTheory.IsIso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.uliftFunctor DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Functor.isRepresentedBy_iff CategoryTheory.NatTrans.isIso_iff_isIso_app Function.Surjective.forall Opposite.op_surjective CategoryTheory.isIso_iff_bijective Function.Bijective.of_comp_iff Equiv.bijective Function.Bijective.of_comp_iff'
iff_natIso 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op	—	CategoryTheory.FunctorToTypes.hom_inv_id_app_apply of_natIso
iff_of_isoObj 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.Iso.inv_hom_id CategoryTheory.FunctorToTypes.map_id_apply of_isoObj
map_bijective 📖	mathematical	CategoryTheory.Functor.IsRepresentedBy	Function.Bijective Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Functor.map Quiver.Hom.op	—	—
of_isRepresentable 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy CategoryTheory.Functor.reprX CategoryTheory.Functor.reprx	—	CategoryTheory.Functor.RepresentableBy.isRepresentedBy
of_isoObj 📖	mathematical	CategoryTheory.Functor.IsRepresentedBy	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	iff_exists_representableBy CategoryTheory.Category.id_comp
of_natIso 📖	mathematical	CategoryTheory.Functor.IsRepresentedBy	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op	—	iff_exists_representableBy CategoryTheory.FunctorToTypes.map_id_apply
representableBy_homEquiv_apply 📖	mathematical	CategoryTheory.Functor.IsRepresentedBy	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.RepresentableBy.homEquiv representableBy CategoryTheory.Functor.map Quiver.Hom.op	—	—
uliftYonedaIso_hom 📖	mathematical	CategoryTheory.Functor.IsRepresentedBy	CategoryTheory.Iso.hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.uliftFunctor uliftYonedaIso DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	—

CategoryTheory.Functor.RepresentableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRepresentedBy 📖	mathematical	—	CategoryTheory.Functor.IsRepresentedBy DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.Iso.isIso_hom

---

← Back to Index