Basic

📁 Source: Mathlib/CategoryTheory/Adjunction/Basic.lean

Statistics

Metric	Count
Definitions CoreHomEquiv, homEquiv, CoreHomEquivUnitCounit, counit, homEquiv, unit, CoreUnitCounit, counit, unit, adjunctionOfEquivLeft, adjunctionOfEquivRight, comp, compCoyonedaIso, compUliftCoyonedaIso, compYonedaIso, corepresentableBy, counit, equivHomsetLeftOfNatIso, equivHomsetRightOfNatIso, homEquiv, id, instInhabitedId, leftAdjointOfEquiv, mk', mkOfHomEquiv, mkOfUnitCounit, ofIsLeftAdjoint, ofIsRightAdjoint, ofNatIsoLeft, ofNatIsoRight, representableBy, rightAdjointOfEquiv, toEquivalence, unit, toAdjunction, IsLeftAdjoint, IsRightAdjoint, adjunction, leftAdjoint, rightAdjoint, «term_⊣_»	41
Theorems homEquiv_naturality_left, homEquiv_naturality_left_symm, homEquiv_naturality_right, homEquiv_naturality_right_symm, homEquiv_counit, homEquiv_unit, left_triangle, right_triangle, adjunctionOfEquivLeft_counit_app, adjunctionOfEquivLeft_unit_app, adjunctionOfEquivRight_counit_app, adjunctionOfEquivRight_unit_app, compCoyonedaIso_hom_app_app, compCoyonedaIso_inv_app_app, compUliftCoyonedaIso_hom_app_app_down, compUliftCoyonedaIso_inv_app_app_down, compYonedaIso_hom_app_app, compYonedaIso_inv_app_app, comp_counit, comp_counit_app, comp_counit_app_assoc, comp_homEquiv, comp_unit, comp_unit_app, comp_unit_app_assoc, corepresentableBy_homEquiv, counit_naturality, counit_naturality_assoc, eq_homEquiv_apply, eq_unit_comp_map_iff, equivHomsetLeftOfNatIso_apply, equivHomsetLeftOfNatIso_symm_apply, equivHomsetRightOfNatIso_apply, equivHomsetRightOfNatIso_symm_apply, ext, ext_iff, homEquiv_apply, homEquiv_apply_eq, homEquiv_counit, homEquiv_id, homEquiv_naturality_left, homEquiv_naturality_left_square, homEquiv_naturality_left_square_assoc, homEquiv_naturality_left_square_iff, homEquiv_naturality_left_symm, homEquiv_naturality_right, homEquiv_naturality_right_square, homEquiv_naturality_right_square_assoc, homEquiv_naturality_right_square_iff, homEquiv_naturality_right_symm, homEquiv_symm_apply, homEquiv_symm_id, homEquiv_unit, id_counit, id_unit, instIsLeftAdjointLeftAdjoint, instIsRightAdjointRightAdjoint, isLeftAdjoint, isRightAdjoint, leftAdjointOfEquiv_map, leftAdjointOfEquiv_obj, left_triangle, left_triangle_components, left_triangle_components_assoc, mk'_counit, mk'_homEquiv, mk'_unit, mkOfHomEquiv_counit_app, mkOfHomEquiv_homEquiv, mkOfHomEquiv_unit_app, mkOfUnitCounit_counit, mkOfUnitCounit_unit, representableBy_homEquiv, rightAdjointOfEquiv_map, rightAdjointOfEquiv_obj, right_triangle, right_triangle_components, right_triangle_components_assoc, toEquivalence_counitIso_hom_app, toEquivalence_counitIso_inv_app, toEquivalence_functor, toEquivalence_inverse, toEquivalence_unitIso_hom_app, toEquivalence_unitIso_inv_app, unit_comp_map_eq_iff, unit_naturality, unit_naturality_assoc, isLeftAdjoint_functor, isLeftAdjoint_inverse, isRightAdjoint_functor, isRightAdjoint_inverse, refl_toAdjunction, toAdjunction_counit, toAdjunction_unit, trans_toAdjunction, exists_rightAdjoint, exists_leftAdjoint, isEquivalence_of_isRightAdjoint, isLeftAdjoint_comp, isLeftAdjoint_of_isEquivalence, isLeftAdjoint_of_iso, isRightAdjoint_comp, isRightAdjoint_of_isEquivalence, isRightAdjoint_of_iso	104
Total	145

CategoryTheory

Definitions

