| Name | Category | Theorems |
|---|
isoWhiskerLeft đ | CompOp | 75 mathmath: CategoryTheory.SingleFunctors.shiftIso_add, SheafOfModules.pushforward_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app, shiftIso_add', CategoryTheory.NatIso.op_rightUnitor, PresheafOfModules.pullback_comp_id, CategoryTheory.NatIso.unop_rightUnitor, CategoryTheory.SingleFunctors.shiftIso_add', CategoryTheory.Equivalence.congrFullSubcategory_counitIso, CategoryTheory.Pi.equivalenceOfEquiv_unitIso, isoWhiskerLeft_trans_isoWhiskerRight, CategoryTheory.NatIso.op_isoWhiskerLeft, isoWhiskerLeft_twice, CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app, triangleIso, CategoryTheory.Localization.Lifting.ofIsos_iso, CategoryTheory.shiftFunctorAdd'_assoc, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_fst_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app, isoWhiskerLeft_right, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, PresheafOfModules.pullback_assoc, isoWhiskerRight_left_assoc, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_snd_app, pentagonIso, CategoryTheory.Iso.coreAssociator, SheafOfModules.pullback_comp_id, shiftIso_add, commShiftPullback_iso_eq, CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, pentagonIso_assoc, isoWhiskerLeft_right_assoc, CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, CategoryTheory.shiftFunctorAdd'_add_zero, isoWhiskerLeft_inv, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_fst_app, CategoryTheory.NatIso.op_associator, isoWhiskerLeft_trans_isoWhiskerRight_assoc, triangleIso_assoc, CategoryTheory.shiftFunctorAdd_assoc, isoWhiskerLeft_trans_assoc, CategoryTheory.NatIso.unop_associator, CategoryTheory.Limits.Cones.functorialityEquivalence_inverse, CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_fst_app, CategoryTheory.SingleFunctors.shiftIso_zero, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, CategoryTheory.Equivalence.trans_counitIso, isoWhiskerLeft_refl, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, SheafOfModules.pullback_assoc, CategoryTheory.Iso.coreRightUnitor, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_fst_app, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, PresheafOfModules.pushforward_assoc, isoWhiskerRight_left, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, SheafOfModules.pushforward_comp_id, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_snd_app, ShiftSequence.shiftIso_add, CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_snd_app, isoWhiskerLeft_trans, CategoryTheory.Adjunction.leftAdjointCompIso_comp_id, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app, isoWhiskerLeft_hom, CategoryTheory.Equivalence.trans_unitIso, CategoryTheory.NatIso.unop_whiskerLeft, CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_snd_app, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, CategoryTheory.Iso.coreWhiskerLeft, PresheafOfModules.pushforward_comp_id, isoWhiskerLeft_symm
|
isoWhiskerRight đ | CompOp | 63 mathmath: CategoryTheory.SingleFunctors.shiftIso_add, SheafOfModules.pushforward_assoc, isoWhiskerRight_twice_assoc, PresheafOfModules.pullback_id_comp, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app, shiftIso_add', isoWhiskerRight_trans, CategoryTheory.shiftFunctorAdd'_zero_add, mapCoconePrecomposeEquivalenceFunctor_inv_hom, CategoryTheory.SingleFunctors.shiftIso_add', CategoryTheory.Pi.equivalenceOfEquiv_counitIso, isoWhiskerLeft_trans_isoWhiskerRight, triangleIso, CategoryTheory.shiftFunctorAdd'_assoc, CategoryTheory.Localization.Lifting.compRight_iso, CategoryTheory.Iso.coreLeftUnitor, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app, isoWhiskerLeft_right, CategoryTheory.NatIso.op_isoWhiskerRight, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, PresheafOfModules.pullback_assoc, isoWhiskerRight_left_assoc, isoWhiskerRight_twice, pentagonIso, shiftIso_zero, CategoryTheory.Iso.coreAssociator, shiftIso_add, commShiftPullback_iso_eq, pentagonIso_assoc, isoWhiskerLeft_right_assoc, mapCoconePrecomposeEquivalenceFunctor_hom_hom, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app, CategoryTheory.NatIso.unop_whiskerRight, SheafOfModules.pullback_id_comp, CategoryTheory.NatIso.op_associator, isoWhiskerLeft_trans_isoWhiskerRight_assoc, triangleIso_assoc, CategoryTheory.shiftFunctorAdd_assoc, CategoryTheory.NatIso.unop_leftUnitor, CategoryTheory.NatIso.unop_associator, mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.NatIso.op_leftUnitor, mapConePostcomposeEquivalenceFunctor_hom_hom, CategoryTheory.Equivalence.trans_counitIso, isoWhiskerRight_hom, SheafOfModules.pullback_assoc, isoWhiskerRight_symm, leftKanExtensionIsoFiberwiseColimit_hom_app, isoWhiskerRight_refl, PresheafOfModules.pushforward_assoc, isoWhiskerRight_left, CategoryTheory.Adjunction.leftAdjointCompIso_id_comp, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, ShiftSequence.shiftIso_add, isoWhiskerRight_trans_assoc, SheafOfModules.pushforward_id_comp, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app, CategoryTheory.Iso.coreWhiskerRight, CategoryTheory.Equivalence.trans_unitIso, isoWhiskerRight_inv, ShiftSequence.shiftIso_zero, PresheafOfModules.pushforward_id_comp, leftKanExtensionIsoFiberwiseColimit_inv_app
|
postcomposeâ đ | CompOp | 9 mathmath: postcomposeâ_obj_obj_obj_map, CategoryTheory.MonoidalCategory.externalProductBifunctor_map_app, CategoryTheory.MonoidalCategory.externalProductFlip_hom_app_app_app_app, CategoryTheory.Localization.Monoidal.liftingâCurriedTensorPost_iso, postcomposeâ_obj_map_app_app, postcomposeâ_obj_obj_obj_obj, postcomposeâ_obj_obj_map_app, postcomposeâ_map_app_app_app, CategoryTheory.MonoidalCategory.externalProductFlip_inv_app_app_app_app
|
postcomposeâ đ | CompOp | 6 mathmath: postcomposeâ_obj_obj_obj_map_app, postcomposeâ_obj_obj_map_app_app, postcomposeâ_obj_obj_obj_obj_obj, postcomposeâ_obj_obj_obj_obj_map, postcomposeâ_map_app_app_app_app, postcomposeâ_obj_map_app_app_app
|
whiskerLeft đ | CompOp | 263 mathmath: PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp, liftOfIsRightKanExtension_fac, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_associator, CategoryTheory.NatTrans.unop_whiskerLeft, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerRight, leftDerivedNatTrans_fac_assoc, CategoryTheory.Limits.Κ_colimitCompWhiskeringLeftIsoCompColimit_hom_assoc, isLimitConeOfIsRightKanExtension_lift, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, CategoryTheory.Sum.functorEquiv_functor_map, descOfIsLeftKanExtension_fac_assoc, isColimitCoconeOfIsLeftKanExtension_desc, CategoryTheory.Limits.Cocone.whisker_Κ, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit, CategoryTheory.Grothendieck.pre_comp_map_assoc, IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc, PresheafOfModules.limitPresheafOfModules_map, pentagon, CategoryTheory.NatTrans.unop_whiskerLeft_assoc, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc, CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom_assoc, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map_assoc, CategoryTheory.Limits.Cone.whisker_Ď, CategoryTheory.Adjunction.Triple.rightToLeft_eq_units, CategoryTheory.NatTrans.CommShift.shift_comm, CategoryTheory.Join.mapWhiskerLeft_whiskerLeft, AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_assoc, CategoryTheory.MonoidalCategory.DayFunctor.Ρ_comp_tensorDec, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl, Condensed.lanPresheafExt_inv, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom_naturality, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CategoryTheory.Presheaf.isLocallySurjective_whisker, rightDerived_fac_assoc, functorialityCompPostcompose_hom_app_hom, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, CategoryTheory.Adjunction.leftAdjointCompNatTransâââ_eq_conjugateEquiv_symm, IsCoverDense.sheafHom_eq, CategoryTheory.NatTrans.shift_comm_assoc, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map, IsCoverDense.restrictHomEquivHom_naturality_right_symm, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, IsCoverDense.restrictHomEquivHom_naturality_left, CategoryTheory.BasedCategory.whiskerLeft_toNatTrans, CategoryTheory.Adjunction.unit_rightAdjointUniq_hom, ModuleCat.extendScalars_assoc_assoc, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, IsCoverDense.sheafHom_restrict_eq, whiskeringLeftâObjObjMap_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, whiskerLeft_comp_whiskerRight_assoc, leftDerived_fac_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv, CategoryTheory.Adjunction.leftAdjointUniq_hom_counit, CategoryTheory.Adjunction.toComonad_δ, CategoryTheory.Presheaf.isLocallyInjective_whisker, CategoryTheory.Limits.LimitPresentation.reindex_Ď, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerLeft, CategoryTheory.Limits.Κ_colimitCompWhiskeringLeftIsoCompColimit_hom, IsCoverDense.restrictHomEquivHom_naturality_left_assoc, whiskerLeft_app, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_leftUnitor, CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft_assoc, PresheafOfModules.pullback_assoc, CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac, CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc, CategoryTheory.conjugateEquiv_whiskerRight, CategoryTheory.NatTrans.shift_comm, functorialityCompPrecompose_hom_app_hom, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_right, CategoryTheory.Adjunction.comp_counit, NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight, whiskeringLeftâMap_app_app, CategoryTheory.Join.mapWhiskerLeft_associator_hom, CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits, AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality, CategoryTheory.NatTrans.op_whiskerLeft_assoc, whiskerLeft_comp, rightKanExtension_hom_ext_iff, CategoryTheory.ExactFunctor.whiskeringLeft_obj_map, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, postcomposeWhiskerLeftMapCone_inv_hom, CategoryTheory.Presheaf.isLocallyInjective_whisker_iff, CategoryTheory.Adjunction.toMonad_Îź, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_comp, precomposeWhiskerLeftMapCocone_hom_hom, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, rightDerivedNatTrans_fac, CategoryTheory.Limits.fiberwiseColim_map_app, triangle, precomposeWhiskerLeftMapCocone_inv_hom, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_Ď_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_NâÎâ_hom, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_comp, isoWhiskerLeft_inv, leftKanExtension_hom_ext_iff, whiskerLeft_twice, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence, CategoryTheory.mateEquiv_symm_apply, CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful, CategoryTheory.Join.mapWhiskerRight_associator_hom, IsCoverDense.restrictHomEquivHom_naturality_right_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerLeft, CategoryTheory.NatTrans.CommShiftCore.shift_comm, CategoryTheory.Grothendieck.pre_comp_map, CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff, CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left, CategoryTheory.NatTrans.CommShiftCore.shift_comm_assoc, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_left, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, PresheafOfModules.colimitPresheafOfModules_map, CategoryTheory.Adjunction.CoreUnitCounit.right_triangle, leftKanExtensionCompIsoOfPreserves_hom_fac, rightKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map, toSheafify_pullbackSheafificationCompatibility, CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_naturalityâ, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_f, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map_assoc, CategoryTheory.Join.mapWhiskerRight_whiskerLeft, CategoryTheory.Adjunction.leftAdjointUniq_hom_counit_assoc, CategoryTheory.NatTrans.Equifibered.whiskerLeft, CategoryTheory.Adjunction.Triple.leftToRight_eq_counits, CategoryTheory.Join.mapWhiskerRight_whiskerLeft_assoc, whiskeringLeft_obj_map, whiskerLeft_id, CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.NatTrans.leftOpWhiskerRight, whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom_assoc, CategoryTheory.Limits.colimit.pre_map, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, CategoryTheory.Join.mapWhiskerLeft_associator_hom_assoc, CategoryTheory.Limits.ColimitPresentation.reindex_Κ, CategoryTheory.Join.mapWhiskerLeft_rightUnitor_hom, whiskerLeft_id', leftDerived_fac, postcomposeWhiskerLeftMapCone_hom_hom, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_base, CategoryTheory.Join.mapWhiskerRight_rightUnitor_hom, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_associator, ModuleCat.extendScalars_assoc', CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ', CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, CategoryTheory.NatTrans.leftOpWhiskerRight_assoc, CategoryTheory.Adjunction.left_triangle, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_fst_app, leftKanExtensionCompIsoOfPreserves_inv_fac, inv_whiskerLeft, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc, CategoryTheory.Presheaf.isLocallySurjective_whisker_iff, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, CategoryTheory.Adjunction.CoreUnitCounit.left_triangle, isRightKanExtension_iff_precomp, PresheafOfModules.pushforward_assoc, CategoryTheory.Adjunction.Triple.whiskerLeft_leftToRight_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_naturalityâ, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_assoc, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom, CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right, whiskerLeft_comp_whiskerRight, rightDerivedNatTrans_fac_assoc, CategoryTheory.NatTrans.op_whiskerLeft, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_Ď_assoc, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map, functorialityCompPrecompose_inv_app_hom, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.conjugateEquiv_whiskerLeft, CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_assoc, ModuleCat.extendScalars_comp_id_assoc, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_Ď, CategoryTheory.Join.mapWhiskerLeft_whiskerLeft_assoc, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp_assoc, CategoryTheory.Adjunction.leftAdjointCompNatTransâââ_eq_conjugateEquiv_symm, CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom_naturality_assoc, descOfIsLeftKanExtension_fac, isLeftKanExtension_iff_precomp, CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom_assoc, CategoryTheory.Adjunction.right_triangle, CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc, isIso_whiskerLeft, CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft, ModuleCat.extendScalars_comp_id, leftDerivedNatTrans_fac, CategoryTheory.NatTrans.Coequifibered.whiskerLeft, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_snd_app, CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformPrecomposeObjSquare_iso_hom_comp, CategoryTheory.Limits.limit.map_pre, CategoryTheory.Adjunction.comp_unit, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, CategoryTheory.Cat.whiskerLeft_toNatTrans, CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_assoc, functorialityCompPostcompose_inv_app_hom, IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, isoWhiskerLeft_hom, CategoryTheory.Limits.whiskerLeft_Κ_colimitCompWhiskeringLeftIsoCompColimit_inv, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_g, CategoryTheory.Equivalence.congrRight_unitIso_hom_app, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, ContinuousCohomology.MultiInd.d_succ, CategoryTheory.GrothendieckTopology.overMapPullback_assoc, CategoryTheory.NatTrans.CommShift.whiskerLeft, LightCondensed.lanPresheafExt_hom, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp, whiskerRight_left, CategoryTheory.Join.eq_mkNatTrans, CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map, CategoryTheory.Limits.whiskerLeft_Κ_colimitCompWhiskeringLeftIsoCompColimit_inv_assoc, CategoryTheory.Sum.functorEquiv_unitIso, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_rightUnitor, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map_assoc, id_hcomp, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, pushforwardContinuousSheafificationCompatibility_hom_app_val, IsCoverDense.restrictHomEquivHom_naturality_right, CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_assoc, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity, CategoryTheory.Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful, rightDerived_fac, CategoryTheory.Adjunction.Triple.whiskerLeft_leftToRight, CategoryTheory.Equivalence.congrRight_counitIso_inv_app, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv_assoc, CategoryTheory.Equivalence.congrRight_counitIso_hom_app, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_Ď, CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom_assoc, CategoryTheory.Sum.functorEquiv_counitIso, IsCoverDense.restrictHomEquivHom_naturality_left_symm, CategoryTheory.SmallObject.SuccStruct.ofNatTrans_toSucc, ModuleCat.extendScalars_assoc, CategoryTheory.Equivalence.congrRight_unitIso_inv_app, liftOfIsRightKanExtension_fac_assoc, CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.NatTrans.IsMonoidal.whiskerLeft, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit_assoc, whiskeringLeft_map_app_app, CategoryTheory.mateEquiv_apply
|
whiskerRight đ | CompOp | 256 mathmath: CategoryTheory.Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget, CategoryTheory.SingleFunctors.Hom.comm, CategoryTheory.Cat.whiskerRight_toNatTrans, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_associator, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatΚCompResolutionNatTransOfIsLocalizationWeakEquivalences, CategoryTheory.Limits.fiberwiseColimit_map, CategoryTheory.IndParallelPairPresentation.hf, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerRight, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_base, CategoryTheory.NonemptyParallelPairPresentationAux.hf, CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_leftUnitor, CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit, mapCoconePrecompose_inv_hom, CategoryTheory.Join.mapWhiskerRight_leftUnitor_hom, CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom_assoc, pentagon, CategoryTheory.Join.isoMkFunctor_hom_app, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc, mapConePostcompose_inv_hom, CategoryTheory.Join.mapWhiskerLeft_whiskerRight, CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, CategoryTheory.sheafCompose_map_val, CategoryTheory.Adjunction.Triple.rightToLeft_eq_units, CategoryTheory.NatTrans.CommShift.shift_comm, CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse, PreservesRightKanExtension.preserves, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_Ď_assoc, CategoryTheory.Join.mkFunctor_edgeTransform, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_Ď_assoc, CategoryTheory.WithTerminal.commaFromOver_map_left, isIso_whiskerRight, CategoryTheory.Adjunction.leftAdjointCompNatTransâââ_eq_conjugateEquiv_symm, CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift, CategoryTheory.Limits.CategoricalPullback.natTrans_ext_iff, CategoryTheory.sheafComposeIso_hom_fac, CategoryTheory.NatTrans.Coequifibered.whiskerRight, sheafPushforwardContinuousNatTrans_app_val, CategoryTheory.NatTrans.shift_comm_assoc, CategoryTheory.SingleFunctors.Hom.comm_assoc, CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map, CategoryTheory.NatTrans.CommShift.whiskerRight, CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom, CategoryTheory.NatTrans.op_whiskerRight_assoc, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions, CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft_assoc, whiskerRight_id', CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd, ModuleCat.extendScalars_assoc_assoc, CategoryTheory.Join.mapWhiskerRight_whiskerRight, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, whiskerLeft_comp_whiskerRight_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, CategoryTheory.Limits.ColimitPresentation.map_Κ, CategoryTheory.Triangulated.SpectralObject.Ďâ_map_homâ, LeftExtension.postcomposeâObjMkIso_inv_right_app, CategoryTheory.Adjunction.toComonad_δ, CategoryTheory.NatTrans.rightOpWhiskerRight, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app, CategoryTheory.Join.mapWhiskerLeft_whiskerRight_assoc, CategoryTheory.Join.isoMkFunctor_inv_app, CategoryTheory.GrothendieckTopology.W_of_preservesSheafification, CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv_assoc, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, whiskeringLeftâObjMap_app, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac, CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc, CategoryTheory.conjugateEquiv_whiskerRight, CategoryTheory.NatTrans.op_whiskerRight, CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful, CategoryTheory.NatTrans.shift_comm, CategoryTheory.NatTrans.unop_whiskerRight, CategoryTheory.Adjunction.comp_counit, NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, CategoryTheory.BasedCategory.whiskerRight_toNatTrans, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, CategoryTheory.Join.mapWhiskerLeft_associator_hom, CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits, CategoryTheory.GrothendieckTopology.toPlus_comp_plusCompIso_inv, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst, CategoryTheory.Presheaf.isLocallyInjective_forget_iff, CategoryTheory.Adjunction.toMonad_Îź, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_comp, triangle, postcomposeâ_map_app_app_app_app, CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit, CategoryTheory.Κ_colimitCompWhiskeringRightIsoColimitComp_hom, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id, CategoryTheory.NatTrans.IsMonoidal.whiskerRight, CategoryTheory.Limits.colimit.map_post, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_comp, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_left, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatΚCompResolutionNatTransOfIsLocalizationWeakEquivalences, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence, LeftExtension.postcomposeâObjMkIso_hom_right_app, CategoryTheory.mateEquiv_symm_apply, CategoryTheory.Join.mapWhiskerRight_associator_hom, CategoryTheory.SimplicialObject.whiskering_map_app_app, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit_assoc, CategoryTheory.whiskerRight_Κ_colimitCompWhiskeringRightIsoColimitComp_inv_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerLeft, CategoryTheory.NatTrans.CommShiftCore.shift_comm, CategoryTheory.Limits.limit.map_post, CategoryTheory.NatTrans.CommShiftCore.shift_comm_assoc, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit_assoc, CategoryTheory.Sheaf.adjunction_unit_app_val, CategoryTheory.Adjunction.CoreUnitCounit.right_triangle, CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac, whiskerRight_zero, whiskeringLeftâ_map_app_app_app_app, rightKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit, CategoryTheory.NatTrans.rightOpWhiskerRight_assoc, CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit, whiskerRight_id, CategoryTheory.functorProdToProdFunctor_map, CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_right, rightKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_naturalityâ, CategoryTheory.WithInitial.commaFromUnder_map_right, CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection, CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_assoc, CategoryTheory.NatTrans.Equifibered.whiskerRight, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map_assoc, isLeftKanExtension_iff_postcompâ, CategoryTheory.Adjunction.Triple.leftToRight_eq_counits, CategoryTheory.Limits.colimit.pre_map', CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc, isoWhiskerRight_hom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w_assoc, CategoryTheory.IndParallelPairPresentation.hg, CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight_assoc, mapPresheaf_map_c, CategoryTheory.Limits.LimitPresentation.map_Ď, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.Presheaf.imageSieve_whisker_forget, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerRight, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc, RightExtension.postcomposeâObjMkIso_inv_left_app, CategoryTheory.Join.mapWhiskerLeft_associator_hom_assoc, CategoryTheory.sheafComposeIso_inv_fac_assoc, whiskeringRight_obj_map, CategoryTheory.Limits.limit.map_pre', CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, PreservesLeftKanExtension.preserves, whiskerRight_app, ModuleCat.extendScalars_id_comp_assoc, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_associator, ModuleCat.extendScalars_assoc', CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ', CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, ModuleCat.extendScalars_id_comp, CategoryTheory.Adjunction.left_triangle, leftKanExtensionCompIsoOfPreserves_inv_fac, whiskerRight_comp_assoc, CategoryTheory.Κ_colimitCompWhiskeringRightIsoColimitComp_hom_assoc, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst, CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft, CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom_assoc, CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc, CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit, CategoryTheory.Adjunction.CoreUnitCounit.left_triangle, mapConePostcompose_hom_hom, CategoryTheory.CosimplicialObject.whiskering_map_app_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_naturalityâ, AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, whiskerLeft_comp_whiskerRight, CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map, whiskerRight_comp, pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.conjugateEquiv_whiskerLeft, CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd, postcomposeâ_map_app_app_app, CategoryTheory.Adjunction.leftAdjointCompNatTransâââ_eq_conjugateEquiv_symm, mapCoconePrecompose_hom_hom, CategoryTheory.Join.mapWhiskerRight_whiskerRight_assoc, CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom, AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_assoc, CategoryTheory.Triangulated.SpectralObject.Ďâ_map_homâ, CategoryTheory.Adjunction.right_triangle, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_rightUnitor, CategoryTheory.whiskerRight_Κ_colimitCompWhiskeringRightIsoColimitComp_inv, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformPrecomposeObjSquare_iso_hom_comp, CategoryTheory.Adjunction.unit_leftAdjointUniq_hom, CategoryTheory.TransfiniteCompositionOfShape.map_incl, CategoryTheory.Adjunction.comp_unit, whiskerRight_twice, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_assoc, CategoryTheory.SingleFunctors.postcompFunctor_map_hom, CategoryTheory.sheafComposeIso_hom_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc, CategoryTheory.sheafComposeIso_inv_fac, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst, CategoryTheory.NatTrans.unop_whiskerRight_assoc, CategoryTheory.Triangulated.SpectralObject.Ďâ_map_homâ, ContinuousCohomology.MultiInd.d_succ, CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful, CategoryTheory.GrothendieckTopology.overMapPullback_assoc, CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_Ď, CategoryTheory.ExactFunctor.whiskeringRight_obj_map, isoWhiskerRight_inv, whiskerRight_left, CategoryTheory.Presheaf.isLocallyInjective_forget, CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit_assoc, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, isRightKanExtension_iff_postcompâ, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp, CategoryTheory.NonemptyParallelPairPresentationAux.hg, CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_Ďâ, hcomp_id, CategoryTheory.Limits.reflexivePair.whiskerRightMkNatTrans, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence, whiskeringRight_map_app_app, inv_whiskerRight, CategoryTheory.instEpiFunctorWhiskerRightOfPreservesEpimorphisms, RightExtension.postcomposeâObjMkIso_hom_left_app, CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso, AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity, CategoryTheory.GrothendieckTopology.plusCompIso_inv_eq_plusLift, CategoryTheory.sheafComposeNatTrans_fac, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc, ModuleCat.extendScalars_assoc, CategoryTheory.RightExactFunctor.whiskeringRight_obj_map, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_Ď, pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac, CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit_assoc, CategoryTheory.mateEquiv_apply, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
|
whiskeringLeft đ | CompOp | 353 mathmath: LeftExtension.coconeAtFunctor_map_hom, CategoryTheory.Adjunction.compUliftCoyonedaIso_hom_app_app_down, CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_inv_app, CategoryTheory.whiskeringLeft_comp_evaluation, leftExtensionEquivalenceOfIsoâ_functor_map_left, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, LeftExtension.precompâ_obj_hom_app, instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, whiskeringRightâ_obj_obj_map_app, CategoryTheory.Sum.functorEquivFunctorCompFstIso_inv_app_app, LeftExtension.precompâ_map_right, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Limits.Κ_colimitCompWhiskeringLeftIsoCompColimit_hom_assoc, whiskeringLeftâObjObjObj_obj_map_app_app, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, instIsIsoAppRanCounit, RightExtension.postcomposeâ_obj_left_map, CategoryTheory.Adjunction.compCoyonedaIso_inv_app_app, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, RightExtension.postcomposeâ_obj_right, smoothSheafCommRing.Κ_evalHom_apply, LeftExtension.postcompâ_map_right_app, CategoryTheory.whiskeringLeft_preservesLimitsOfShape, CategoryTheory.MonoidalCategory.externalProductCompDiagIso_hom_app_app, CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app, LaxMonoidal.ofBifunctor.secondMapâ_app_app_app, leftExtensionEquivalenceOfIsoâ_functor_obj_left, instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, IsRightKanExtension.nonempty_isUniversal, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableByâ_homEquiv, CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app, LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app, whiskeringLeft_obj_id, RightExtension.coneAt_pt, LeftExtension.postcompâ_obj_left, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, reflective', FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_down, LeftExtension.precomp_map_right, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, LeftExtension.precompâ_obj_left, RightExtension.coneAt_Ď_app, RightExtension.postcompâ_obj_left_map, CategoryTheory.Adjunction.compYonedaIso_hom_app_app, RightExtension.postcompâ_map_right, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, CategoryTheory.IsSifted.factorization_prodComparison_colim, ranCompLimIso_inv_app, whiskeringLeftâ_map_app_app_app_app_app_app, whiskeringLeft_obj_comp, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv, sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app, LeftExtension.precomp_obj_hom_app, CategoryTheory.Equivalence.congrLeft_counitIso_inv_app, curryObjProdComp_hom_app_app, CategoryTheory.RightExactFunctor.whiskeringLeft_map_app, LeftExtension.coconeAtWhiskerRightIso_inv_hom, RightExtension.precomp_map_left, LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc, CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, instIsLeftKanExtensionObjLanAppLanUnit, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_hom_app_app_f, LeftExtension.postcomposeâ_obj_right_map, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_hom_app_app_f, sheafPushforwardContinuous_map_val_app, RightExtension.mk_hom, leftExtensionEquivalenceOfIsoâ_inverse_map_left, FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_down, leftExtensionEquivalenceOfIsoâ_inverse_obj_left, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, CategoryTheory.Enriched.FunctorCategory.diagram_map_app, CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app, lanUnit_app_app_lanAdjunction_counit_app_app, CategoryTheory.Adjunction.compUliftCoyonedaIso_inv_app_app_down, lanUnit_app_whiskerLeft_lanAdjunction_counit_app, whiskerLeft_obj_map_bijective_of_isCoverDense, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app, whiskeringLeftâ_obj_obj_obj_map_app, instIsIsoAppLanUnit, LeftExtension.postcomposeâObjMkIso_inv_right_app, sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, CategoryTheory.TwoSquare.isIso_lanBaseChange_app, instIsEquivalenceRightExtensionPostcompâOfIsIso, CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app, smoothSheafCommRing.Κ_evalHom, CategoryTheory.Limits.Κ_colimitCompWhiskeringLeftIsoCompColimit_hom, CategoryTheory.Localization.faithful_whiskeringLeft, CategoryTheory.Presheaf.restrictedULiftYoneda_map_app, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_inv_app_app, RightExtension.coneAtFunctor_obj, whiskeringLeftâObjMap_app, whiskeringLeftObjIdIso_hom_app_app, LeftExtension.IsPointwiseLeftKanExtensionAt.Κ_isoColimit_hom, LeftExtension.postcomposeâ_map_right_app, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom, CategoryTheory.Equivalence.congrLeft_functor, Monoidal.whiskeringLeft_Îľ_app, FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app, CategoryTheory.ExactFunctor.whiskeringLeft_map_app, Monoidal.whiskeringLeft_Îź_app, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableByâ'_homEquiv, RightExtension.postcompâ_obj_left_obj, CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, instIsEquivalenceLeftExtensionPostcompâOfIsIso, isIso_ranAdjunction_unit_app_iff, LeftExtension.postcomposeâ_obj_hom_app, CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_hom_app, whiskeringLeftâ_obj_obj_map_app_app_app_app, whiskeringLeftâMap_app_app, CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft, SSet.Truncated.rightExtensionInclusion_right_as, RightExtension.coneAtWhiskerRightIso_inv_hom, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_hom_app_app, LeftExtension.postcompâ_obj_hom_app, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app, whiskeringLeftâ_obj_map_app_app_app_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, CategoryTheory.Localization.full_whiskeringLeft, CategoryTheory.CostructuredArrow.mapCompΚCompGrothendieckProj_inv_app, constCompWhiskeringLeftIso_hom_app_app, lanCompColimIso_inv_app, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app, leftExtensionEquivalenceOfIsoâ_inverse_map_right, CategoryTheory.MonoidalCategory.externalProductCompDiagIso_inv_app_app, LeftExtension.postcomposeâ_obj_right_obj, whiskeringLeftâ_obj_map_app_app_app, CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff, CategoryTheory.TwoSquare.instIsIsoFunctorLanBaseChangeOfGuitartExact, ranObjObjIsoLimit_inv_Ď_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app, RightExtension.precomp_obj_right, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_Ď_assoc, CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app, CategoryTheory.whiskeringLeft_preservesLimits, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, LeftExtension.IsPointwiseLeftKanExtensionAt.Κ_isoColimit_hom_assoc, leftExtensionEquivalenceOfIsoâ_inverse_obj_right, HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, RightExtension.IsPointwiseRightKanExtension.isIso_hom, RightExtension.mk_right_as, LeftExtension.IsPointwiseLeftKanExtensionAt.Κ_isoColimit_inv_assoc, leftExtensionEquivalenceOfIsoâ_counitIso_inv_app_right_app, isIso_ranAdjunction_homEquiv_iff, CategoryTheory.Equivalence.congrLeft_unitIso_inv_app, LeftExtension.postcomposeâObjMkIso_hom_right_app, ranCounit_app_app_ranAdjunction_unit_app_app_assoc, RightExtension.postcompâ_map_left_app, CategoryTheory.Equivalence.congrLeft_unitIso_hom_app, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, instIsEquivalenceObjWhiskeringLeft, LeftExtension.postcompâ_obj_right_map, ranObjObjIsoLimit_hom_Ď_assoc, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, PreservesPointwiseLeftKanExtensionAt.preserves, Monoidal.whiskeringLeft_Ρ_app, instReflectsIsomorphismsDiscreteObjWhiskeringLeftIncl, CategoryTheory.whiskeringLeft_preservesColimit, LeftExtension.coconeAtFunctor_obj, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app, instIsRightKanExtensionObjRanAppRanCounit, LeftExtension.coconeAtWhiskerRightIso_hom_hom, RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app, instIsEquivalenceLeftExtensionCompPrecomp, leftExtensionEquivalenceOfIsoâ_inverse_obj_hom_app, whiskeringLeftâ_obj_obj_obj_map_app_app_app, CategoryTheory.Idempotents.KaroubiUniversalâ.counitIso_hom_app_app_f, CategoryTheory.Idempotents.KaroubiUniversalâ.counitIso_inv_app_app_f, instPreservesLimitOfIsCoreflexivePairDiscreteObjWhiskeringLeftIncl, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, LeftExtension.precomp_obj_right, CategoryTheory.Adjunction.compYonedaIso_inv_app_app, whiskeringRightâ_map_app_app_app, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app, lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc, LeftExtension.postcomposeâ_obj_left, isIso_lanAdjunction_homEquiv_symm_iff, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_map_app, LeftExtension.IsPointwiseLeftKanExtension.isIso_hom, RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_Ď, LeftExtension.precomp_obj_left, CategoryTheory.Equivalence.congrLeftFunctor_map, SSet.Truncated.rightExtensionInclusion_left, leftExtensionEquivalenceOfIsoâ_functor_obj_hom_app, whiskeringLeftâ_map_app_app_app_app, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, toSheafify_pullbackSheafificationCompatibility, lanAdjunction_unit, PreservesPointwiseRightKanExtensionAt.preserves, RightExtension.IsPointwiseRightKanExtension.isRightKanExtension, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_hom_app_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, RightExtension.mk_left, CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_hom_app_app, whiskeringLeft_obj_map, RightExtension.postcompâ_obj_right, CategoryTheory.Sum.functorEquivFunctorCompSndIso_inv_app_app, FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down, LeftExtension.postcomposeâ_map_left, LeftExtension.postcompâ_obj_right_obj, CategoryTheory.Adjunction.compCoyonedaIso_hom_app_app, closedIhom_map_app, whiskeringLeftObjIdIso_inv_app_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_app, RightExtension.postcomposeâ_obj_hom_app, RightExtension.precomp_obj_hom_app, ranCounit_app_app_ranAdjunction_unit_app_app, RightExtension.precomp_map_right, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_inv_app_app_f, RightExtension.postcomposeâObjMkIso_inv_left_app, IsCoverDense.sheafCoyonedaHom_app, reflective, RightExtension.postcomposeâ_map_left_app, FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_down, RightExtension.postcomposeâ_obj_left_obj, FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_down, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_app, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, constCompWhiskeringLeftIso_inv_app_app, RightExtension.postcomposeâ_map_right, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app, CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_Ď_assoc, LeftExtension.precomp_map_left, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, CategoryTheory.Quotient.full_whiskeringLeft_functor, CategoryTheory.Quotient.faithful_whiskeringLeft_functor, LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, LeftExtension.precompâ_obj_right, ranObjObjIsoLimit_hom_Ď, CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app, CategoryTheory.whiskeringLeft_preservesColimitsOfShape, LeftExtension.coconeAt_pt, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app, CategoryTheory.Idempotents.karoubiUniversalâ_unitIso, LeftExtension.postcompâ_map_left, RightExtension.coneAtFunctor_map_hom, RightExtension.coneAtWhiskerRightIso_hom_hom, CategoryTheory.MonoidalCategory.externalProductSwap_inv_app_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app, CategoryTheory.Idempotents.karoubiUniversalâ_inverse, LeftExtension.mk_right, CategoryTheory.CostructuredArrow.mapCompΚCompGrothendieckProj_hom_app, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app, RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_Ď, smoothSheafCommRing.Κ_evalHom_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_inv_app_app, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_Ď_assoc, CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app, CategoryTheory.Adjunction.whiskerLeft_unit_app_app, leftExtensionEquivalenceOfIsoâ_unitIso_hom_app_right_app, whiskeringLeftâObjObjObj_obj_obj_map_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_Ď, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, ranObjObjIsoLimit_inv_Ď, CategoryTheory.Equivalence.congrLeft_counitIso_hom_app, LeftExtension.IsPointwiseLeftKanExtensionAt.Κ_isoColimit_inv, curryObjProdComp_inv_app_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_app, RightExtension.postcompâ_obj_hom_app, ranAdjunction_counit, whiskeringLeftâ_obj_obj_obj_obj_obj_map_app, instIsIsoAppLanUnit_1, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app, CategoryTheory.Equivalence.congrLeft_inverse, ranCounit_app_whiskerLeft_ranAdjunction_unit_app, LeftExtension.coconeAt_Κ_app, Monoidal.whiskeringLeft_δ_app, LeftExtension.mk_left_as, whiskeringLeftObjCompIso_hom_app_app, LeftExtension.precompâ_map_left, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, SSet.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.Limits.whiskerLeft_Κ_colimitCompWhiskeringLeftIsoCompColimit_inv, CategoryTheory.MonoidalCategory.externalProductSwap_hom_app_app, coreflective', CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app, OplaxMonoidal.ofBifunctor.firstMapâ_app_app_app, IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, CategoryTheory.Sum.functorEquivFunctorCompSndIso_hom_app_app, CategoryTheory.TwoSquare.lanBaseChange_app, CategoryTheory.Sum.functorEquivFunctorCompFstIso_hom_app_app, CategoryTheory.whiskeringLeftCompEvaluation_inv_app, whiskeringLeft_obj_obj, ranCompLimIso_hom_app, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app, sheafAdjunctionCocontinuous_homEquiv_apply_val, leftExtensionEquivalenceOfIsoâ_counitIso_hom_app_right_app, CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app, CategoryTheory.Limits.whiskerLeft_Κ_colimitCompWhiskeringLeftIsoCompColimit_inv_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_hom_app_app, ranAdjunction_unit_app, lanAdjunction_counit_app, RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_Ď_assoc, isIso_lanAdjunction_counit_app_iff, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp, coreflective, pushforwardContinuousSheafificationCompatibility_hom_app_val, whiskeringLeftâ_obj_obj_obj_obj_map_app_app, CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, sheafAdjunctionCocontinuous_unit_app_val, lanUnit_app_app_lanAdjunction_counit_app_app_assoc, leftExtensionEquivalenceOfIsoâ_functor_map_right, CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_inv_app_app, whiskeringLeftâ_obj_obj_map_app_app, instIsIsoAppRanCounit_1, RightExtension.postcomposeâObjMkIso_hom_left_app, whiskeringRightâ_obj_map_app_app, CategoryTheory.whiskeringLeftCompEvaluation_hom_app, leftExtensionEquivalenceOfIsoâ_unitIso_inv_app_right_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv, CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_Ď, lanCompColimIso_hom_app, LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc, whiskeringLeftâObjObjObj_map_app_app_app, LeftExtension.mk_hom, IsLeftKanExtension.nonempty_isUniversal, whiskeringLeft_map_app_app, CategoryTheory.Adjunction.whiskerLeft_counit_app_app, RightExtension.precomp_obj_left, instIsEquivalenceRightExtensionCompPrecomp, leftExtensionEquivalenceOfIsoâ_functor_obj_right, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_inv_app_app, whiskeringLeftObjCompIso_inv_app_app, CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
|
whiskeringLeftObjCompIso đ | CompOp | 2 mathmath: whiskeringLeftObjCompIso_hom_app_app, whiskeringLeftObjCompIso_inv_app_app
|
whiskeringLeftObjIdIso đ | CompOp | 2 mathmath: whiskeringLeftObjIdIso_hom_app_app, whiskeringLeftObjIdIso_inv_app_app
|
whiskeringLeftâ đ | CompOp | 54 mathmath: whiskeringLeftâObjObjObj_obj_map_app_app, LaxMonoidal.ofBifunctor.secondMapâ_app_app_app, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Limits.PreservesColimitâ.map_Κ_comp_isoColimitUncurryWhiskeringLeftâ_inv_assoc, whiskeringLeftâ_map_app_app_app_app_app_app, CategoryTheory.Limits.PreservesLimitâ.isoObjConePointsOfIsColimit_inv_comp_map_Ď, CategoryTheory.Limits.PreservesColimitâ.map_Κ_comp_isoColimitUncurryWhiskeringLeftâ_inv, curryâObjProdComp_inv_app_app_app, whiskeringLeftâObjObjMap_app, whiskeringLeftâ_obj_obj_obj_map_app, whiskeringLeftâ_obj_obj_obj_obj_obj, CategoryTheory.Localization.liftâ_iso_hom_app_appâ, CategoryTheory.Limits.PreservesColimitâ.map_Κ_comp_isoObjConePointsOfIsColimit_hom, whiskeringLeftâObjMap_app, curryâObjProdComp_hom_app_app_app, CategoryTheory.Limits.PreservesLimitâ.isoObjConePointsOfIsLimit_hom_comp_Ď, whiskeringLeftâ_obj_obj_map_app_app_app_app, whiskeringLeftâMap_app_app, whiskeringLeftâ_obj_map_app_app_app_app_app, CategoryTheory.Limits.PreservesColimitâ.map_Κ_comp_isoObjConePointsOfIsColimit_hom_assoc, whiskeringLeftâ_obj_map_app_app_app, CategoryTheory.Limits.PreservesLimitâ.isoObjConePointsOfIsColimit_inv_comp_map_Ď_assoc, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app, mapConeâ_pt, CategoryTheory.Limits.PreservesLimitâ.nonempty_isLimit_mapConeâ, whiskeringLeftâ_obj_obj_obj_map_app_app_app, mapConeâ_Ď_app, CategoryTheory.Limits.PreservesLimitâ.isoObjConePointsOfIsLimit_hom_comp_Ď_assoc, CategoryTheory.Localization.Monoidal.liftingâCurriedTensorPost_iso, whiskeringLeftâ_map_app_app_app_app, CategoryTheory.Limits.PreservesLimitâ.isoLimitUncurryWhiskeringLeftâ_inv_comp_Ď, mapCoconeâ_pt, mapCoconeâ_Κ_app, CategoryTheory.Limits.PreservesLimitâ.isoLimitUncurryWhiskeringLeftâ_inv_comp_Ď_assoc, CategoryTheory.Localization.liftâNatTrans_app_app, CategoryTheory.Limits.PreservesColimitâ.Κ_comp_isoObjConePointsOfIsColimit_inv, CategoryTheory.Limits.PreservesLimitâ.isoLimitUncurryWhiskeringLeftâ_hom_comp_map_Ď, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, whiskeringLeftâ_obj_obj_obj_obj_map, CategoryTheory.Limits.PreservesLimitâ.isoLimitUncurryWhiskeringLeftâ_hom_comp_map_Ď_assoc, CategoryTheory.Limits.PreservesColimitâ.Κ_comp_isoColimitUncurryWhiskeringLeftâ_hom_assoc, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app, OplaxMonoidal.ofBifunctor.firstMapâ_app_app_app, CategoryTheory.Limits.PreservesColimitâ.Κ_comp_isoObjConePointsOfIsColimit_inv_assoc, CategoryTheory.Localization.liftâ_iso_hom_app_appâ, CategoryTheory.Limits.PreservesColimitâ.Κ_comp_isoColimitUncurryWhiskeringLeftâ_hom, CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeftâOfPreservesLimitâ, whiskeringLeftâ_obj_obj_obj_obj_map_app_app, CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeftâOfPreservesColimitâ, whiskeringLeftâ_obj_obj_map_app_app, CategoryTheory.Localization.associator_hom_app_app_app, whiskeringLeftâObjObjObj_map_app_app_app, CategoryTheory.Limits.PreservesColimitâ.nonempty_isColimit_mapCoconeâ, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
|
whiskeringLeftâ đ | CompOp | 9 mathmath: whiskeringLeftâ_map_app_app_app_app_app_app, whiskeringLeftâ_obj_obj_obj_obj_obj_obj_obj, whiskeringLeftâ_obj_obj_map_app_app_app_app, whiskeringLeftâ_obj_map_app_app_app_app_app, whiskeringLeftâ_obj_obj_obj_map_app_app_app, CategoryTheory.Localization.liftâNatTrans_app_app_app, whiskeringLeftâ_obj_obj_obj_obj_obj_map_app, whiskeringLeftâ_obj_obj_obj_obj_obj_obj_map, whiskeringLeftâ_obj_obj_obj_obj_map_app_app
|
whiskeringLeftâMap đ | CompOp | 1 mathmath: whiskeringLeftâMap_app_app
|
whiskeringLeftâObj đ | CompOp | 4 mathmath: whiskeringLeftâObj_map, whiskeringLeftâ_map_app_app_app_app_app_app, whiskeringLeftâMap_app_app, whiskeringLeftâObj_obj
|
whiskeringLeftâObjMap đ | CompOp | 2 mathmath: whiskeringLeftâObj_map, whiskeringLeftâObjMap_app
|
whiskeringLeftâObjObj đ | CompOp | 5 mathmath: whiskeringLeftâObjMap_app, whiskeringLeftâ_obj_map_app_app_app_app_app, whiskeringLeftâObj_obj, whiskeringLeftâObjObj_map, whiskeringLeftâObjObj_obj
|
whiskeringLeftâObjObjMap đ | CompOp | 2 mathmath: whiskeringLeftâObjObjMap_app, whiskeringLeftâObjObj_map
|
whiskeringLeftâObjObjObj đ | CompOp | 8 mathmath: whiskeringLeftâObjObjObj_obj_map_app_app, whiskeringLeftâObjObjMap_app, whiskeringLeftâ_obj_obj_map_app_app_app_app, whiskeringLeftâObjObjObj_obj_obj_obj_obj, whiskeringLeftâObjObjObj_obj_obj_obj_map, whiskeringLeftâObjObjObj_obj_obj_map_app, whiskeringLeftâObjObjObj_map_app_app_app, whiskeringLeftâObjObj_obj
|
whiskeringRight đ | CompOp | 194 mathmath: whiskeringRightObjIdIso_hom_app_app, CategoryTheory.whiskeringRightPreservesLimits, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding, whiskeringRightâ_obj_obj_map_app, CategoryTheory.whiskeringRightPreservesColimits, full_whiskeringRight_obj, CategoryTheory.Idempotents.functorExtensionâ_map_app_f, curryObjCompIso_hom_app_app, CategoryTheory.whiskering_linearCoyoneda, whiskeringLeftâObjObjObj_obj_map_app_app, CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_hom_app, LaxMonoidal.ofBifunctor.secondMapâ_app_app_app, whiskeringRight_obj_id, IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities, CategoryTheory.Equivalence.congrFullSubcategory_counitIso, IsCoverDense.isoOver_hom_app, CategoryTheory.Idempotents.functorExtension_map_app, CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app, CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app, whiskeringLeftâ_map_app_app_app_app_app_app, LaxMonoidal.ofBifunctor.firstMapâ_app_app_app, CategoryTheory.preservesColimitNatIso_inv_app, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_Ď_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, compConstIso_hom_app_app, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_Ď_assoc, postcomposeâ_obj_obj_obj_map_app, CategoryTheory.RightExactFunctor.whiskeringRight_map_app, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_hom_app_app_f, CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight, CategoryTheory.LeftExactFunctor.whiskeringRight_map_app, postcomposeâ_obj_obj_map_app_app, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans, AddCommGrpCat.coyonedaForget_inv_app_app, AlgebraicTopology.DoldKan.Îâ_obj_p_app, whiskeringLeftâObjObjMap_app, AddCommGrpCat.coyonedaForget_hom_app_app_hom, CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app, CategoryTheory.Idempotents.functorExtensionâ_obj_map_f, CategoryTheory.GrothendieckTopology.PreservesSheafification.le, CategoryTheory.Limits.limCompFlipIsoWhiskerLim_inv_app_app, whiskeringLeftâ_obj_obj_obj_map_app, CommMonCat.coyonedaForget_inv_app_app, CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight, ranCompIsoOfPreserves_inv_app, whiskeringLeftâObjMap_app, LeftExtension.postcomposeâ_map_right_app, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom, CategoryTheory.δ_app, CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, CategoryTheory.whiskering_linearYoneda, ranCompIsoOfPreserves_hom_app, CategoryTheory.whiskeringRightCompEvaluation_inv_app, CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app, CategoryTheory.whiskering_linearCoyonedaâ, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, CategoryTheory.Equivalence.congrRight_functor, CategoryTheory.Cat.exp_map, LeftExtension.postcomposeâ_obj_hom_app, CategoryTheory.preservesLimitNatIso_inv_app, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, whiskeringLeftâ_obj_obj_map_app_app_app_app, whiskeringLeftâMap_app_app, CategoryTheory.GrothendieckTopology.plusFunctorWhiskerRightIso_inv_app, whiskeringLeftâ_obj_map_app_app_app_app_app, OplaxMonoidal.whiskeringRight_δ_app, CategoryTheory.Equivalence.congrFullSubcategory_unitIso, CategoryTheory.whiskering_preadditiveYoneda, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.preservesColimitNatIso_hom_app, whiskeringLeftâ_obj_map_app_app_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_hom_app, CategoryTheory.whiskeringRight_preservesColimitsOfShape, CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_hom_app_app, postcomposeâ_map_app_app_app_app, CategoryTheory.Κ_colimitCompWhiskeringRightIsoColimitComp_hom, FullyFaithful.whiskeringRight_preimage_app, CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, CategoryTheory.sheafComposeNatTrans_app_uniq, CategoryTheory.whiskerRight_Κ_colimitCompWhiskeringRightIsoColimitComp_inv_assoc, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_hom_app_app, CategoryTheory.whiskeringRightCompEvaluation_hom_app, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app, whiskeringLeftâ_obj_obj_obj_map_app_app_app, LaxMonoidal.whiskeringRight_Îź_app, CategoryTheory.Localization.Monoidal.isInvertedByâ, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, CategoryTheory.Sheaf.adjunction_unit_app_val, whiskeringRightâ_map_app_app_app, CategoryTheory.Cat.ihom_map, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_map_app, CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_inv_app, CategoryTheory.uliftYoneda_map_app, whiskeringLeftâ_map_app_app_app_app, postcomposeâ_obj_map_app_app, curryObjCompIso_inv_app_app, LaxMonoidal.whiskeringRight_Îľ_app, CommGrpCat.coyonedaForget_hom_app_app_hom, instIsEquivalenceObjWhiskeringRight, lanCompIsoOfPreserves_inv_app, CategoryTheory.ExactFunctor.whiskeringRight_map_app, CategoryTheory.Ρ_app, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, CategoryTheory.Limits.limIsoFlipCompWhiskerLim_hom_app_app, CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_inv_app_app, LeftExtension.postcomposeâ_map_left, closedIhom_map_app, RightExtension.postcomposeâ_obj_hom_app, AddCommMonCat.coyonedaForget_inv_app_app, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.Idempotents.functorExtensionâCompWhiskeringLeftToKaroubiIso_inv_app_app_f, whiskeringRight_obj_map, RightExtension.postcomposeâ_map_left_app, whiskeringRightObjCompIso_hom_app_app, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, RightExtension.postcomposeâ_map_right, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app, CategoryTheory.Κ_colimitCompWhiskeringRightIsoColimitComp_hom_assoc, OplaxMonoidal.ofBifunctor.secondMapâ_app_app_app, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app, whiskeringRightObjIdIso_inv_app_app, CommGrpCat.coyonedaForget_inv_app_app, CategoryTheory.whiskeringRight_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, IsCoverDense.isoOver_inv_app, CommMonCat.coyonedaForget_hom_app_app_hom, postcomposeâ_obj_obj_map_app, CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, CategoryTheory.Limits.limCompFlipIsoWhiskerLim_hom_app_app, whiskeringRight_obj_obj, lanCompIsoOfPreserves_hom_app, postcomposeâ_obj_map_app_app_app, whiskeringLeftâObjObjObj_obj_obj_map_app, postcomposeâ_map_app_app_app, OplaxMonoidal.whiskeringRight_Ρ_app, PresheafOfModules.freeAdjunction_unit_app, faithful_whiskeringRight_obj, CategoryTheory.Limits.limIsoFlipCompWhiskerLim_inv_app_app, whiskeringLeftâ_obj_obj_obj_obj_obj_map_app, CategoryTheory.whiskerRight_Κ_colimitCompWhiskeringRightIsoColimitComp_inv, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app, CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, whiskeringRight_obj_comp, CategoryTheory.Equivalence.congrRight_inverse, AlgebraicTopology.DoldKan.Îâ_map_f_app, CategoryTheory.whiskering_linearYonedaâ, AddCommMonCat.coyonedaForget_hom_app_app_hom, CategoryTheory.Adjunction.whiskerRight_counit_app_app, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app, CategoryTheory.preservesLimitNatIso_hom_app, CategoryTheory.Equivalence.congrRight_unitIso_hom_app, CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app, OplaxMonoidal.ofBifunctor.firstMapâ_app_app_app, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_Ď, compConstIso_inv_app_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc, CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_inv_app_app, curry_obj_comp_flip, PresheafOfModules.freeAdjunction_homEquiv, CategoryTheory.Adjunction.whiskerRight_unit_app_app, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp, whiskeringLeftâ_obj_obj_obj_obj_map_app_app, CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, whiskeringRight_map_app_app, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app, CategoryTheory.Îľ_app, whiskeringLeftâ_obj_obj_map_app_app, whiskeringRightâ_obj_map_app_app, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app, CategoryTheory.Equivalence.congrRightFunctor_map, whiskeringRightObjCompIso_inv_app_app, CategoryTheory.whiskeringRight_comp_evaluation, CategoryTheory.Localization.associator_hom_app_app_app, CategoryTheory.Equivalence.congrRight_counitIso_inv_app, CategoryTheory.sheafComposeNatTrans_fac, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, CategoryTheory.Equivalence.congrRight_counitIso_hom_app, CategoryTheory.Îź_app, whiskeringLeftâObjObjObj_map_app_app_app, CategoryTheory.Equivalence.congrRight_unitIso_inv_app, CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_Ď, CategoryTheory.whiskering_preadditiveCoyoneda, CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
|
whiskeringRightObjCompIso đ | CompOp | 2 mathmath: whiskeringRightObjCompIso_hom_app_app, whiskeringRightObjCompIso_inv_app_app
|
whiskeringRightObjIdIso đ | CompOp | 2 mathmath: whiskeringRightObjIdIso_hom_app_app, whiskeringRightObjIdIso_inv_app_app
|