Yoneda

📁 Source: Mathlib/CategoryTheory/Yoneda.lean

Statistics

Metric	Count
Definitions fullyFaithful, ext, fullyFaithful, objOpOp, opIso, preimage, punitIso, CorepresentableBy, coyoneda, equivOfIsoObj, equivUliftCoyonedaIso, homEquiv, isoCoreprX, ofIso, ofIsoObj, toIso, uniqueUpToIso, compUliftCoyonedaCompWhiskeringLeft, compUliftYonedaCompWhiskeringLeft, compYonedaCompWhiskeringLeft, compYonedaCompWhiskeringLeftMaxRight, homNatIso, homNatIso', homNatIsoMaxRight, IsCorepresentable, IsRepresentable, RepresentableBy, equivOfIsoObj, equivUliftYonedaIso, homEquiv, isoReprX, ofIso, ofIsoObj, toIso, uniqueUpToIso, yoneda, coreprW, coreprX, corepresentableBy, corepresentableByEquiv, corepresentableByUliftFunctorEquiv, coreprx, reprW, reprX, representableBy, representableByEquiv, representableByUliftFunctorEquiv, reprx, sectionsEquivHom, uliftCoyonedaCoreprXIso, uliftYonedaReprXIso, fullyFaithful, ext, fullyFaithful, coyoneda, coyonedaCompYonedaObj, coyonedaEquiv, coyonedaEvaluation, coyonedaLemma, coyonedaPairing, curriedCoyonedaLemma, curriedCoyonedaLemma', curriedYonedaLemma, curriedYonedaLemma', largeCurriedCoyonedaLemma, largeCurriedYonedaLemma, prodCategoryInstance1, prodCategoryInstance2, sectionsFunctorNatIsoCoyoneda, uliftCoyoneda, uliftCoyonedaEquiv, uliftCoyonedaIsoCoyoneda, uliftCoyonedaRightOpCompCoyoneda, uliftYoneda, uliftYonedaEquiv, uliftYonedaIsoYoneda, uliftYonedaMap, uliftYonedaOpCompCoyoneda, yoneda, yonedaEquiv, yonedaEvaluation, yonedaLemma, yonedaMap, yonedaOpCompYonedaObj, yonedaPairing	85
Theorems instFaithfulOppositeFunctorTypeUliftCoyoneda, instFullOppositeFunctorTypeUliftCoyoneda, coyoneda_faithful, coyoneda_full, fullyFaithful_preimage, isIso, naturality, objOpOp_hom_app, objOpOp_inv_app, coyoneda_homEquiv, equivOfIsoObj_apply, equivOfIsoObj_symm_apply, equivUliftCoyonedaIso_apply, equivUliftCoyonedaIso_symm_apply_homEquiv, ext, ext_iff, homEquiv_comp, homEquiv_eq, homEquiv_symm_comp, isCorepresentable, ofIsoObj_homEquiv, uniqueUpToIso_hom, uniqueUpToIso_inv, compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down, compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down, compUliftYonedaCompWhiskeringLeft_hom_app_app_down, compUliftYonedaCompWhiskeringLeft_inv_app_app_down, compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down, compYonedaCompWhiskeringLeftMaxRight_inv_app_app, homNatIso'_hom_app_down, homNatIso'_inv_app_down, homNatIsoMaxRight_hom_app_down, homNatIsoMaxRight_inv_app, homNatIso_hom_app_down, homNatIso_inv_app_down, has_corepresentation, mk', has_representation, mk', comp_homEquiv_symm, coyoneda_homEquiv, equivOfIsoObj_apply, equivOfIsoObj_symm_apply, equivUliftYonedaIso_apply, equivUliftYonedaIso_symm_apply_homEquiv, ext, ext_iff, homEquiv_comp, homEquiv_eq, homEquiv_unop_comp, isRepresentable, ofIsoObj_homEquiv, uniqueUpToIso_hom, uniqueUpToIso_inv, coreprW_hom_app, corepresentableByUliftFunctorEquiv_apply_homEquiv, corepresentableByUliftFunctorEquiv_symm_apply_homEquiv, instIsCorepresentableCompUliftFunctor, instIsCorepresentableObjOppositeTypeCoyoneda, instIsRepresentableCompOppositeUliftFunctor, instIsRepresentableObjOppositeTypeYoneda, isCorepresentable_comp_uliftFunctor_iff, isRepresentable_comp_uliftFunctor_iff, reprW_hom_app, representableByUliftFunctorEquiv_apply_homEquiv, representableByUliftFunctorEquiv_symm_apply_homEquiv, sectionsEquivHom_apply_app, sectionsEquivHom_naturality, sectionsEquivHom_naturality_symm, uliftCoyonedaCoreprXIso_hom_app, uliftYonedaReprXIso_hom_app, instFaithfulFunctorOppositeTypeUliftYoneda, instFullFunctorOppositeTypeUliftYoneda, fullyFaithful_preimage, isIso, naturality, obj_map_id, yoneda_faithful, yoneda_full, corepresentable_of_natIso, coyonedaEquiv_apply, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map, coyonedaEquiv_naturality, coyonedaEquiv_symm_app_apply, coyonedaEquiv_symm_map, coyonedaEvaluation_map_down, coyonedaPairingExt, coyonedaPairingExt_iff, coyonedaPairing_map, hom_ext_uliftCoyoneda, hom_ext_uliftYoneda, hom_ext_yoneda, instIsCorepresentableIdType, isIso_iff_coyoneda_map_bijective, isIso_iff_isIso_coyoneda_map, isIso_iff_isIso_yoneda_map, isIso_iff_yoneda_map_bijective, isIso_of_coyoneda_map_bijective, isIso_of_yoneda_map_bijective, isRepresentable_of_natIso, map_coyonedaEquiv, map_yonedaEquiv, map_yonedaEquiv', sectionsFunctorNatIsoCoyoneda_hom_app_app, sectionsFunctorNatIsoCoyoneda_inv_app_coe, uliftCoyonedaEquiv_apply, uliftCoyonedaEquiv_comp, uliftCoyonedaEquiv_naturality, uliftCoyonedaEquiv_symm_apply_app, uliftCoyonedaEquiv_symm_map, uliftCoyonedaEquiv_symm_map_assoc, uliftCoyonedaEquiv_uliftCoyoneda_map, uliftCoyonedaIsoCoyoneda_hom_app_app, uliftCoyonedaIsoCoyoneda_inv_app_app_down, uliftYonedaEquiv_apply, uliftYonedaEquiv_comp, uliftYonedaEquiv_naturality, uliftYonedaEquiv_symm_apply_app, uliftYonedaEquiv_symm_map, uliftYonedaEquiv_symm_map_assoc, uliftYonedaEquiv_uliftYoneda_map, uliftYonedaIsoYoneda_hom_app_app, uliftYonedaIsoYoneda_inv_app_app_down, uliftYonedaMap_app_apply, uliftYoneda_map_app, uliftYoneda_map_app_down, uliftYoneda_obj_map, uliftYoneda_obj_map_down, uliftYoneda_obj_obj, yonedaEquiv_apply, yonedaEquiv_comp, yonedaEquiv_naturality, yonedaEquiv_naturality', yonedaEquiv_symm_app_apply, yonedaEquiv_symm_map, yonedaEquiv_symm_naturality_left, yonedaEquiv_symm_naturality_right, yonedaEquiv_yoneda_map, yonedaEvaluation_map_down, yonedaMap_app_apply, yonedaPairingExt, yonedaPairingExt_iff, yonedaPairing_map, yoneda_map_app, yoneda_obj_map, yoneda_obj_obj	147
Total	232

CategoryTheory

Definitions