Name	Category	Theorems
«term_⊣_» 📖	CompOp	—

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
CoreHomEquiv 📖	CompData	—
CoreHomEquivUnitCounit 📖	CompData	—
CoreUnitCounit 📖	CompData	—
adjunctionOfEquivLeft 📖	CompOp	2 math math: adjunctionOfEquivLeft_counit_app, adjunctionOfEquivLeft_unit_app
adjunctionOfEquivRight 📖	CompOp	2 math math: adjunctionOfEquivRight_counit_app, adjunctionOfEquivRight_unit_app
comp 📖	CompOp	32 math math: CategoryTheory.iterated_mateEquiv_conjugateEquiv, isMonoidal_comp, CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm, comp_homEquiv, toCat_comp_toCat, CategoryTheory.frobeniusMorphism_mate, conjugateEquiv_leftAdjointCompIso_inv, leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.conjugateEquiv_leftUnitor_hom, CategoryTheory.Bicategory.Adjunction.ofCat_comp, CategoryTheory.conjugateEquiv_whiskerRight, CategoryTheory.mateEquiv_hcomp, comp_counit, comp_counit_app, SheafOfModules.conjugateEquiv_pullbackComp_inv, rightOp_eq, CategoryTheory.conjugateEquiv_rightUnitor_hom, IsTriangulated.comp, CommShift.instComp, leftOp_eq, CategoryTheory.conjugateEquiv_associator_hom, comp_unit_app_assoc, AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_inv, CategoryTheory.conjugateEquiv_whiskerLeft, leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm, comp_unit, comp_counit_app_assoc, CategoryTheory.mateEquiv_square, CategoryTheory.Equivalence.trans_toAdjunction, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, comp_unit_app
compCoyonedaIso 📖	CompOp	2 math math: compCoyonedaIso_inv_app_app, compCoyonedaIso_hom_app_app
compUliftCoyonedaIso 📖	CompOp	2 math math: compUliftCoyonedaIso_hom_app_app_down, compUliftCoyonedaIso_inv_app_app_down
compYonedaIso 📖	CompOp	2 math math: compYonedaIso_hom_app_app, compYonedaIso_inv_app_app
corepresentableBy 📖	CompOp	1 math math: corepresentableBy_homEquiv
counit 📖	CompOp	278 math math: adjunctionOfEquivLeft_counit_app, Triple.isIso_unit_iff_isIso_counit, leftOp_unit, CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, CategoryTheory.mateEquiv_counit_symm, CategoryTheory.isIso_sheafificationAdjunction_counit, whiskerLeftLCounitIsoOfIsIsoUnit_hom_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, CategoryTheory.Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, CategoryTheory.equivEssImageOfReflective_unitIso, CategoryTheory.PullbackShift.adjunction_counit, AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, LeftAdjointCommShift.iso_hom_app_assoc, Rep.coindResAdjunction_counit_app, map_ε_comp_counit_app_unit_assoc, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, Rep.resCoindAdjunction_counit_app_hom_hom, derivedε_fac_app_assoc, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, instIsIsoFunctorCounitOfIsEquivalence_1, instIsIsoAppCounitOfFullOfFaithful, adjunctionOfEquivRight_counit_app, ofCat_counit, compCoyonedaIso_inv_app_app, LeftAdjointCommShift.iso_inv_app_assoc, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit, CondensedMod.isDiscrete_tfae, rightAdjointLaxMonoidal_μ, CondensedSet.instEpiTopCatAppCounitTopCatAdjunction, IsMonoidal.leftAdjoint_μ, CompHausLike.LocallyConstant.adjunction_counit, Rep.coinvariantsAdjunction_counit_app, CategoryTheory.instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction, CategoryTheory.Functor.reflective', LightCondMod.isDiscrete_tfae, CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, id_counit, CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app, compYonedaIso_hom_app_app, CategoryTheory.conjugateEquiv_symm_apply_app, CategoryTheory.OppositeShift.adjunction_unit, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.conjugateEquiv_apply_app, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left, instIsIsoAppCounitObjOfFaithfulOfFull, CategoryTheory.Over.postAdjunctionRight_counit_app, AlgebraicGeometry.Scheme.Modules.instIsIsoFunctorCounitRestrictAdjunction, Triple.adj₁_counit_app_rightToLeft_app, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair, mapCommMon_counit, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, mkOfHomEquiv_counit_app, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, CategoryTheory.Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, CategoryTheory.Pi.monoidalClosed_closed_adj_counit, CategoryTheory.Under.postAdjunctionRight_unit_app_right, Triple.mono_leftToRight_app_iff_mono_adj₁_counit_app, leftAdjointUniq_hom_app_counit_assoc, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f, CategoryTheory.Over.mapPullbackAdj_counit_app, derived_counit, Triple.whiskerRight_rightToLeft_assoc, CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app, compUliftCoyonedaIso_inv_app_app_down, CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app, instIsIsoFunctorCounitOfIsEquivalence, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, CategoryTheory.conjugateEquiv_counit_symm, CategoryTheory.evaluationAdjunctionRight_counit_app_app, CategoryTheory.Monad.comparison_obj_a, leftAdjointUniq_hom_counit, isIso_counit_of_iso, CategoryTheory.Monad.adj_counit, map_restrictFullyFaithful_counit_app, CategoryTheory.Over.forgetAdjStar_counit_app, leftAdjointUniq_hom_app_counit, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, toComonad_ε, isIso_counit_app_of_iso, toCat_counit_toNatTrans, Triple.leftToRight_app_obj, CategoryTheory.Functor.essImage.counit_isIso, shift_counit_app, map_restrictFullyFaithful_counit_app_assoc, Rep.indResAdjunction_counit_app_hom_hom, counit_naturality, AlgebraicGeometry.Scheme.kerAdjunction_counit_app, CommShift.commShift_counit, whiskerRight_counit_iso_of_L_fully_faithful, CategoryTheory.Monad.MonadicityInternal.unitCofork_π, mk'_counit, comp_counit, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, mapMon_counit, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_right, derived'_counit, Triple.rightToLeft_eq_counits, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, comp_counit_app, CategoryTheory.ObjectProperty.isColocal_adj_counit_app, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', leftAdjointCompIso_inv_app, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.Over.toOverSectionsAdj_counit_app, toMonad_μ, CategoryTheory.Comonad.adj_counit, unop_counit, CategoryTheory.Codiscrete.adj_counit_app, CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit, CategoryTheory.ExponentiableMorphism.ev_def, Rep.resIndAdjunction_counit_app, rightOp_counit, functorialityCounit_app_hom, AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, commShiftIso_inv_app_counit_app_assoc, CategoryTheory.mateEquiv_symm_apply, LeftAdjointCommShift.iso_inv_app, counit_epi_of_R_faithful, whiskerLeft_counit_iso_of_L_fully_faithful, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc, CategoryTheory.conjugateEquiv_counit, CategoryTheory.Grpd.freeForgetAdjunction_counit_app, CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair, CategoryTheory.ReflQuiv.adj_counit_app, TopologicalSpace.Opens.adjunction_counit_map_functor, op_unit, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', CommShift.compatibilityCounit_left, Triple.adj₁_counit_app_rightToLeft_app_assoc, CategoryTheory.plusPlusAdjunction_counit_app_val, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, TopologicalSpace.Opens.adjunction_counit_app_self, commShiftIso_hom_app_counit_app_shift_assoc, CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, rightAdjointUniq_hom_counit_assoc, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CategoryTheory.Equivalence.toAdjunction_counit, CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, Rep.invariantsAdjunction_counit_app_hom, map_η_comp_η_assoc, RightAdjointCommShift.iso_hom_app_assoc, CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit_assoc, inv_counit_map, leftOp_counit, Triple.epi_rightToLeft_app_iff, rightAdjointUniq_hom_counit, CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit, CondensedSet.isDiscrete_tfae, leftAdjointUniq_hom_counit_assoc, Triple.leftToRight_eq_counits, counit_isIso_of_R_fully_faithful, CategoryTheory.LiftLeftAdjoint.instIsReflexivePairMapAppCounitOtherMap, rightOp_unit, CategoryTheory.Over.postAdjunctionRight_unit_app, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_counit_app_left, map_μ_comp_counit_app_tensor, CategoryTheory.Monad.MonadicityInternal.unitCofork_pt, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, rightAdjointUniq_hom_app_counit, localization_counit_app, CommShift.compatibilityUnit_right, Triple.map_rightToLeft_app, eq_unit_comp_map_iff, CategoryTheory.SimplicialObject.Truncated.cosk_reflective, left_triangle, homEquiv_symm_id, mkOfUnitCounit_counit, CategoryTheory.Monad.comparison_map_f, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, Triple.whiskerRight_rightToLeft, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit, RightAdjointCommShift.iso_inv_app, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, rightAdjointUniq_hom_app_counit_assoc, TopCat.adj₂_counit, Triple.whiskerLeft_leftToRight_assoc, CategoryTheory.Under.mapPushoutAdj_counit_app, Triple.map_adj₂_counit_app_leftToRight_app, Triple.map_rightToLeft_app_assoc, CategoryTheory.counit_obj_eq_map_counit, whiskerLeftRUnitIsoOfIsIsoCounit_hom_app, RightAdjointCommShift.iso_inv_app_assoc, functorCategory_inverseImage_isomorphisms_counit, CategoryTheory.sheafificationAdjunction_counit_app_val, right_triangle_components, CategoryTheory.Under.postAdjunctionLeft_counit_app, CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_counit_app, SSet.Truncated.cosk_reflective, homEquiv_counit, counit_naturality_assoc, CategoryTheory.constantSheafAdj_counit_w, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit, LeftAdjointCommShift.iso_hom_app, LightCondSet.isDiscrete_tfae, right_triangle, Triple.epi_rightToLeft_app_iff_epi_map_adj₂_counit_app, CategoryTheory.conjugateEquiv_adjunction_id, CategoryTheory.Functor.ranAdjunction_counit, CategoryTheory.OppositeShift.adjunction_counit, right_triangle_components_assoc, TopCat.adj₁_counit, CategoryTheory.Monad.MonadicityInternal.main_pair_G_split, leftAdjointCompIso_hom_app, CategoryTheory.Monad.MonadicityInternal.counitCofork_pt, CategoryTheory.Under.postAdjunctionRight_counit_app_right, whiskerRight_counit_app_app, CategoryTheory.Monad.MonadicityInternal.counitCofork_ι_app, CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive, IsMonoidal.instIsMonoidalCounit, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, homEquiv_symm_rightAdjointUniq_hom_app, commShiftIso_inv_app_counit_app, Triple.leftToRight_app_obj_assoc, CategoryTheory.sheafification_reflective, comp_counit_app_assoc, CategoryTheory.constantPresheafAdj_counit_app_app, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit, AlgebraicGeometry.Scheme.ofRestrict_app, left_triangle_components_assoc, CategoryTheory.mateEquiv_counit, RightAdjointCommShift.iso_hom_app, CategoryTheory.constantSheafAdj_counit_app, map_η_comp_η, op_counit, CategoryTheory.instIsReflexivePairMapAppCounitObj, leftAdjointIdIso_hom_app, instIsIsoMapAppCounitOfFaithfulOfFull, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, map_ε_comp_counit_app_unit, CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit_assoc, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app, CategoryTheory.Functor.lanAdjunction_counit_app, unit_comp_map_eq_iff, CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff, isIso_counit_app_iff_mem_essImage, unop_unit, commShiftIso_hom_app_counit_app_shift, CategoryTheory.Limits.coneOfAdj_π, CategoryTheory.nerveAdjunction.isIso_counit, Localization.η_app, CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app_assoc, left_triangle_components, CategoryTheory.ihom.ihom_adjunction_counit, Triple.whiskerLeft_leftToRight, derivedε_fac_app, CategoryTheory.forgetAdjToOver_counit_app, map_μ_comp_counit_app_tensor_assoc, homEquiv_symm_apply, counit_isSplitMono_of_R_full, inv_map_unit, mapCommGrp_counit, functorialityCounit'_app_hom, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, shift_counit_app_assoc, mapGrp_counit, Triple.mono_leftToRight_app_iff, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit_assoc, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, whiskerLeft_counit_app_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit, leftAdjointCompNatTrans_app, CategoryTheory.evaluationAdjunctionLeft_counit_app, CategoryTheory.mateEquiv_apply
equivHomsetLeftOfNatIso 📖	CompOp	3 math math: CategoryTheory.Over.postAdjunctionLeft_unit_app_left, equivHomsetLeftOfNatIso_symm_apply, equivHomsetLeftOfNatIso_apply
equivHomsetRightOfNatIso 📖	CompOp	3 math math: equivHomsetRightOfNatIso_apply, CategoryTheory.Under.postAdjunctionRight_counit_app_right, equivHomsetRightOfNatIso_symm_apply
homEquiv 📖	CompOp	120 math math: Rep.invariantsAdjunction_homEquiv_symm_apply_hom, CategoryTheory.ReflQuiv.adj_homEquiv, LightCondensed.ihomPoints_apply, CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq, homEquiv_naturality_left_square, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, rightAdjointLaxMonoidal_μ, comp_homEquiv, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str, CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str, ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, CategoryTheory.CommSq.instHasLift, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, eq_homEquiv_apply, Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, homEquiv_unit, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.CartesianClosed.homEquiv_apply_eq, compPreadditiveYonedaIso_inv_app_app_apply, Rep.homEquiv_def, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, homAddEquiv_sub, restrictFullyFaithful_homEquiv_apply, CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, Rep.resIndAdjunction_homEquiv_symm_apply, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, CategoryTheory.Quiv.adj_homEquiv, ModuleCat.adj_homEquiv, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', corepresentableBy_homEquiv, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f, instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms, Rep.resIndAdjunction_homEquiv_apply, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, homAddEquiv_add, Rep.coindResAdjunction_homEquiv_apply, CategoryTheory.Functor.isIso_ranAdjunction_homEquiv_iff, CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app, CategoryTheory.CommSq.right_adjoint_hasLift_iff, homEquiv_naturality_right_square_iff, CategoryTheory.Limits.isLimitConeOfAdj_lift, compPreadditiveYonedaIso_hom_app_app_apply, homAddEquiv_symm_zero, ModuleCat.homEquiv_extendScalarsComp, CategoryTheory.CommSq.left_adjoint_hasLift_iff, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.Functor.isIso_lanAdjunction_homEquiv_symm_iff, CategoryTheory.CommSq.right_adjoint, homAddEquiv_symm_neg, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, CategoryTheory.forgetAdjToOver.homEquiv_symm, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, Rep.coindResAdjunction_homEquiv_symm_apply, homAddEquiv_zero, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, CategoryTheory.CommSq.left_adjoint, CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq, LightCondensed.ihomPoints_symm_apply, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, homAddEquiv_symm_apply, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, homAddEquiv_symm_add, homAddEquiv_neg, homEquiv_symm_id, homEquiv_naturality_left_square_iff, homEquiv_naturality_right_symm, Rep.invariantsAdjunction_homEquiv_apply_hom, homEquiv_apply, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, CategoryTheory.CommSq.instHasLift_1, CategoryTheory.MonoidalClosed.homEquiv_apply_eq, CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f, homEquiv_naturality_left_symm, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str, rightAdjointLaxMonoidal_ε, homEquiv_counit, CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, homEquiv_naturality_right_square, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, representableBy_homEquiv, CategoryTheory.ParametrizedAdjunction.homEquiv_eq, CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str, homAddEquiv_apply, homEquiv_naturality_right_square_assoc, mk'_homEquiv, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, homEquiv_symm_rightAdjointUniq_hom_app, homAddEquiv_symm_sub, CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm, homEquiv_apply_eq, Rep.coinvariantsAdjunction_homEquiv_apply_hom, CategoryTheory.TwoSquare.lanBaseChange_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, PresheafOfModules.freeAdjunction_homEquiv, homEquiv_leftAdjointUniq_hom_app, homEquiv_naturality_right, CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq, ModuleCat.homEquiv_extendScalarsId, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, homEquiv_id, homEquiv_naturality_left, CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, homEquiv_symm_apply, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, homEquiv_naturality_left_square_assoc, mkOfHomEquiv_homEquiv
id 📖	CompOp	14 math math: IsTriangulated.id, id_counit, CommShift.instId, CategoryTheory.conjugateEquiv_leftUnitor_hom, conjugateEquiv_leftAdjointIdIso_hom, CategoryTheory.Bicategory.Adjunction.ofCat_id, instIsMonoidalId, CategoryTheory.conjugateEquiv_rightUnitor_hom, CategoryTheory.Equivalence.refl_toAdjunction, AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackId_hom, id_unit, CategoryTheory.conjugateEquiv_adjunction_id_symm, SheafOfModules.conjugateEquiv_pullbackId_hom, CategoryTheory.conjugateEquiv_adjunction_id
instInhabitedId 📖	CompOp	—
leftAdjointOfEquiv 📖	CompOp	5 math math: adjunctionOfEquivLeft_counit_app, leftAdjointOfEquiv_obj, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, leftAdjointOfEquiv_map, adjunctionOfEquivLeft_unit_app
mk' 📖	CompOp	3 math math: mk'_counit, mk'_homEquiv, mk'_unit
mkOfHomEquiv 📖	CompOp	3 math math: mkOfHomEquiv_counit_app, mkOfHomEquiv_unit_app, mkOfHomEquiv_homEquiv
mkOfUnitCounit 📖	CompOp	2 math math: mkOfUnitCounit_unit, mkOfUnitCounit_counit
ofIsLeftAdjoint 📖	CompOp	—
ofIsRightAdjoint 📖	CompOp	—
ofNatIsoLeft 📖	CompOp	—
ofNatIsoRight 📖	CompOp	—
representableBy 📖	CompOp	1 math math: representableBy_homEquiv
rightAdjointOfEquiv 📖	CompOp	5 math math: adjunctionOfEquivRight_counit_app, adjunctionOfEquivRight_unit_app, rightAdjointOfEquiv_obj, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit, rightAdjointOfEquiv_map
toEquivalence 📖	CompOp	8 math math: toEquivalence_inverse, toEquivalence_counitIso_hom_app, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, toEquivalence_unitIso_hom_app, toEquivalence_counitIso_inv_app, toEquivalence_unitIso_inv_app, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, toEquivalence_functor
unit 📖	CompOp	271 math math: compUliftCoyonedaIso_hom_app_app_down, Triple.isIso_unit_iff_isIso_counit, leftOp_unit, whiskerLeftLCounitIsoOfIsIsoUnit_inv_app, Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_app, Localization.ε_app, unit_app_tensor_comp_map_δ_assoc, LeftAdjointCommShift.iso_hom_app_assoc, TopCat.Presheaf.germ_stalkPullbackHom, CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app, instIsIsoAppUnitObjOfFaithfulOfFull, mapMon_unit, derived'_unit, CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.Comonad.ComonadicityInternal.unitFork_pt, LeftAdjointCommShift.iso_inv_app_assoc, IsMonoidal.leftAdjoint_μ, SSet.Truncated.sk_coreflective, CategoryTheory.Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom_assoc, instIsIsoFunctorUnitOfIsEquivalence, CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_unit_app, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_left, Triple.rightToLeft_eq_units, CategoryTheory.evaluationAdjunctionLeft_unit_app_app, Rep.resCoindAdjunction_unit_app_hom_hom, CategoryTheory.ReflQuiv.adj_unit_app, localization_unit_app, CategoryTheory.conjugateEquiv_symm_apply_app, CategoryTheory.OppositeShift.adjunction_unit, CategoryTheory.conjugateEquiv_apply_app, ε_comp_map_ε_assoc, mapCommMon_unit, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.PullbackShift.adjunction_unit, homEquiv_unit, CategoryTheory.Under.postAdjunctionRight_unit_app_right, mapCommGrp_unit, unit_mono_of_L_faithful, AlgebraicGeometry.Scheme.kerAdjunction_unit_app, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair, CategoryTheory.Localization.LeftBousfield.W_adj_unit_app, Triple.whiskerRight_rightToLeft_assoc, unit_app_shift_commShiftIso_inv_app, unit_rightAdjointUniq_hom, Rep.invariantsAdjunction_unit_app, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app, mapGrp_unit, map_restrictFullyFaithful_unit_app_assoc, mkOfUnitCounit_unit, unit_app_unit_comp_map_η, toComonad_δ, CategoryTheory.GrothendieckTopology.W_adj_unit_app, CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι, IsMonoidal.leftAdjoint_ε, CategoryTheory.Under.mapPushoutAdj_unit_app, CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_unit_app_left, functorialityUnit_app_hom, CategoryTheory.Monad.adj_unit, Rep.coindResAdjunction_unit_app, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app, CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair, toMonad_η, Triple.leftToRight_app_obj, instIsIsoAppUnitOfFullOfFaithful, CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom, unit_rightAdjointUniq_hom_app, restrictFullyFaithful_homEquiv_apply, AlgebraicGeometry.ΓSpec.adjunction_unit_app, CategoryTheory.Over.mapPullbackAdj_unit_app, instIsIsoFunctorUnitOfIsEquivalence_1, CategoryTheory.Functor.isIso_ranAdjunction_unit_app_iff, CategoryTheory.unit_conjugateEquiv_symm, CategoryTheory.unit_conjugateEquiv, isIso_unit_app_iff_mem_essImage, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, CategoryTheory.Over.toOverSectionsAdj_unit_app, mkOfHomEquiv_unit_app, leftAdjointCompIso_inv_app, IsMonoidal.instIsMonoidalUnit, derived_unit, CategoryTheory.forgetAdjToOver_unit_app, adjunctionOfEquivRight_unit_app, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, unop_counit, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, rightOp_counit, CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.Functor.essImage.unit_isIso, CategoryTheory.mateEquiv_symm_apply, CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app_assoc, LeftAdjointCommShift.iso_inv_app, ε_comp_map_ε, CategoryTheory.ExponentiableMorphism.coev_def, unit_isIso_of_L_fully_faithful, CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage, unit_app_shift_commShiftIso_inv_app_assoc, unit_isSplitEpi_of_L_full, op_unit, ModuleCat.homEquiv_extendScalarsComp, CommShift.compatibilityCounit_left, functorialityUnit'_app_hom, TopCat.Presheaf.pullback_obj_obj_ext_iff, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f, compYonedaIso_inv_app_app, CategoryTheory.Sheaf.adjunction_unit_app_val, CategoryTheory.Monoidal.Reflective.instIsIsoAppUnitObjIhom, shift_unit_app, RightAdjointCommShift.iso_hom_app_assoc, unit_app_commShiftIso_hom_app_assoc, inv_counit_map, leftOp_counit, CategoryTheory.unit_mateEquiv_symm, isIso_unit_of_iso, Triple.epi_rightToLeft_app_iff, CategoryTheory.Comonad.comparison_map_f, CategoryTheory.Functor.lanAdjunction_unit, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive, Triple.leftToRight_app_map_adj₁_unit_app_assoc, TopCat.Presheaf.germ_stalkPullbackHom_assoc, unit_leftAdjointUniq_hom_assoc, CategoryTheory.ihom.ihom_adjunction_unit, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map_assoc, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, rightOp_unit, CategoryTheory.Over.postAdjunctionRight_unit_app, CategoryTheory.unit_mateEquiv, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, CategoryTheory.sheafificationAdjunction_unit_app, unit_naturality, CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_app, compCoyonedaIso_hom_app_app, CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app, comp_unit_app_assoc, toCat_unit_toNatTrans, derivedη_fac_app, ext_iff, derivedη_fac_app_assoc, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit, CategoryTheory.Pi.monoidalClosed_closed_adj_unit, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, instIsIsoMapAppUnitOfFaithfulOfFull, CategoryTheory.plusPlusAdjunction_unit_app, CommShift.compatibilityUnit_right, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom, Triple.map_rightToLeft_app, eq_unit_comp_map_iff, functorCategory_inverseImage_isomorphisms_unit, Rep.indResAdjunction_unit_app_hom_hom, left_triangle, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, unit_leftAdjointUniq_hom_app_assoc, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CategoryTheory.Codiscrete.adj_unit_app, Triple.whiskerRight_rightToLeft, homEquiv_apply, RightAdjointCommShift.iso_inv_app, CategoryTheory.SimplicialObject.Truncated.sk_coreflective, Triple.whiskerLeft_leftToRight_assoc, Triple.map_rightToLeft_app_assoc, CategoryTheory.evaluationAdjunctionRight_unit_app, unit_app_tensor_comp_map_δ, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom, RightAdjointCommShift.iso_inv_app_assoc, right_triangle_components, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map, unit_app_commShiftIso_hom_app, CategoryTheory.Under.postAdjunctionLeft_counit_app, whiskerLeft_unit_app_app, unit_rightAdjointUniq_hom_assoc, isIso_unit_app_of_iso, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right, CategoryTheory.ObjectProperty.isLocal_adj_unit_app, Rep.resIndAdjunction_unit_app, CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, id_unit, Triple.leftToRight_app, CategoryTheory.conjugateEquiv_adjunction_id_symm, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, LeftAdjointCommShift.iso_hom_app, right_triangle, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc, PresheafOfModules.freeAdjunction_unit_app, map_restrictFullyFaithful_unit_app, CommShift.commShift_unit, ofCat_unit, TopCat.adj₂_unit, Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app, CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom, CategoryTheory.OppositeShift.adjunction_counit, TopCat.adj₁_unit, CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit, right_triangle_components_assoc, unit_leftAdjointUniq_hom, ModuleCat.extendRestrictScalarsAdj_unit_app_apply, comp_unit, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom, CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app, unit_app_unit_comp_map_η_assoc, Rep.coinvariantsAdjunction_unit_app_hom, leftAdjointCompIso_hom_app, CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.unitCompPartialBijectiveAux_symm_apply, CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso, Triple.rightToLeft_app_adj₂_unit_app, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair, CategoryTheory.Functor.coreflective', Triple.leftToRight_app_obj_assoc, AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, CategoryTheory.Grpd.freeForgetAdjunction_unit_app, CategoryTheory.equivEssImageOfReflective_counitIso, leftAdjointIdIso_inv_app, whiskerRight_unit_iso_of_R_fully_faithful, CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt, left_triangle_components_assoc, CategoryTheory.Over.forgetAdjStar_unit_app_left, whiskerLeftRUnitIsoOfIsIsoCounit_inv_app, RightAdjointCommShift.iso_hom_app, unit_rightAdjointUniq_hom_app_assoc, op_counit, CategoryTheory.Comonad.adj_unit, homEquiv_leftAdjointUniq_hom_app, whiskerRight_unit_app_app, CategoryTheory.Functor.ranAdjunction_unit_app, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app_assoc, CategoryTheory.Equivalence.toAdjunction_unit, unit_comp_map_eq_iff, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, shift_unit_app_assoc, CategoryTheory.Under.postAdjunctionLeft_unit_app, unop_unit, unit_leftAdjointUniq_hom_app, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_assoc, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, homEquiv_id, left_triangle_components, mk'_unit, whiskerLeft_unit_iso_of_R_fully_faithful, CategoryTheory.unit_obj_eq_map_unit, Triple.whiskerLeft_leftToRight, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, CategoryTheory.sheafComposeNatTrans_fac, inv_map_unit, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc, CompHausLike.LocallyConstant.adjunction_unit, Triple.leftToRight_app_map_adj₁_unit_app, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA, Triple.rightToLeft_app_adj₂_unit_app_assoc, CategoryTheory.Monoidal.Reflective.instIsIsoMapTensorHomAppUnit, unit_naturality_assoc, CategoryTheory.constantPresheafAdj_unit_app, Triple.mono_leftToRight_app_iff, comp_unit_app, adjunctionOfEquivLeft_unit_app, leftAdjointCompNatTrans_app, CategoryTheory.mateEquiv_apply, CategoryTheory.unitCompPartialBijective_symm_apply, CategoryTheory.LiftRightAdjoint.instIsCoreflexivePairMapAppUnitOtherMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjunctionOfEquivLeft_counit_app 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp leftAdjointOfEquiv CategoryTheory.Functor.id counit adjunctionOfEquivLeft Equiv.symm CategoryTheory.CategoryStruct.id	—	—
adjunctionOfEquivLeft_unit_app 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp leftAdjointOfEquiv unit adjunctionOfEquivLeft CategoryTheory.CategoryStruct.id	—	—
adjunctionOfEquivRight_counit_app 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp rightAdjointOfEquiv CategoryTheory.Functor.id counit adjunctionOfEquivRight Equiv.symm CategoryTheory.CategoryStruct.id	—	—
adjunctionOfEquivRight_unit_app 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp rightAdjointOfEquiv unit adjunctionOfEquivRight CategoryTheory.CategoryStruct.id	—	—
compCoyonedaIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom compCoyonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.id unit CategoryTheory.Functor.map	—	homEquiv_unit
compCoyonedaIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.inv compCoyonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.map CategoryTheory.Functor.id counit	—	homEquiv_counit
compUliftCoyonedaIso_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.op CategoryTheory.uliftCoyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom compUliftCoyonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.id unit CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	homEquiv_unit
compUliftCoyonedaIso_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.Functor.comp CategoryTheory.uliftCoyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.inv compUliftCoyonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.id counit	—	homEquiv_counit
compYonedaIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.hom compYonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.map CategoryTheory.Functor.id counit	—	homEquiv_counit
compYonedaIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.inv compYonedaIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.id unit CategoryTheory.Functor.map	—	homEquiv_unit
comp_counit 📖	mathematical	—	counit CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc
comp_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
comp_counit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit comp CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_counit_app
comp_homEquiv 📖	mathematical	—	homEquiv CategoryTheory.Functor.comp comp Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	mk'_homEquiv
comp_unit 📖	mathematical	—	unit CategoryTheory.Functor.comp comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.inv CategoryTheory.Functor.rightUnitor CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.associator CategoryTheory.Iso.hom	—	CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc
comp_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
comp_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit comp CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_unit_app
corepresentableBy_homEquiv 📖	mathematical	—	CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op corepresentableBy homEquiv	—	—
counit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit	—	CategoryTheory.NatTrans.naturality
counit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_naturality
eq_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv Equiv.symm	—	eq_unit_comp_map_iff
eq_unit_comp_map_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map counit	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality left_triangle_components_assoc unit_naturality_assoc right_triangle_components CategoryTheory.Category.comp_id
equivHomsetLeftOfNatIso_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equivHomsetLeftOfNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
equivHomsetLeftOfNatIso_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivHomsetLeftOfNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
equivHomsetRightOfNatIso_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike equivHomsetRightOfNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
equivHomsetRightOfNatIso_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivHomsetRightOfNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
ext 📖	—	unit	—	—	CategoryTheory.NatTrans.ext' Equiv.injective homEquiv_unit right_triangle_components
ext_iff 📖	mathematical	—	unit	—	ext
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit CategoryTheory.Functor.map	—	—
homEquiv_apply_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv Equiv.symm	—	unit_comp_map_eq_iff
homEquiv_counit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	homEquiv_symm_apply
homEquiv_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.id CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit	—	homEquiv_unit CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
homEquiv_naturality_left 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.eq_symm_apply homEquiv_naturality_left_symm Equiv.symm_apply_apply
homEquiv_naturality_left_square 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike homEquiv	—	homEquiv_naturality_left homEquiv_naturality_right
homEquiv_naturality_left_square_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike homEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homEquiv_naturality_left_square
homEquiv_naturality_left_square_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.Functor.map	—	Equiv.symm_apply_apply homEquiv_naturality_right_square homEquiv_naturality_left_square
homEquiv_naturality_left_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	homEquiv_counit CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
homEquiv_naturality_right 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	homEquiv_unit CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
homEquiv_naturality_right_square 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv	—	homEquiv_naturality_left_symm homEquiv_naturality_right_symm
homEquiv_naturality_right_square_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homEquiv_naturality_right_square
homEquiv_naturality_right_square_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv	—	Equiv.apply_symm_apply homEquiv_naturality_left_square homEquiv_naturality_right_square
homEquiv_naturality_right_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.symm_apply_eq homEquiv_naturality_right Equiv.apply_symm_apply
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	—
homEquiv_symm_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	homEquiv_counit CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
homEquiv_unit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit CategoryTheory.Functor.map	—	homEquiv_apply
id_counit 📖	mathematical	—	counit CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp	—	—
id_unit 📖	mathematical	—	unit CategoryTheory.Functor.id id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	—
instIsLeftAdjointLeftAdjoint 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Functor.leftAdjoint	—	isLeftAdjoint
instIsRightAdjointRightAdjoint 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Functor.rightAdjoint	—	isRightAdjoint
isLeftAdjoint 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint	—	—
isRightAdjoint 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint	—	—
leftAdjointOfEquiv_map 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	leftAdjointOfEquiv Equiv.symm CategoryTheory.CategoryStruct.id	—	—
leftAdjointOfEquiv_obj 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	leftAdjointOfEquiv	—	—
left_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight unit CategoryTheory.Functor.whiskerLeft counit CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' left_triangle_components
left_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app unit counit CategoryTheory.CategoryStruct.id	—	—
left_triangle_components_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit counit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' left_triangle_components
mk'_counit 📖	mathematical	—	counit mk' CoreHomEquivUnitCounit.counit	—	—
mk'_homEquiv 📖	mathematical	—	homEquiv mk' CoreHomEquivUnitCounit.homEquiv	—	Equiv.ext homEquiv_unit CoreHomEquivUnitCounit.homEquiv_unit mk'_unit
mk'_unit 📖	mathematical	—	unit mk' CoreHomEquivUnitCounit.unit	—	—
mkOfHomEquiv_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit mkOfHomEquiv DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CoreHomEquiv.homEquiv CategoryTheory.CategoryStruct.id	—	—
mkOfHomEquiv_homEquiv 📖	mathematical	—	homEquiv mkOfHomEquiv CoreHomEquiv.homEquiv	—	Equiv.ext homEquiv_unit CoreHomEquiv.homEquiv_naturality_right CategoryTheory.Category.id_comp
mkOfHomEquiv_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit mkOfHomEquiv DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CoreHomEquiv.homEquiv CategoryTheory.CategoryStruct.id	—	—
mkOfUnitCounit_counit 📖	mathematical	—	counit mkOfUnitCounit CoreUnitCounit.counit	—	—
mkOfUnitCounit_unit 📖	mathematical	—	unit mkOfUnitCounit CoreUnitCounit.unit	—	—
representableBy_homEquiv 📖	mathematical	—	CategoryTheory.Functor.RepresentableBy.homEquiv CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda representableBy Equiv.symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homEquiv	—	—
rightAdjointOfEquiv_map 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	rightAdjointOfEquiv Equiv.symm CategoryTheory.CategoryStruct.id	—	—
rightAdjointOfEquiv_obj 📖	mathematical	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	rightAdjointOfEquiv	—	—
right_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft unit CategoryTheory.Functor.whiskerRight counit CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' right_triangle_components
right_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map counit CategoryTheory.CategoryStruct.id	—	—
right_triangle_components_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map counit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' right_triangle_components
toEquivalence_counitIso_hom_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso toEquivalence	—	—
toEquivalence_counitIso_inv_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso toEquivalence CategoryTheory.inv	—	—
toEquivalence_functor 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Equivalence.functor toEquivalence	—	—
toEquivalence_inverse 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Equivalence.inverse toEquivalence	—	—
toEquivalence_unitIso_hom_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso toEquivalence	—	—
toEquivalence_unitIso_inv_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit counit	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso toEquivalence CategoryTheory.inv	—	—
unit_comp_map_eq_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map counit	—	CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc counit_naturality left_triangle_components_assoc unit_naturality_assoc right_triangle_components CategoryTheory.Category.comp_id
unit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
unit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_naturality