Name	Category	Theorems
coyoneda 📖	CompOp	153 math math: Functor.functorHomEquiv_apply_app, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, Functor.natTransEquiv_apply_app, uliftCoyonedaIsoCoyoneda_hom_app_app, coyonedaEquiv_symm_app_apply, GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, sheafOver_val, cocones_map_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, FunctorToTypes.functorHomEquiv_symm_apply_app_app, Functor.CorepresentableBy.uniqueUpToIso_inv, whiskering_linearCoyoneda, Adjunction.compCoyonedaIso_inv_app_app, Limits.colimitCoyonedaHomIsoLimit'_π_apply, MonoidalCategory.DayConvolution.corepresentableBy₂_homEquiv, Limits.coyonedaCompLimIsoCones_inv_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, Functor.IsCoverDense.isoOver_hom_app, Coyoneda.objOpOp_inv_app, uliftCoyonedaIsoCoyoneda_inv_app_app_down, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, coyonedaEquiv_comp, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app, IsCofiltered.iff_nonempty_limit, Coyoneda.objOpOp_hom_app, Presheaf.isLimit_iff_isSheafFor_presieve, Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc, Limits.limitCompCoyonedaIsoCone_hom_app, preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall, isFinitelyPresentable_iff_preservesFilteredColimitsOfSize, AddCommGrpCat.coyonedaForget_inv_app_app, Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π, AddCommGrpCat.coyonedaForget_hom_app_app_hom, Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc, coyoneda_preservesLimits, Functor.coreprW_hom_app, Functor.natTransEquiv_symm_apply_app, Coyoneda.colimitCocone_ι_app, Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, CommMonCat.coyonedaForget_inv_app_app, HomologicalComplex.instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj, sectionsFunctorNatIsoCoyoneda_inv_app_coe, Presheaf.isSeparated_iff_subsingleton, FunctorToTypes.rightAdj_map_app, MonoidalCategory.DayConvolution.corepresentableBy₂'_homEquiv, Limits.whiskeringLimYonedaIsoCones_inv_app_app, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, Limits.colimitCoyonedaHomIsoLimitUnop_π_apply, FunctorToTypes.rightAdj_map_app_app, isSeparator_iff_faithful_coyoneda_obj, isDetector_iff_reflectsIsomorphisms_coyoneda_obj, Limits.compCoyonedaSectionsEquiv_symm_apply_coe, Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, Adjunction.corepresentableBy_homEquiv, Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app, IsGrothendieckAbelian.preservesColimit_coyoneda_obj_of_mono, coyonedaEquiv_naturality, coyonedaEquiv_apply, Limits.compCoyonedaSectionsEquiv_apply_app, Functor.functorHom_ext_iff, Coyoneda.naturality, MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app, MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, Enriched.Functor.natTransEquiv_symm_app_app_apply, coyonedaPreservesLimitsOfShape, instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable, Coyoneda.colimitCoconeIsColimit_desc, Coyoneda.colimitCocone_pt, preservesFilteredColimits_coyoneda, ObjectProperty.IsDetecting.isIso_iff_of_mono, FunctorToTypes.functorHomEquiv_apply_app, Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π, Functor.instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined, CommGrpCat.coyonedaForget_hom_app_app_hom, coyonedaEquiv_coyoneda_map, IsDetecting.isIso_iff_of_mono, Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, Adjunction.compCoyonedaIso_hom_app_app, MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_app, Limits.limitCompCoyonedaIsoCone_inv, AddCommMonCat.coyonedaForget_inv_app_app, sectionsFunctorNatIsoCoyoneda_hom_app_app, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app, Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc, Functor.IsCoverDense.sheafCoyonedaHom_app, Functor.IsCoverDense.homOver_app, MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_app, Functor.CorepresentableBy.uniqueUpToIso_hom, FunctorToTypes.rightAdj_obj_map_app, GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, Coyoneda.instHasColimitObjOppositeFunctorTypeCoyoneda, Functor.instIsCorepresentableObjOppositeTypeCoyoneda, Coyoneda.coyoneda_full, Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, preservesColimit_coyoneda_of_finitePresentation, Limits.whiskeringLimYonedaIsoCones_hom_app_app_app, Square.isPullback_iff_map_coyoneda_isPullback, FunctorToTypes.rightAdj_obj_obj, Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc, isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj, MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app, CommGrpCat.coyonedaForget_inv_app_app, MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app, Functor.IsCoverDense.isoOver_inv_app, CommMonCat.coyonedaForget_hom_app_app_hom, MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, isIso_iff_isIso_coyoneda_map, Limits.colimitCoyonedaHomIsoLimit_π_apply, Limits.coneOfSectionCompCoyoneda_π, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, coyoneda_preservesLimit, coyonedaPairing_map, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, Coyoneda.fullyFaithful_preimage, MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, Limits.Cocone.extend_ι, PreGaloisCategory.PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda, MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_app, coyonedaEquiv_symm_map, coyonedaPairingExt_iff, Presheaf.isLimit_iff_isSheafFor, AddCommMonCat.coyonedaForget_hom_app_app_hom, instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda, coyonedaFunctor_preservesLimits, isFinitelyPresentable_iff_preservesFilteredColimits, yonedaYonedaColimit_app_inv, SmallObject.preservesColimit, coyonedaFunctor_reflectsLimits, PreGaloisCategory.PointedGaloisObject.cocone_app, GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_comp_coyoneda, Limits.coyonedaCompLimIsoCones_hom_app_app, Functor.leftAdjointObjIsDefined_iff, Functor.CorepresentableBy.coyoneda_homEquiv, Presheaf.subsingleton_iff_isSeparatedFor, Limits.colimitCoyonedaHomIsoLimitLeftOp_π_apply, CommRingCat.preservesFilteredColimits_coyoneda, Limits.Cocone.extensions_app, CommRingCat.preservesColimit_coyoneda_of_finitePresentation, MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv, map_coyonedaEquiv, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, Functor.functorHomEquiv_symm_apply_app_app, preservesColimitsOfShape_of_isCardinalPresentable, whiskering_preadditiveCoyoneda, Coyoneda.coyoneda_faithful
coyonedaCompYonedaObj 📖	CompOp	—
coyonedaEquiv 📖	CompOp	7 math math: coyonedaEquiv_symm_app_apply, coyonedaEquiv_comp, coyonedaEquiv_naturality, coyonedaEquiv_apply, coyonedaEquiv_coyoneda_map, coyonedaEquiv_symm_map, map_coyonedaEquiv
coyonedaEvaluation 📖	CompOp	1 math math: coyonedaEvaluation_map_down
coyonedaLemma 📖	CompOp	—
coyonedaPairing 📖	CompOp	1 math math: coyonedaPairing_map
curriedCoyonedaLemma 📖	CompOp	—
curriedCoyonedaLemma' 📖	CompOp	—
curriedYonedaLemma 📖	CompOp	—
curriedYonedaLemma' 📖	CompOp	—
largeCurriedCoyonedaLemma 📖	CompOp	—
largeCurriedYonedaLemma 📖	CompOp	1 math math: GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app
prodCategoryInstance1 📖	CompOp	—
prodCategoryInstance2 📖	CompOp	3 math math: yonedaPairing_map, yonedaPairingExt_iff, yonedaEvaluation_map_down
sectionsFunctorNatIsoCoyoneda 📖	CompOp	2 math math: sectionsFunctorNatIsoCoyoneda_inv_app_coe, sectionsFunctorNatIsoCoyoneda_hom_app_app
uliftCoyoneda 📖	CompOp	22 math math: Adjunction.compUliftCoyonedaIso_hom_app_app_down, uliftCoyonedaEquiv_apply, uliftCoyonedaIsoCoyoneda_hom_app_app, Functor.uliftCoyonedaCoreprXIso_hom_app, Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down, uliftCoyonedaIsoCoyoneda_inv_app_app_down, uliftCoyonedaEquiv_uliftCoyoneda_map, uliftCoyonedaEquiv_symm_apply_app, Coyoneda.ULiftCoyoneda.instFullOppositeFunctorTypeUliftCoyoneda, Adjunction.compUliftCoyonedaIso_inv_app_app_down, Functor.FullyFaithful.homNatIso'_hom_app_down, Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv, Functor.CorepresentableBy.equivUliftCoyonedaIso_apply, uliftCoyonedaEquiv_naturality, uliftCoyonedaEquiv_symm_map_assoc, Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down, Functor.FullyFaithful.homNatIso'_inv_app_down, isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj, uliftCoyonedaEquiv_symm_map, instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable, uliftCoyonedaEquiv_comp, Coyoneda.ULiftCoyoneda.instFaithfulOppositeFunctorTypeUliftCoyoneda
uliftCoyonedaEquiv 📖	CompOp	7 math math: uliftCoyonedaEquiv_apply, uliftCoyonedaEquiv_uliftCoyoneda_map, uliftCoyonedaEquiv_symm_apply_app, uliftCoyonedaEquiv_naturality, uliftCoyonedaEquiv_symm_map_assoc, uliftCoyonedaEquiv_symm_map, uliftCoyonedaEquiv_comp
uliftCoyonedaIsoCoyoneda 📖	CompOp	2 math math: uliftCoyonedaIsoCoyoneda_hom_app_app, uliftCoyonedaIsoCoyoneda_inv_app_app_down
uliftCoyonedaRightOpCompCoyoneda 📖	CompOp	—
uliftYoneda 📖	CompOp	72 math math: Functor.FullyFaithful.homNatIsoMaxRight_inv_app, ULiftYoneda.instFullFunctorOppositeTypeUliftYoneda, Subfunctor.Subpresheaf.range_eq_ofSection', Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down, Presheaf.functorToRepresentables_map, Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj, uliftYonedaEquiv_symm_apply_app, Subfunctor.Subpresheaf.ofSection_eq_range', Functor.FullyFaithful.homNatIso_inv_app_down, uliftYonedaEquiv_apply, Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_down, uliftYonedaEquiv_symm_map, uliftYonedaEquiv_naturality, Subfunctor.ofSection_eq_range', Presheaf.restrictedULiftYoneda_map_app, Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, Presheaf.functorToRepresentables_obj, Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app, uliftYonedaEquiv_comp, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app, Sieve.sieveOfUliftSubfunctor_apply, Sieve.uliftNatTransOfLe_comm, uliftYoneda_obj_map, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app, uliftYoneda_obj_obj, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, Presheaf.tautologicalCocone'_pt, uliftYonedaEquiv_uliftYoneda_map, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, Subfunctor.range_eq_ofSection', Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv, uliftYoneda_obj_map_down, Sieve.uliftFunctorInclusion_app, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, uliftYoneda_map_app, Functor.uliftYonedaReprXIso_hom_app, Presheaf.instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize, Functor.IsRepresentedBy.uliftYonedaIso_hom, uliftYoneda_map_app_down, Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj, Sieve.uliftFunctorInclusion_is_mono, uliftYonedaIsoYoneda_hom_app_app, Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_down, Presheaf.map_comp_uliftYonedaEquiv_down_assoc, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv, ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda, Presheaf.map_comp_uliftYonedaEquiv_down, Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, Functor.RepresentableBy.equivUliftYonedaIso_apply, Presheaf.tautologicalCocone'_ι_app, Presheaf.coconeOfRepresentable_ι_app, Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, Sieve.uliftFunctorInclusion_top_isIso, Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, uliftYonedaMap_app_apply, Functor.FullyFaithful.homNatIso_hom_app_down, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp_naturality, uliftYonedaIsoYoneda_inv_app_app_down, uliftYonedaEquiv_symm_map_assoc, uliftYonedaFunctor_preservesLimits, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map, Sieve.toUliftFunctor_app_down_coe, Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp_naturality_assoc, Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap
uliftYonedaEquiv 📖	CompOp	27 math math: Subfunctor.Subpresheaf.range_eq_ofSection', Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, uliftYonedaEquiv_symm_apply_app, Subfunctor.Subpresheaf.ofSection_eq_range', uliftYonedaEquiv_apply, uliftYonedaEquiv_symm_map, uliftYonedaEquiv_naturality, Subfunctor.ofSection_eq_range', uliftYonedaEquiv_comp, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, uliftYonedaEquiv_uliftYoneda_map, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, Subfunctor.range_eq_ofSection', Presheaf.uliftYonedaAdjunction_homEquiv_app, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, Functor.IsRepresentedBy.uliftYonedaIso_hom, Presheaf.uliftYonedaAdjunction_unit_app_app, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj, Presheaf.map_comp_uliftYonedaEquiv_down_assoc, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv, Presheaf.map_comp_uliftYonedaEquiv_down, Presheaf.coconeOfRepresentable_ι_app, uliftYonedaEquiv_symm_map_assoc, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map
uliftYonedaIsoYoneda 📖	CompOp	2 math math: uliftYonedaIsoYoneda_hom_app_app, uliftYonedaIsoYoneda_inv_app_app_down
uliftYonedaMap 📖	CompOp	2 math math: uliftYonedaMap_app_apply, Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap
uliftYonedaOpCompCoyoneda 📖	CompOp	1 math math: GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app
yoneda 📖	CompOp	274 math math: Limits.colimitHomIsoLimitYoneda'_hom_comp_π, Functor.FullyFaithful.homNatIsoMaxRight_inv_app, Adjunction.compUliftCoyonedaIso_hom_app_app_down, instSmallOppositeObjFunctorTypeYoneda, Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, yoneda_preservesLimit, Limits.colimitHomIsoLimitYoneda_hom_comp_π, SSet.stdSimplex.coe_triangle_down_toOrderHom, CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app, shrinkYoneda_map, GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, OverPresheafAux.costructuredArrowPresheafToOver_map, Subfunctor.Subpresheaf.range_eq_ofSection', Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom, CategoryOfElements.costructuredArrowYonedaEquivalence_functor, OverPresheafAux.unitAux_hom, IndParallelPairPresentation.hf, Subfunctor.Subpresheaf.range_eq_ofSection, CondensedMod.IsSolid.isIso_solidification_map, NonemptyParallelPairPresentationAux.hf, yoneda_map_app, OverPresheafAux.restrictedYoneda_map, Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, Limits.IsIndObject.isFiltered, OverPresheafAux.restrictedYoneda_obj, Limits.IndObjectPresentation.extend_ι_app_app, Limits.opCompYonedaSectionsEquiv_symm_apply_coe, Yoneda.naturality, GrothendieckTopology.yoneda_map_val, Limits.yonedaCompLimIsoCocones_inv_app, Subfunctor.ofSection_eq_range, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, yonedaEquiv_apply, Limits.IndObjectPresentation.instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, IsFiltered.iff_nonempty_limit, Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down, Coyoneda.objOpOp_inv_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, uliftCoyonedaIsoCoyoneda_inv_app_app_down, Adjunction.compYonedaIso_hom_app_app, PresheafOfModules.freeYonedaEquiv_symm_app, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, Functor.RepresentableBy.coyoneda_homEquiv, Limits.colimitYonedaHomIsoLimit'_π_apply, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app, GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Limits.colimitHomIsoLimitYoneda'_hom_comp_π_assoc, Limits.compYonedaSectionsEquiv_apply_app, Functor.imageSieve_eq_imageSieve, Functor.rightAdjointObjIsDefined_iff, yonedaFunctor_reflectsLimits, GrothendieckTopology.MayerVietorisSquare.isPushout, Functor.FullyFaithful.homNatIso_inv_app_down, OverPresheafAux.counitForward_naturality₁, Coyoneda.objOpOp_hom_app, Limits.Cone.extend_π, extensiveTopology.isSheaf_yoneda_obj, Presheaf.isSheaf_yoneda', Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_down, shrinkYoneda_obj, Adjunction.compUliftCoyonedaIso_inv_app_app_down, OverPresheafAux.YonedaCollection.map₂_snd, Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app, OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, Limits.colimitYonedaHomIsoLimit_π_apply, equivYoneda'_inv_val, OverPresheafAux.counitForward_val_snd, Limits.yonedaCompLimIsoCocones_hom_app_app, Yoneda.yoneda_faithful, OverPresheafAux.yonedaCollectionFunctor_obj, Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, isIso_iff_isIso_yoneda_map, Functor.IsCoverDense.presheafIso_hom_app, GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Functor.instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined, Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app, yoneda_obj_obj, Limits.IndObjectPresentation.toCostructuredArrow_obj_right_as, Presheaf.freeYoneda_map, whiskering_linearYoneda, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, Sieve.sieveOfUliftSubfunctor_apply, yonedaEquiv_yoneda_map, CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, Limits.opCompYonedaSectionsEquiv_apply_app, CategoryOfElements.costructuredArrowYonedaEquivalence_inverse, Limits.isIndObject_iff, Presheaf.final_toCostructuredArrow_comp_pre, yoneda_preservesLimitsOfShape, Sieve.natTransOfLe_comm, typeEquiv_counitIso_inv_app_val_app, OverPresheafAux.counitAuxAux_inv, SSet.stdSimplex.coe_edge_down_toOrderHom, Limits.IsIndObject.finallySmall, yonedaEquiv_naturality', Functor.instIsRepresentableObjOppositeTypeYoneda, OverPresheafAux.restrictedYonedaObj_map, Limits.IndObjectPresentation.yoneda_isColimit_desc, whiskering_preadditiveYoneda, yoneda_obj_map, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app, CategoryOfElements.fromCostructuredArrow_obj_snd, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, OverPresheafAux.counitBackward_counitForward, Limits.colimitHomIsoLimitYoneda_hom_comp_π_assoc, Limits.IndObjectPresentation.toCostructuredArrow_obj_left, Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits, Sieve.functorInclusion_app, Limits.IndObjectPresentation.toCostructuredArrow_map_left, isCodetector_iff_reflectsIsomorphisms_yoneda_obj, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, Subfunctor.range_eq_ofSection', Functor.FullyFaithful.homNatIso'_hom_app_down, regularTopology.isSheaf_yoneda_obj, Limits.isIndObject_limit_comp_yoneda, Limits.isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits, uliftYoneda_obj_map_down, Limits.colimitHomIsoLimitYoneda'_inv_comp_π_assoc, Limits.IndObjectPresentation.yoneda_ι_app, Sieve.sieveOfSubfunctor_apply, coherentTopology.isSheaf_yoneda_obj, Limits.IndObjectPresentation.toCostructuredArrow_obj_hom, yonedaFunctor_preservesLimits, OverPresheafAux.counitAux_hom, CategoryOfElements.fromCostructuredArrow_map_coe, Adjunction.compYonedaIso_inv_app_app, Limits.isIndObject_yoneda, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app, Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap, Sieve.yonedaFamily_fromCocone_compatible, OverPresheafAux.unitAuxAux_inv_app_fst, Limits.IndObjectPresentation.ofCocone_I, OverPresheafAux.unitAuxAux_inv_app_snd_coe, PresheafOfModules.Elements.fromFreeYoneda_app_apply, SSet.horn.edge₃_coe_down, Functor.RepresentableBy.uniqueUpToIso_hom, uliftYoneda_map_app, Yoneda.yoneda_full, SSet.stdSimplex.const_down_toOrderHom, equivYoneda_hom_app, Presieve.IsSheafFor.functorInclusion_comp_extend, yonedaMap_app_apply, Limits.limitCompYonedaIsoCocone_inv, CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality, Limits.coneOfSectionCompYoneda_π, Limits.IndObjectPresentation.ofCocone_isColimit, OverPresheafAux.restrictedYonedaObj_obj, OverPresheafAux.MakesOverArrow.app, CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso, OverPresheafAux.OverArrows.app_val, Subfunctor.range_eq_ofSection, yonedaPairing_map, GrothendieckTopology.MayerVietorisSquare.shortComplex_g, uliftYoneda_map_app_down, GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, OverPresheafAux.restrictedYonedaObjMap₁_app, GrothendieckTopology.yoneda_obj_val, IndParallelPairPresentation.hg, yonedaPairingExt_iff, isCoseparator_iff_faithful_yoneda_obj, instPresheafIsFiniteObjFunctorOppositeTypeYoneda, typeEquiv_counitIso_hom_app_val_app, CategoryOfElements.toCostructuredArrow_obj, OverPresheafAux.yonedaCollectionFunctor_map, Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down, OverPresheafAux.YonedaCollection.mk_snd, Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj, Functor.CorepresentableBy.equivUliftCoyonedaIso_apply, CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app, OverPresheafAux.YonedaCollection.map₁_comp, PresheafOfModules.pullbackObjIsDefined_free_yoneda, uliftYonedaIsoYoneda_hom_app_app, IsCodetecting.isIso_iff_of_epi, Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_down, equivYoneda_inv_app, yoneda'_obj_val, Limits.IndObjectPresentation.extend_isColimit_desc_app, Limits.IndObjectPresentation.ofCocone_ι, Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down, Presheaf.map_comp_uliftYonedaEquiv_down_assoc, Functor.RepresentableBy.uniqueUpToIso_inv, Sieve.forallYonedaIsSheaf_iff_colimit, Sieve.functorInclusion_top_isIso, Limits.IndObjectPresentation.ofCocone_F, Functor.FullyFaithful.homNatIso'_inv_app_down, yonedaEquiv_naturality, Limits.IndObjectPresentation.ofCocone_ℐ, typeEquiv_functor_map_val_app, map_yonedaEquiv, GrothendieckTopology.MayerVietorisSquare.shortComplex_f, OverPresheafAux.YonedaCollection.map₁_id, yoneda_preservesLimits, CommRingCat.instIsRightAdjointOppositeObjFunctorTypeYoneda, Presieve.IsSheafFor.functorInclusion_comp_extend_assoc, Presheaf.map_comp_uliftYonedaEquiv_down, Sieve.functorInclusion_is_mono, Injective.injective_iff_preservesEpimorphisms_yoneda_obj, Limits.limitCompYonedaIsoCocone_hom_app, Limits.colimitYonedaHomIsoLimitOp_π_apply, Presheaf.tautologicalCocone_ι_app, Functor.RepresentableBy.equivUliftYonedaIso_apply, CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, yoneda'_comp, Presieve.extension_iff_amalgamation, SSet.horn.primitiveEdge_coe_down, CategoryOfElements.fromCostructuredArrow_obj_mk, Limits.IndObjectPresentation.cocone_pt, Yoneda.fullyFaithful_preimage, equivYoneda'_hom_val, PresheafOfModules.freeYonedaEquiv_comp, cones_map_app_app, Adjunction.representableBy_homEquiv, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, Limits.IndizationClosedUnderFilteredColimitsAux.isFiltered, instSmallHomFunctorOppositeTypeColimitCompYoneda, instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda, Presieve.isSheaf_yoneda', uliftYonedaMap_app_apply, OverPresheafAux.counitForward_counitBackward, OverPresheafAux.costructuredArrowPresheafToOver_obj, Sieve.equalizer_eq_equalizerSieve, Functor.FullyFaithful.homNatIso_hom_app_down, Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app, OverPresheafAux.YonedaCollection.map₁_snd, yonedaEquiv_symm_map, Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, Sieve.toFunctor_app_coe, Functor.reprW_hom_app, Limits.colimitHomIsoLimitYoneda_inv_comp_π, yonedaYonedaColimit_app_inv, Limits.Cone.extensions_app, yonedaEquiv_symm_naturality_left, ObjectProperty.IsCodetecting.isIso_iff_of_epi, yonedaEquiv_symm_naturality_right, Limits.IndObjectPresentation.yoneda_I, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, OverPresheafAux.OverArrows.map_val, uliftYonedaIsoYoneda_inv_app_app_down, Limits.colimitYonedaHomIsoLimitRightOp_π_apply, Presheaf.tautologicalCocone_pt, yoneda'_map_val, OverPresheafAux.map_mkPrecomp_eqToHom, NonemptyParallelPairPresentationAux.hg, OverPresheafAux.counitAuxAux_hom, Limits.colimitHomIsoLimitYoneda_inv_comp_π_assoc, yoneda_obj_isGeneratedBy, Subfunctor.Subpresheaf.ofSection_eq_range, Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, OverPresheafAux.YonedaCollection.map₂_fst, Sieve.toUliftFunctor_app_down_coe, Limits.IndObjectPresentation.yoneda_F, OverPresheafAux.counitForward_val_fst, Limits.IndObjectPresentation.yoneda_ℐ, CategoryOfElements.fromCostructuredArrow_obj_fst, Yoneda.obj_map_id, map_yonedaEquiv', CategoryOfElements.toCostructuredArrow_map, CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app, Presheaf.freeYoneda_obj, colimitYonedaHomEquiv_π_apply, Sheaf.isSheaf_yoneda_obj, yonedaEquiv_symm_app_apply, Limits.colimitHomIsoLimitYoneda'_inv_comp_π, Square.isPushout_iff_op_map_yoneda_isPullback, Limits.compYonedaSectionsEquiv_symm_apply_coe, yonedaEquiv_comp, OverPresheafAux.counitForward_naturality₂
yonedaEquiv 📖	CompOp	29 math math: GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, Subfunctor.Subpresheaf.range_eq_ofSection, Subfunctor.ofSection_eq_range, yonedaEquiv_apply, OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, yonedaEquiv_yoneda_map, yonedaEquiv_naturality', CategoryOfElements.fromCostructuredArrow_obj_snd, CategoryOfElements.fromCostructuredArrow_map_coe, OverPresheafAux.unitAuxAux_inv_app_fst, OverPresheafAux.unitAuxAux_inv_app_snd_coe, OverPresheafAux.MakesOverArrow.app, OverPresheafAux.OverArrows.app_val, Subfunctor.range_eq_ofSection, CategoryOfElements.toCostructuredArrow_obj, yonedaEquiv_naturality, map_yonedaEquiv, OverPresheafAux.MakesOverArrow.of_arrow, Presieve.extension_iff_amalgamation, CategoryOfElements.fromCostructuredArrow_obj_mk, yonedaEquiv_symm_map, yonedaEquiv_symm_naturality_left, yonedaEquiv_symm_naturality_right, Subfunctor.Subpresheaf.ofSection_eq_range, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, map_yonedaEquiv', CategoryOfElements.toCostructuredArrow_map, yonedaEquiv_symm_app_apply, yonedaEquiv_comp
yonedaEvaluation 📖	CompOp	1 math math: yonedaEvaluation_map_down
yonedaLemma 📖	CompOp	—
yonedaMap 📖	CompOp	3 math math: Functor.imageSieve_eq_imageSieve, Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap, yonedaMap_app_apply
yonedaOpCompYonedaObj 📖	CompOp	—
yonedaPairing 📖	CompOp	1 math math: yonedaPairing_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
corepresentable_of_natIso 📖	mathematical	—	Functor.IsCorepresentable	—	Functor.CorepresentableBy.isCorepresentable
coyonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike coyonedaEquiv NatTrans.app CategoryStruct.id	—	—
coyonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike coyonedaEquiv CategoryStruct.comp NatTrans.app	—	—
coyonedaEquiv_coyoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike coyonedaEquiv Functor.map Quiver.Hom.op	—	coyonedaEquiv_apply Category.comp_id
coyonedaEquiv_naturality 📖	mathematical	—	Functor.map types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike coyonedaEquiv CategoryStruct.comp Quiver.Hom.op	—	NatTrans.naturality Category.id_comp Category.comp_id
coyonedaEquiv_symm_app_apply 📖	mathematical	—	NatTrans.app types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm coyonedaEquiv Functor.map	—	—
coyonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv Functor.obj types Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm coyonedaEquiv Functor.map CategoryStruct.comp Quiver.Hom.op	—	Equiv.surjective coyonedaEquiv_naturality Equiv.symm_apply_apply
coyonedaEvaluation_map_down 📖	mathematical	—	Functor.obj Functor types prod' Functor.category evaluationUncurried Functor.map coyonedaEvaluation NatTrans.app Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	—	—
coyonedaPairingExt 📖	—	NatTrans.app types Opposite.unop Functor Opposite Functor.obj prod' Functor.category Category.opposite Functor.prod Functor.rightOp coyoneda Functor.id	—	—	NatTrans.ext
coyonedaPairingExt_iff 📖	mathematical	—	NatTrans.app types Opposite.unop Functor Opposite Functor.obj prod' Functor.category Category.opposite Functor.prod Functor.rightOp coyoneda Functor.id	—	coyonedaPairingExt
coyonedaPairing_map 📖	mathematical	—	Functor.map Functor types prod' Functor.category coyonedaPairing CategoryStruct.comp Category.toCategoryStruct Functor.obj Opposite Category.opposite coyoneda Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Quiver.Hom Functor.prod Functor.rightOp Functor.id	—	—
hom_ext_uliftCoyoneda 📖	—	CategoryStruct.comp Functor types Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda	—	—	NatTrans.ext' types_ext FunctorToTypes.map_id_apply
hom_ext_uliftYoneda 📖	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj uliftYoneda	—	—	NatTrans.ext' types_ext FunctorToTypes.map_id_apply
hom_ext_yoneda 📖	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj yoneda	—	—	NatTrans.ext' types_ext Equiv.apply_symm_apply
instIsCorepresentableIdType 📖	mathematical	—	Functor.IsCorepresentable types Functor.id	—	corepresentable_of_natIso Functor.instIsCorepresentableObjOppositeTypeCoyoneda
isIso_iff_coyoneda_map_bijective 📖	mathematical	—	IsIso Function.Bijective Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp	—	isIso_iff_bijective NatIso.isIso_app_of_isIso Functor.map_isIso isIso_op isIso_of_coyoneda_map_bijective
isIso_iff_isIso_coyoneda_map 📖	mathematical	—	IsIso types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op NatTrans.app Functor.map Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	isIso_iff_coyoneda_map_bijective isIso_iff_bijective
isIso_iff_isIso_yoneda_map 📖	mathematical	—	IsIso types Functor.obj Opposite Category.opposite Functor Functor.category yoneda Opposite.op NatTrans.app Functor.map	—	isIso_iff_yoneda_map_bijective isIso_iff_bijective
isIso_iff_yoneda_map_bijective 📖	mathematical	—	IsIso Function.Bijective Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp	—	isIso_iff_bijective NatIso.isIso_app_of_isIso Functor.map_isIso isIso_of_yoneda_map_bijective
isIso_of_coyoneda_map_bijective 📖	mathematical	Function.Bijective Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp	IsIso	—	Category.id_comp Category.comp_id
isIso_of_yoneda_map_bijective 📖	mathematical	Function.Bijective Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.comp	IsIso	—	Category.assoc Category.comp_id Category.id_comp
isRepresentable_of_natIso 📖	mathematical	—	Functor.IsRepresentable	—	Functor.RepresentableBy.isRepresentable
map_coyonedaEquiv 📖	mathematical	—	Functor.map types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike coyonedaEquiv NatTrans.app	—	coyonedaEquiv_naturality coyonedaEquiv_comp coyonedaEquiv_coyoneda_map
map_yonedaEquiv 📖	mathematical	—	Functor.map Opposite Category.opposite types Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom Functor Functor.category Functor.obj yoneda EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv NatTrans.app	—	yonedaEquiv_naturality yonedaEquiv_comp yonedaEquiv_yoneda_map
map_yonedaEquiv' 📖	mathematical	—	Functor.map Opposite Category.opposite types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv NatTrans.app Quiver.Hom.unop	—	yonedaEquiv_naturality' yonedaEquiv_comp yonedaEquiv_yoneda_map
sectionsFunctorNatIsoCoyoneda_hom_app_app 📖	mathematical	—	NatTrans.app types Opposite.unop Functor Opposite.op Functor.obj Functor.category Functor.const Functor.sectionsFunctor Opposite Category.opposite coyoneda Iso.hom sectionsFunctorNatIsoCoyoneda Set Set.instMembership Functor.sections	—	—
sectionsFunctorNatIsoCoyoneda_inv_app_coe 📖	mathematical	—	Set Set.instMembership Functor.sections NatTrans.app Functor types Functor.category Functor.obj Opposite Category.opposite coyoneda Opposite.op Functor.const Functor.sectionsFunctor Iso.inv sectionsFunctorNatIsoCoyoneda Unique.instInhabited	—	—
uliftCoyonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda Opposite.unop EquivLike.toFunLike Equiv.instEquivLike uliftCoyonedaEquiv NatTrans.app CategoryStruct.id	—	—
uliftCoyonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda Opposite.unop EquivLike.toFunLike Equiv.instEquivLike uliftCoyonedaEquiv CategoryStruct.comp NatTrans.app	—	—
uliftCoyonedaEquiv_naturality 📖	mathematical	—	Functor.map types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda Opposite.op Opposite.unop EquivLike.toFunLike Equiv.instEquivLike uliftCoyonedaEquiv CategoryStruct.comp Quiver.Hom.op	—	FunctorToTypes.naturality Category.id_comp Category.comp_id
uliftCoyonedaEquiv_symm_apply_app 📖	mathematical	—	NatTrans.app types Functor.obj Opposite Category.opposite Functor Functor.category uliftCoyoneda DFunLike.coe Equiv Opposite.unop Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftCoyonedaEquiv Functor.map	—	—
uliftCoyonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv Functor.obj types Opposite.unop Opposite.op Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Opposite Category.opposite uliftCoyoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftCoyonedaEquiv Functor.map CategoryStruct.comp Quiver.Hom.op	—	Equiv.surjective uliftCoyonedaEquiv_naturality Equiv.symm_apply_apply
uliftCoyonedaEquiv_symm_map_assoc 📖	mathematical	—	CategoryStruct.comp Functor types Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftCoyonedaEquiv Functor.map Quiver.Hom.op	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' uliftCoyonedaEquiv_symm_map
uliftCoyonedaEquiv_uliftCoyoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj Opposite Category.opposite uliftCoyoneda Opposite.unop EquivLike.toFunLike Equiv.instEquivLike uliftCoyonedaEquiv Functor.map Quiver.Hom.unop	—	Category.comp_id
uliftCoyonedaIsoCoyoneda_hom_app_app 📖	mathematical	—	NatTrans.app types Functor.obj Opposite Category.opposite Functor Functor.category uliftCoyoneda coyoneda Iso.hom uliftCoyonedaIsoCoyoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
uliftCoyonedaIsoCoyoneda_inv_app_app_down 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category yoneda NatTrans.app coyoneda uliftCoyoneda Iso.inv uliftCoyonedaIsoCoyoneda	—	—
uliftYonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj uliftYoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv NatTrans.app CategoryStruct.id	—	—
uliftYonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj uliftYoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryStruct.comp NatTrans.app	—	—
uliftYonedaEquiv_naturality 📖	mathematical	—	Functor.map Opposite Category.opposite types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj uliftYoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv CategoryStruct.comp Quiver.Hom.unop	—	FunctorToTypes.naturality Category.comp_id Category.id_comp
uliftYonedaEquiv_symm_apply_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category uliftYoneda DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv Functor.map Quiver.Hom.op Opposite.unop	—	—
uliftYonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv Functor.obj Opposite Category.opposite types Opposite.op Opposite.unop Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category uliftYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv Functor.map CategoryStruct.comp Quiver.Hom.unop	—	Equiv.surjective uliftYonedaEquiv_naturality Equiv.symm_apply_apply
uliftYonedaEquiv_symm_map_assoc 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj uliftYoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm uliftYonedaEquiv Functor.map Quiver.Hom.unop	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' uliftYonedaEquiv_symm_map
uliftYonedaEquiv_uliftYoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj uliftYoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike uliftYonedaEquiv Functor.map	—	Category.id_comp
uliftYonedaIsoYoneda_hom_app_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category uliftYoneda yoneda Iso.hom uliftYonedaIsoYoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
uliftYonedaIsoYoneda_inv_app_app_down 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category yoneda NatTrans.app uliftYoneda Iso.inv uliftYonedaIsoYoneda	—	—
uliftYonedaMap_app_apply 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category uliftYoneda Functor.comp Functor.op uliftYonedaMap yoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Functor.map	—	—
uliftYoneda_map_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category Functor.whiskeringRight uliftFunctor yoneda Functor.map uliftYoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CategoryStruct.comp	—	—
uliftYoneda_map_app_down 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category yoneda NatTrans.app uliftYoneda Functor.map CategoryStruct.comp Category.toCategoryStruct Opposite.unop	—	—
uliftYoneda_obj_map 📖	mathematical	—	Functor.map Opposite Category.opposite types Functor.obj Functor Functor.category uliftYoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CategoryStruct.comp Quiver.Hom.unop	—	—
uliftYoneda_obj_map_down 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category yoneda Functor.map uliftYoneda CategoryStruct.comp Category.toCategoryStruct Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver	—	—
uliftYoneda_obj_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category uliftYoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
yonedaEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv NatTrans.app CategoryStruct.id	—	—
yonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryStruct.comp NatTrans.app	—	—
yonedaEquiv_naturality 📖	mathematical	—	Functor.map Opposite Category.opposite types Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom Functor Functor.category Functor.obj yoneda EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryStruct.comp	—	NatTrans.naturality Category.comp_id Category.id_comp
yonedaEquiv_naturality' 📖	mathematical	—	Functor.map Opposite Category.opposite types DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv CategoryStruct.comp Quiver.Hom.unop	—	yonedaEquiv_naturality
yonedaEquiv_symm_app_apply 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category yoneda DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv Functor.map Opposite.unop Quiver.Hom.op	—	—
yonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv Functor.obj Opposite Category.opposite types Opposite.op Opposite.unop Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category yoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv Functor.map CategoryStruct.comp Quiver.Hom.unop	—	Equiv.surjective yonedaEquiv_naturality' Equiv.symm_apply_apply
yonedaEquiv_symm_naturality_left 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj yoneda Functor.map DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv Quiver.Hom.op	—	Equiv.injective Equiv.apply_symm_apply yonedaEquiv_yoneda_map
yonedaEquiv_symm_naturality_right 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj yoneda DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm yonedaEquiv NatTrans.app	—	Equiv.injective Equiv.apply_symm_apply
yonedaEquiv_yoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike yonedaEquiv Functor.map	—	yonedaEquiv_apply Category.id_comp
yonedaEvaluation_map_down 📖	mathematical	—	Functor.obj Opposite Functor Category.opposite types prodCategoryInstance2 evaluationUncurried Functor.map yonedaEvaluation NatTrans.app Quiver.Hom CategoryStruct.toQuiver CategoryStruct.opposite Category.toCategoryStruct Functor.category	—	—
yonedaMap_app_apply 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Functor.obj Functor Functor.category yoneda Functor.comp Functor.op yonedaMap Functor.map Opposite.unop	—	—
yonedaPairingExt 📖	—	NatTrans.app Opposite Category.opposite types Opposite.unop Functor Functor.obj prodCategoryInstance2 prod' Functor.category Functor.prod Functor.op yoneda Functor.id	—	—	NatTrans.ext
yonedaPairingExt_iff 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Opposite.unop Functor Functor.obj prodCategoryInstance2 prod' Functor.category Functor.prod Functor.op yoneda Functor.id	—	yonedaPairingExt
yonedaPairing_map 📖	mathematical	—	Functor.map Opposite Functor Category.opposite types prodCategoryInstance2 yonedaPairing CategoryStruct.comp Category.toCategoryStruct Functor.category Functor.obj yoneda Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Quiver.Hom CategoryStruct.opposite prod' Functor.prod Functor.op Functor.id	—	—
yoneda_map_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite types Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CategoryStruct.comp Quiver.Hom.unop Functor.map Functor Functor.category yoneda	—	—
yoneda_obj_map 📖	mathematical	—	Functor.map Opposite Category.opposite types Functor.obj Functor Functor.category yoneda CategoryStruct.comp Category.toCategoryStruct Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver	—	—
yoneda_obj_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite types Functor Functor.category yoneda Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—

CategoryTheory.Coyoneda

Definitions

Name	Category	Theorems
ext 📖	CompOp	—
fullyFaithful 📖	CompOp	3 math math: CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv, CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom, fullyFaithful_preimage
objOpOp 📖	CompOp	2 math math: objOpOp_inv_app, objOpOp_hom_app
opIso 📖	CompOp	—
preimage 📖	CompOp	—
punitIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyoneda_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda	—	CategoryTheory.Functor.FullyFaithful.faithful
coyoneda_full 📖	mathematical	—	CategoryTheory.Functor.Full Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda	—	CategoryTheory.Functor.FullyFaithful.full
fullyFaithful_preimage 📖	mathematical	—	CategoryTheory.Functor.FullyFaithful.preimage Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda fullyFaithful Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id	—	—
isIso 📖	mathematical	—	CategoryTheory.IsIso Opposite CategoryTheory.Category.opposite	—	CategoryTheory.isIso_of_fully_faithful coyoneda_full coyoneda_faithful
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	CategoryTheory.FunctorToTypes.naturality
objOpOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op CategoryTheory.yoneda CategoryTheory.Iso.hom objOpOp DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.opEquiv	—	—
objOpOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.coyoneda Opposite.op CategoryTheory.Iso.inv objOpOp DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.opEquiv	—	—