CategoryTheory.Adjunction.CoreHomEquiv

Definitions

Name	Category	Theorems
homEquiv 📖	CompOp	8 math math: homEquiv_naturality_right, homEquiv_naturality_right_symm, CategoryTheory.Adjunction.mkOfHomEquiv_counit_app, CategoryTheory.Adjunction.mkOfHomEquiv_unit_app, homEquiv_naturality_left_symm, homEquiv_naturality_left, CategoryTheory.Over.coreHomEquivToOverSections_homEquiv, CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv_naturality_left 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.eq_symm_apply homEquiv_naturality_left_symm Equiv.symm_apply_apply
homEquiv_naturality_left_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	—
homEquiv_naturality_right 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	—
homEquiv_naturality_right_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.symm_apply_eq homEquiv_naturality_right Equiv.apply_symm_apply

CategoryTheory.Adjunction.CoreHomEquivUnitCounit

Definitions

Name	Category	Theorems
counit 📖	CompOp	2 math math: CategoryTheory.Adjunction.mk'_counit, homEquiv_counit
homEquiv 📖	CompOp	3 math math: homEquiv_unit, CategoryTheory.Adjunction.mk'_homEquiv, homEquiv_counit
unit 📖	CompOp	2 math math: homEquiv_unit, CategoryTheory.Adjunction.mk'_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv_counit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit	—	—
homEquiv_unit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map	—	—

CategoryTheory.Adjunction.CoreUnitCounit

Definitions

Name	Category	Theorems
counit 📖	CompOp	3 math math: right_triangle, CategoryTheory.Adjunction.mkOfUnitCounit_counit, left_triangle
unit 📖	CompOp	3 math math: CategoryTheory.Adjunction.mkOfUnitCounit_unit, right_triangle, left_triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight unit CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft counit CategoryTheory.NatTrans.id	—	—
right_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft unit CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight counit CategoryTheory.NatTrans.id	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
toAdjunction 📖	CompOp	16 math math: CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, inverseFunctor_map, symmEquivFunctor_map, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Adjunction.rightOp_eq, toAdjunction_counit, congrLeftFunctor_map, CategoryTheory.Adjunction.leftOp_eq, refl_toAdjunction, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, toAdjunction_unit, trans_toAdjunction, symmEquivInverse_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftAdjoint_functor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint functor	—	—
isLeftAdjoint_inverse 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint inverse	—	isLeftAdjoint_functor
isRightAdjoint_functor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint functor	—	isRightAdjoint_inverse
isRightAdjoint_inverse 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint inverse	—	—
refl_toAdjunction 📖	mathematical	—	toAdjunction refl CategoryTheory.Adjunction.id	—	—
toAdjunction_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit functor inverse toAdjunction counit	—	—
toAdjunction_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit functor inverse toAdjunction unit	—	—
trans_toAdjunction 📖	mathematical	—	toAdjunction trans CategoryTheory.Adjunction.comp functor inverse	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsLeftAdjoint 📖	CompData	62 math math: CategoryTheory.Equivalence.isLeftAdjoint_inverse, CategoryTheory.Over.instIsLeftAdjointForget, instIsLeftAdjointDiscreteTensorLeftCompIncl, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits, AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor, PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification, CategoryTheory.Under.pushoutIsLeftAdjoint, TopCat.Sheaf.instIsLeftAdjointPullback, SheafOfModules.instIsLeftAdjointPullback, isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top, CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow, CategoryTheory.ihom.instIsLeftAdjointTensorLeft, isLeftAdjoint_of_isEquivalence, Rep.instIsLeftAdjointActionModuleCatRes, AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointPullback, CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const, TopModuleCat.instIsLeftAdjointModuleCatWithModuleTopology, CategoryTheory.isLeftAdjoint_of_costructuredArrowTerminals, CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor, CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint, instIsLeftAdjointPresheafStalkFunctor, ModuleCat.instIsLeftAdjointRestrictScalars, AddCommMonCat.instIsLeftAdjointFree, TopModuleCat.instIsLeftAdjointTopCatFree, CategoryTheory.instIsLeftAdjointOfComonadicLeftAdjoint, CategoryTheory.Under.instIsLeftAdjointCostar, CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating, CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor, CategoryTheory.Under.isLeftAdjoint_post, CategoryTheory.instIsLeftAdjointReflector, IsRightAdjoint.op, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, CategoryTheory.Limits.instIsLeftAdjointFunctorColim, TopCat.instIsLeftAdjointForgetContinuousMapCarrier, CategoryTheory.evaluationIsLeftAdjoint, IsRightAdjoint.leftOp, CategoryTheory.Equivalence.isLeftAdjoint_functor, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, AddCommGrpCat.instIsLeftAdjointFree, isLeftAdjoint_comp, AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointRestrictFunctor, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify, CategoryTheory.isLeftAdjoint_square_lift, CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top, ModuleCat.instIsLeftAdjointExtendScalars, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra, CategoryTheory.instIsLeftAdjointTensorLeft, isLeftAdjoint_of_iso, Rep.instIsLeftAdjointIndFunctor, CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, CategoryTheory.Comonad.instIsLeftAdjointCoalgebraForget, CategoryTheory.instIsLeftAdjointOfCoreflective, CategoryTheory.isLeftAdjoint_triangle_lift_comonadic, CategoryTheory.isLeftAdjoint_square_lift_comonadic, CategoryTheory.Over.isLeftAdjoint_post, IsRightAdjoint.rightOp, CategoryTheory.isLeftAdjoint_triangle_lift
IsRightAdjoint 📖	CompData	75 math math: ModuleCat.instIsRightAdjointCoextendScalars, PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp, CategoryTheory.MonoOver.instIsRightAdjointOverForget, IsLeftAdjoint.op, CategoryTheory.isRightAdjoint_triangle_lift_monadic, CategoryTheory.Equivalence.isRightAdjoint_functor, Rep.instIsRightAdjointCoindFunctor, TopModuleCat.instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal, CategoryTheory.instIsRightAdjointOfReflective, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top, CategoryTheory.Limits.instIsRightAdjointFunctorLim, sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, CategoryTheory.OrthogonalReflection.isRightAdjoint_ι, MonCat.instIsRightAdjointForgetMonoidHomCarrier, Rep.instIsRightAdjointModuleCatInvariantsFunctor, CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier, CategoryTheory.Over.instIsRightAdjointStar, TopModuleCat.instIsRightAdjointModuleCatIndiscrete, CategoryTheory.instIsRightAdjointSheafΓ, isRightAdjoint_comp, ModuleCat.instIsRightAdjointRestrictScalars, IsLeftAdjoint.rightOp, CategoryTheory.isRightAdjoint_square_lift, CategoryTheory.Over.pullbackIsRightAdjoint, CategoryTheory.Over.isRightAdjoint_post, CategoryTheory.Under.instIsRightAdjointForget, CategoryTheory.isRightAdjointOfStructuredArrowInitials, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ, CategoryTheory.isRightAdjoint_square_lift_monadic, CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const, CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow, IsLeftAdjoint.leftOp, ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, CommMonCat.instIsRightAdjointForgetMonoidHomCarrier, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Monad.instIsRightAdjointAlgebraForget, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, CategoryTheory.isRightAdjoint_triangle_lift, AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier, instIsRightAdjointCommGrpCatCommMonCatUnits, CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating, TopCat.Sheaf.instIsRightAdjointPushforward, TopCat.instIsRightAdjointForgetContinuousMapCarrier, isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top, CommRingCat.instIsRightAdjointOppositeObjFunctorTypeYoneda, Rep.instIsRightAdjointActionModuleCatRes, SheafOfModules.instIsRightAdjointPushforward, CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition, isRightAdjoint_of_iso, CategoryTheory.evaluationIsRightAdjoint, CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint, CategoryTheory.sheafToPresheaf_isRightAdjoint, CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPushforward, PresheafOfModules.instIsRightAdjointPushforward, CategoryTheory.instIsRightAdjointCoreflector, CategoryTheory.Equivalence.isRightAdjoint_inverse, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, instIsRightAdjointGrpCatMonCatUnits, AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint, instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits, CategoryTheory.Under.isRightAdjoint_post, PresheafOfModules.instIsRightAdjointPushforwardIdFunctorOppositeRingCat, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, CommRingCat.instIsRightAdjointForgetRingHomCarrier, instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits, AlgCat.instIsRightAdjointForgetAlgHomCarrier, isRightAdjoint_of_isEquivalence, GrpCat.instIsRightAdjointForgetMonoidHomCarrier
adjunction 📖	CompOp	—
leftAdjoint 📖	CompOp	3 math math: CategoryTheory.HasSheafify.isLeftExact, CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf
rightAdjoint 📖	CompOp	1 math math: CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquivalence_of_isRightAdjoint 📖	mathematical	CategoryTheory.IsIso obj id comp leftAdjoint CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.Adjunction.ofIsRightAdjoint CategoryTheory.Adjunction.counit	IsEquivalence	—	CategoryTheory.Equivalence.isEquivalence_inverse
isLeftAdjoint_comp 📖	mathematical	—	IsLeftAdjoint comp	—	—
isLeftAdjoint_of_isEquivalence 📖	mathematical	—	IsLeftAdjoint	—	CategoryTheory.Equivalence.isLeftAdjoint_functor
isLeftAdjoint_of_iso 📖	mathematical	—	IsLeftAdjoint	—	—
isRightAdjoint_comp 📖	mathematical	—	IsRightAdjoint comp	—	—
isRightAdjoint_of_isEquivalence 📖	mathematical	—	IsRightAdjoint	—	CategoryTheory.Equivalence.isRightAdjoint_functor
isRightAdjoint_of_iso 📖	mathematical	—	IsRightAdjoint	—	—

CategoryTheory.Functor.IsLeftAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_rightAdjoint 📖	mathematical	—	CategoryTheory.Adjunction	—	—

CategoryTheory.Functor.IsRightAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_leftAdjoint 📖	mathematical	—	CategoryTheory.Adjunction	—	—

---

← Back to Index