CategoryTheory.Coyoneda.ULiftCoyoneda

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulOppositeFunctorTypeUliftCoyoneda 📖	mathematical	—	CategoryTheory.Functor.Faithful Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftCoyoneda	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullOppositeFunctorTypeUliftCoyoneda 📖	mathematical	—	CategoryTheory.Functor.Full Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftCoyoneda	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.Functor

Definitions

Name	Category	Theorems
CorepresentableBy 📖	CompData	7 math math: CorepresentableBy.equivOfIsoObj_symm_apply, CorepresentableBy.equivOfIsoObj_apply, corepresentableByUliftFunctorEquiv_apply_homEquiv, corepresentableByUliftFunctorEquiv_symm_apply_homEquiv, CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv, CorepresentableBy.equivUliftCoyonedaIso_apply, IsCorepresentable.has_corepresentation
IsCorepresentable 📖	CompData	19 math math: CategoryTheory.Types.instIsCorepresentableForgetTypeHom, GrpCat.forget_isCorepresentable, CorepresentableBy.isCorepresentable, instIsCorepresentableCompUliftFunctor, HomologicalComplex.instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp, CommGrpCat.forget_isCorepresentable, IsCorepresentable.mk', AddMonCat.forget_isCorepresentable, MonCat.forget_isCorepresentable, CategoryTheory.instIsCorepresentableIdType, instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined, CategoryTheory.corepresentable_of_natIso, instIsCorepresentableObjOppositeTypeCoyoneda, AddCommMonCat.forget_isCorepresentable, AddGrpCat.forget_isCorepresentable, AddCommGrpCat.forget_isCorepresentable, leftAdjointObjIsDefined_iff, isCorepresentable_comp_uliftFunctor_iff, CommMonCat.forget_isCorepresentable
IsRepresentable 📖	CompData	13 math math: AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable, rightAdjointObjIsDefined_iff, CategoryTheory.essImage_yonedaMon, CategoryTheory.essImage_yonedaGrp, instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined, IsRepresentable.mk', IsRepresentable.iff_exists_isRepresentedBy, instIsRepresentableObjOppositeTypeYoneda, RepresentableBy.isRepresentable, instIsRepresentableCompOppositeUliftFunctor, CategoryTheory.isRepresentable_of_natIso, CategoryTheory.isRepresentable_hasClassifier_iff, isRepresentable_comp_uliftFunctor_iff
RepresentableBy 📖	CompData	7 math math: representableByUliftFunctorEquiv_symm_apply_homEquiv, IsRepresentable.has_representation, RepresentableBy.equivOfIsoObj_symm_apply, RepresentableBy.equivOfIsoObj_apply, RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv, representableByUliftFunctorEquiv_apply_homEquiv, RepresentableBy.equivUliftYonedaIso_apply
coreprW 📖	CompOp	1 math math: coreprW_hom_app
coreprX 📖	CompOp	2 math math: uliftCoyonedaCoreprXIso_hom_app, coreprW_hom_app
corepresentableBy 📖	CompOp	—
corepresentableByEquiv 📖	CompOp	—
corepresentableByUliftFunctorEquiv 📖	CompOp	2 math math: corepresentableByUliftFunctorEquiv_apply_homEquiv, corepresentableByUliftFunctorEquiv_symm_apply_homEquiv
coreprx 📖	CompOp	2 math math: uliftCoyonedaCoreprXIso_hom_app, coreprW_hom_app
reprW 📖	CompOp	1 math math: reprW_hom_app
reprX 📖	CompOp	3 math math: IsRepresentedBy.of_isRepresentable, uliftYonedaReprXIso_hom_app, reprW_hom_app
representableBy 📖	CompOp	—
representableByEquiv 📖	CompOp	—
representableByUliftFunctorEquiv 📖	CompOp	2 math math: representableByUliftFunctorEquiv_symm_apply_homEquiv, representableByUliftFunctorEquiv_apply_homEquiv
reprx 📖	CompOp	3 math math: IsRepresentedBy.of_isRepresentable, uliftYonedaReprXIso_hom_app, reprW_hom_app
sectionsEquivHom 📖	CompOp	3 math math: sectionsEquivHom_naturality, sectionsEquivHom_naturality_symm, sectionsEquivHom_apply_app
uliftCoyonedaCoreprXIso 📖	CompOp	1 math math: uliftCoyonedaCoreprXIso_hom_app
uliftYonedaReprXIso 📖	CompOp	1 math math: uliftYonedaReprXIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreprW_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category CategoryTheory.coyoneda Opposite.op coreprX CategoryTheory.Iso.hom coreprW map coreprx	—	CorepresentableBy.homEquiv_eq
corepresentableByUliftFunctorEquiv_apply_homEquiv 📖	mathematical	—	CorepresentableBy.homEquiv DFunLike.coe Equiv CorepresentableBy comp CategoryTheory.types CategoryTheory.uliftFunctor EquivLike.toFunLike Equiv.instEquivLike corepresentableByUliftFunctorEquiv Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Equiv.ulift	—	—
corepresentableByUliftFunctorEquiv_symm_apply_homEquiv 📖	mathematical	—	CorepresentableBy.homEquiv comp CategoryTheory.types CategoryTheory.uliftFunctor DFunLike.coe Equiv CorepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm corepresentableByUliftFunctorEquiv Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Equiv.ulift	—	—
instIsCorepresentableCompUliftFunctor 📖	mathematical	—	IsCorepresentable comp CategoryTheory.types CategoryTheory.uliftFunctor	—	isCorepresentable_comp_uliftFunctor_iff
instIsCorepresentableObjOppositeTypeCoyoneda 📖	mathematical	—	IsCorepresentable obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types category CategoryTheory.coyoneda	—	IsCorepresentable.mk'
instIsRepresentableCompOppositeUliftFunctor 📖	mathematical	—	IsRepresentable comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftFunctor	—	isRepresentable_comp_uliftFunctor_iff
instIsRepresentableObjOppositeTypeYoneda 📖	mathematical	—	IsRepresentable obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types category CategoryTheory.yoneda	—	IsRepresentable.mk'
isCorepresentable_comp_uliftFunctor_iff 📖	mathematical	—	IsCorepresentable comp CategoryTheory.types CategoryTheory.uliftFunctor	—	—
isRepresentable_comp_uliftFunctor_iff 📖	mathematical	—	IsRepresentable comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftFunctor	—	—
reprW_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types obj CategoryTheory.Functor category CategoryTheory.yoneda reprX CategoryTheory.Iso.hom reprW map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct reprx	—	RepresentableBy.homEquiv_eq
representableByUliftFunctorEquiv_apply_homEquiv 📖	mathematical	—	RepresentableBy.homEquiv DFunLike.coe Equiv RepresentableBy comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftFunctor EquivLike.toFunLike Equiv.instEquivLike representableByUliftFunctorEquiv Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Opposite.op Equiv.ulift	—	—
representableByUliftFunctorEquiv_symm_apply_homEquiv 📖	mathematical	—	RepresentableBy.homEquiv comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.uliftFunctor DFunLike.coe Equiv RepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm representableByUliftFunctorEquiv Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj Opposite.op Equiv.ulift	—	—
sectionsEquivHom_apply_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types obj CategoryTheory.Functor category const DFunLike.coe Equiv Set.Elem sections Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike sectionsEquivHom Set Set.instMembership	—	—
sectionsEquivHom_naturality 📖	mathematical	—	DFunLike.coe Equiv Set.Elem sections Quiver.Hom CategoryTheory.Functor CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category obj const EquivLike.toFunLike Equiv.instEquivLike sectionsEquivHom map sectionsFunctor CategoryTheory.CategoryStruct.comp	—	—
sectionsEquivHom_naturality_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category obj const Set.Elem sections EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sectionsEquivHom CategoryTheory.CategoryStruct.comp map sectionsFunctor	—	—
uliftCoyonedaCoreprXIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor category CategoryTheory.uliftCoyoneda Opposite.op coreprX CategoryTheory.Iso.hom uliftCoyonedaCoreprXIso map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct coreprx	—	CorepresentableBy.homEquiv_eq
uliftYonedaReprXIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types obj CategoryTheory.Functor category CategoryTheory.uliftYoneda reprX CategoryTheory.Iso.hom uliftYonedaReprXIso map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom reprx	—	RepresentableBy.homEquiv_eq

CategoryTheory.Functor.CorepresentableBy

Definitions

Name	Category	Theorems
coyoneda 📖	CompOp	1 math math: coyoneda_homEquiv
equivOfIsoObj 📖	CompOp	2 math math: equivOfIsoObj_symm_apply, equivOfIsoObj_apply
equivUliftCoyonedaIso 📖	CompOp	2 math math: equivUliftCoyonedaIso_symm_apply_homEquiv, equivUliftCoyonedaIso_apply
homEquiv 📖	CompOp	24 math math: HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, uniqueUpToIso_inv, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂_homEquiv, ofIsoObj_homEquiv, homEquiv_eq, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂'_homEquiv, CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_apply_homEquiv, CategoryTheory.Adjunction.corepresentableBy_homEquiv, CategoryTheory.Functor.Elements.initialOfCorepresentableBy_snd, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply, CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_symm_apply_homEquiv, equivUliftCoyonedaIso_symm_apply_homEquiv, equivUliftCoyonedaIso_apply, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app, homEquiv_comp, uniqueUpToIso_hom, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, ext_iff, homEquiv_symm_comp, coyoneda_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv
isoCoreprX 📖	CompOp	—
ofIso 📖	CompOp	—
ofIsoObj 📖	CompOp	3 math math: equivOfIsoObj_symm_apply, equivOfIsoObj_apply, ofIsoObj_homEquiv
toIso 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_inv, uniqueUpToIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyoneda_homEquiv 📖	mathematical	—	homEquiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.unop coyoneda Equiv.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
equivOfIsoObj_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.CorepresentableBy EquivLike.toFunLike Equiv.instEquivLike equivOfIsoObj ofIsoObj	—	—
equivOfIsoObj_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.CorepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivOfIsoObj ofIsoObj CategoryTheory.Iso.symm	—	—
equivUliftCoyonedaIso_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.CorepresentableBy CategoryTheory.Iso CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.uliftCoyoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike equivUliftCoyonedaIso CategoryTheory.NatIso.ofComponents equivEquivIso Equiv.trans CategoryTheory.yoneda Equiv.ulift homEquiv	—	—
equivUliftCoyonedaIso_symm_apply_homEquiv 📖	mathematical	—	homEquiv DFunLike.coe Equiv CategoryTheory.Iso CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.uliftCoyoneda Opposite.op CategoryTheory.Functor.CorepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivUliftCoyonedaIso Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Equiv.ulift equivEquivIso CategoryTheory.Iso.app	—	—
ext 📖	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.id	—	—	homEquiv_eq Equiv.ext
ext_iff 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.id	—	ext
homEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	—
homEquiv_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp homEquiv_comp
homEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv CategoryTheory.Functor.obj CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.Functor.map	—	Equiv.injective homEquiv_comp Equiv.apply_symm_apply
isCorepresentable 📖	mathematical	—	CategoryTheory.Functor.IsCorepresentable	—	—
ofIsoObj_homEquiv 📖	mathematical	—	homEquiv ofIsoObj Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Iso.homFromEquiv	—	—
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.FullyFaithful.preimage Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda CategoryTheory.Coyoneda.fullyFaithful CategoryTheory.Functor.obj CategoryTheory.NatIso.ofComponents Quiver.Hom DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.trans homEquiv	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.FullyFaithful.preimage Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.coyoneda CategoryTheory.Coyoneda.fullyFaithful CategoryTheory.Functor.obj CategoryTheory.NatIso.ofComponents Quiver.Hom DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.trans homEquiv	—	—

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
compUliftCoyonedaCompWhiskeringLeft 📖	CompOp	2 math math: compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down, compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down
compUliftYonedaCompWhiskeringLeft 📖	CompOp	2 math math: compUliftYonedaCompWhiskeringLeft_inv_app_app_down, compUliftYonedaCompWhiskeringLeft_hom_app_app_down
compYonedaCompWhiskeringLeft 📖	CompOp	—
compYonedaCompWhiskeringLeftMaxRight 📖	CompOp	2 math math: compYonedaCompWhiskeringLeftMaxRight_inv_app_app, compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down
homNatIso 📖	CompOp	2 math math: homNatIso_inv_app_down, homNatIso_hom_app_down
homNatIso' 📖	CompOp	2 math math: homNatIso'_hom_app_down, homNatIso'_inv_app_down
homNatIsoMaxRight 📖	CompOp	2 math math: homNatIsoMaxRight_inv_app, homNatIsoMaxRight_hom_app_down

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op Opposite.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.uliftCoyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom compUliftCoyonedaCompWhiskeringLeft preimage Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op Opposite.unop CategoryTheory.NatTrans.app CategoryTheory.uliftCoyoneda CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.inv compUliftCoyonedaCompWhiskeringLeft CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
compUliftYonedaCompWhiskeringLeft_hom_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.uliftYoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.hom compUliftYonedaCompWhiskeringLeft preimage Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
compUliftYonedaCompWhiskeringLeft_inv_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.op CategoryTheory.NatTrans.app CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.inv compUliftYonedaCompWhiskeringLeft CategoryTheory.Functor.map Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.uliftYoneda CategoryTheory.Iso.hom compYonedaCompWhiskeringLeftMaxRight preimage Opposite.unop	—	—
compYonedaCompWhiskeringLeftMaxRight_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.yoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.inv compYonedaCompWhiskeringLeftMaxRight CategoryTheory.Functor.map Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
homNatIso'_hom_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.uliftCoyoneda CategoryTheory.Iso.hom homNatIso' preimage Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
homNatIso'_inv_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op CategoryTheory.NatTrans.app CategoryTheory.uliftCoyoneda CategoryTheory.Functor.comp CategoryTheory.Iso.inv homNatIso' CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
homNatIsoMaxRight_hom_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.uliftYoneda CategoryTheory.Iso.hom homNatIsoMaxRight preimage Opposite.unop	—	—
homNatIsoMaxRight_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.yoneda CategoryTheory.Iso.inv homNatIsoMaxRight CategoryTheory.Functor.map Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
homNatIso_hom_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.uliftYoneda CategoryTheory.Iso.hom homNatIso preimage Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
homNatIso_inv_app_down 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.op CategoryTheory.NatTrans.app CategoryTheory.uliftYoneda CategoryTheory.Functor.comp CategoryTheory.Iso.inv homNatIso CategoryTheory.Functor.map Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Functor.IsCorepresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_corepresentation 📖	mathematical	—	CategoryTheory.Functor.CorepresentableBy	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.IsCorepresentable	—	CategoryTheory.Functor.CorepresentableBy.isCorepresentable

CategoryTheory.Functor.IsRepresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_representation 📖	mathematical	—	CategoryTheory.Functor.RepresentableBy	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.IsRepresentable	—	CategoryTheory.Functor.RepresentableBy.isRepresentable

CategoryTheory.Functor.RepresentableBy

Definitions

Name	Category	Theorems
equivOfIsoObj 📖	CompOp	2 math math: equivOfIsoObj_symm_apply, equivOfIsoObj_apply
equivUliftYonedaIso 📖	CompOp	2 math math: equivUliftYonedaIso_symm_apply_homEquiv, equivUliftYonedaIso_apply
homEquiv 📖	CompOp	27 math math: CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, homEquiv_eq, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, CategoryTheory.MonObj.ofRepresentableBy_one, coyoneda_homEquiv, CategoryTheory.Functor.representableByUliftFunctorEquiv_symm_apply_homEquiv, comp_homEquiv_symm, CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq, equivUliftYonedaIso_symm_apply_homEquiv, homEquiv_comp, isRepresentedBy, homEquiv_unop_comp, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, uniqueUpToIso_hom, CategoryTheory.MonObj.ofRepresentableBy_mul, ext_iff, CategoryTheory.Functor.representableByUliftFunctorEquiv_apply_homEquiv, uniqueUpToIso_inv, equivUliftYonedaIso_apply, CategoryTheory.Adjunction.representableBy_homEquiv, CategoryTheory.Functor.Elements.initialOfRepresentableBy_snd, ofIsoObj_homEquiv, CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy, CategoryTheory.Functor.IsRepresentedBy.representableBy_homEquiv_apply
isoReprX 📖	CompOp	—
ofIso 📖	CompOp	—
ofIsoObj 📖	CompOp	3 math math: equivOfIsoObj_symm_apply, equivOfIsoObj_apply, ofIsoObj_homEquiv
toIso 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_hom, uniqueUpToIso_inv
yoneda 📖	CompOp	1 math math: coyoneda_homEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_homEquiv_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.Functor.map Quiver.Hom.op	—	Equiv.injective homEquiv_comp Equiv.apply_symm_apply
coyoneda_homEquiv 📖	mathematical	—	homEquiv CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda yoneda Equiv.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
equivOfIsoObj_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.RepresentableBy EquivLike.toFunLike Equiv.instEquivLike equivOfIsoObj ofIsoObj	—	—
equivOfIsoObj_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.RepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivOfIsoObj ofIsoObj CategoryTheory.Iso.symm	—	—
equivUliftYonedaIso_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.RepresentableBy CategoryTheory.Iso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda EquivLike.toFunLike Equiv.instEquivLike equivUliftYonedaIso CategoryTheory.NatIso.ofComponents equivEquivIso Equiv.trans CategoryTheory.yoneda Equiv.ulift homEquiv Opposite.unop	—	—
equivUliftYonedaIso_symm_apply_homEquiv 📖	mathematical	—	homEquiv DFunLike.coe Equiv CategoryTheory.Iso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.uliftYoneda CategoryTheory.Functor.RepresentableBy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivUliftYonedaIso Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Equiv.ulift equivEquivIso CategoryTheory.Iso.app	—	—
ext 📖	—	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	—	—	homEquiv_eq Equiv.ext
ext_iff 📖	mathematical	—	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	—	ext
homEquiv_comp 📖	mathematical	—	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.comp CategoryTheory.Functor.map Quiver.Hom.op	—	—
homEquiv_eq 📖	mathematical	—	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.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id homEquiv_comp
homEquiv_unop_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Functor.map	—	homEquiv_comp
isRepresentable 📖	mathematical	—	CategoryTheory.Functor.IsRepresentable	—	—
ofIsoObj_homEquiv 📖	mathematical	—	homEquiv ofIsoObj Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Iso.homToEquiv	—	—
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso CategoryTheory.Functor.FullyFaithful.preimage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Yoneda.fullyFaithful CategoryTheory.Functor.obj CategoryTheory.NatIso.ofComponents Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv Equiv.trans	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso CategoryTheory.Functor.FullyFaithful.preimage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Yoneda.fullyFaithful CategoryTheory.Functor.obj CategoryTheory.NatIso.ofComponents Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv Equiv.trans	—	—

CategoryTheory.ULiftYoneda

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulFunctorOppositeTypeUliftYoneda 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullFunctorOppositeTypeUliftYoneda 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.Yoneda

Definitions

Name	Category	Theorems
ext 📖	CompOp	—
fullyFaithful 📖	CompOp	3 math math: CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom, CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv, fullyFaithful_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fullyFaithful_preimage 📖	mathematical	—	CategoryTheory.Functor.FullyFaithful.preimage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda fullyFaithful CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
isIso 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.isIso_of_fully_faithful yoneda_full yoneda_faithful
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op Opposite.unop	—	CategoryTheory.FunctorToTypes.naturality
obj_map_id 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
yoneda_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	CategoryTheory.Functor.FullyFaithful.faithful
yoneda_full 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	CategoryTheory.Functor.FullyFaithful.full

---

← Back to Index