| Metric | Count |
|---|
DefinitionsAddCommGrpCat, hom, hom, hom', asHom, carrier, fullyFaihtfulForgetâToAddGrp, hasForgetToAddCommMonCat, hasForgetToAddGroup, instCategory, instCoeAddGrpCat, instCoeCommMonCat, instCoeSortType, instConcreteCategoryAddMonoidHomCarrier, instInhabited, instZeroHom, of, ofHom, str, uliftFunctor, AddCommGrpMax, AddCommGrpMaxAux, toAddCommGrpIso, toAddGrpIso, AddGrpCat, hom, hom', carrier, fullyFaihtfulForgetâToAddMonCat, hasForgetToAddMonCat, instCategory, instCoeMonCat, instCoeSortType, instConcreteCategoryAddMonoidHomCarrier, instInhabited, instZeroHom, of, ofHom, str, uliftFunctor, AddGrpMax, isoPerm, mulEquivPerm, addCommGroupIsoToAddEquiv, addGroupIsoToAddEquiv, commGroupIsoToMulEquiv, groupIsoToMulEquiv, CommGrpCat, hom, hom, hom', carrier, fullyFaithfulForgetâToGrp, hasForgetToCommMonCat, hasForgetToGroup, instCategory, instCoeCommMonCat, instCoeGrpCat, instCoeSortType, instConcreteCategoryMonoidHomCarrier, instInhabited, instOneHom, of, ofHom, str, uliftFunctor, CommGrpMax, GrpCat, hom, hom, hom', carrier, fullyFaithfulForgetâToMonCat, hasForgetToMonCat, instCategory, instCoeMonCat, instCoeSortType, instConcreteCategoryMonoidHomCarrier, instInhabited, instOneHom, of, ofHom, str, uliftFunctor, GrpMax, GrpMaxAux, toCommGrpIso, toGrpIso, addEquivIsoAddCommGroupIso, addEquivIsoAddGroupIso, mulEquivIsoCommGroupIso, mulEquivIsoGroupIso | 92 |
Theoremsext, ext_iff, asHom_hom_apply, asHom_injective, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forget_map, forget_reflects_isos, forgetâ_addGrp_map_ofHom, forgetâ_commMonCat_map_ofHom, forgetâ_map, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_neg_apply, hom_ofHom, id_apply, injective_of_mono, instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, int_hom_ext, int_hom_ext_iff, neg_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom_injective, uliftFunctor_map, uliftFunctor_obj, zero_apply, toAddCommGrpIso_hom, toAddCommGrpIso_inv, toAddGrpIso_hom, toAddGrpIso_inv, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forget_reflects_isos, forgetâ_map, forgetâ_map_ofHom, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_neg_apply, hom_ofHom, id_apply, instFullMonCatForgetâAddMonoidHomCarrierCarrier, neg_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom_injective, uliftFunctor_map, uliftFunctor_obj, zero_apply, addCommGroupIsoToAddEquiv_apply, addCommGroupIsoToAddEquiv_symm_apply, commGroupIsoToMulEquiv_apply, commGroupIsoToMulEquiv_symm_apply, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forget_map, forget_reflects_isos, forgetâ_commMonCat_map_ofHom, forgetâ_grp_map_ofHom, forgetâ_map, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, instFullGrpCatForgetâMonoidHomCarrierCarrier, inv_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom_injective, one_apply, uliftFunctor_map, uliftFunctor_obj, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forget_map, forget_reflects_isos, forgetâ_map, forgetâ_map_ofHom, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, instFullMonCatForgetâMonoidHomCarrierCarrier, inv_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom_injective, one_apply, uliftFunctor_map, uliftFunctor_obj, toCommGrpIso_hom, toCommGrpIso_inv, toGrpIso_hom, toGrpIso_inv | 134 |
| Total | 226 |
| Name | Category | Theorems |
|---|
asHom đ | CompOp | 2 mathmath: asHom_hom_apply, asHom_injective
|
carrier đ | CompOp | 232 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, CategoryTheory.ShortComplex.ShortExact.ab_finite_iff, forgetâAddGroup_preservesLimitsOfShape, coyoneda_obj_obj_coe, isZero_iff_subsingleton, binaryProductLimitCone_cone_pt, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, ModuleCat.FilteredColimits.colimit_smul_mk_eq, ModuleCat.forgetâ_reflectsLimitsOfSize, biproductIsoPi_inv_comp_Ď_apply, comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForgetâRingHomCarrierAddMonoidHomCarrier, ModuleCat.forgetâPreservesColimitsOfSize, hom_add, asHom_hom_apply, FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forgetâAddCommGroup_preservesLimitsOfSize, prop_isFinite_iff, ModuleCat.mkOfSMul'_smul, PresheafOfModules.Sheafify.add_smul, CategoryTheory.ShortComplex.ShortExact.ab_surjective_g, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.extFunctorObj_obj_coe, hom_zero, coe_of, PresheafOfModules.sections_property, RingCat.forgetâAddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', CochainComplex.HomComplex.leftHomologyData_K_coe, isColimit_iff_bijective_desc, ModuleCat.forgetâ_addCommGrp_essSurj, neg_hom_apply, forget_preservesLimits, ModuleCat.forgetâAddCommGroup_reflectsLimitOfShape, forget_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, ModuleCat.FilteredColimits.colimit_zero_eq, coe_comp, CategoryTheory.ShortComplex.Exact.ab_finite, forgetâ_map, ModuleCat.HasColimit.colimitCocone_Κ_app, subsingleton_of_isZero, Colimits.colimitCocone_Κ_app, ModuleCat.forgetâ_addCommGroup_full, PresheafOfModules.sectionsMap_coe, FilteredColimits.forgetâAddGroup_preservesFilteredColimits, CategoryTheory.ShortComplex.abToCycles_apply_coe, asHom_injective, CategoryTheory.ShortComplex.Exact.ab_range_eq_ker, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, ModuleCat.HasColimit.colimitCocone_pt_isModule, PresheafOfModules.toPresheaf_obj_coe, CategoryTheory.preadditiveYoneda_obj, ext_iff, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, forget_commGrp_preserves_epi, coyonedaForget_inv_app_app, free_map_coe, CategoryTheory.ShortComplex.ShortExact.ab_injective_f, CategoryTheory.ShortComplex.abLeftHomologyData_Ď, coyonedaForget_hom_app_app_hom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, HasLimit.productLimitCone_isLimit_lift, CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, biprodIsoProd_inv_comp_snd_apply, toCommGrp_obj_coe, CategoryTheory.ShortComplex.exact_iff_of_hasForget, binaryProductLimitCone_isLimit_lift, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, binaryProductLimitCone_cone_Ď_app_left, homAddEquiv_symm_apply_hom, hom_sub, ModuleCat.forgetâAddCommGroup_preservesLimits, free_obj_coe, Colimits.quotUliftToQuot_Κ, PresheafOfModules.presheaf_map_apply_coe, hom_id, hom_nsmul, HasLimit.productLimitCone_cone_pt_coe, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mkâ_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, ModuleCat.forgetâ_obj, range_eq_top_of_epi, forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyonedaâ, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, Colimits.Quot.desc_toCocone_desc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Preadditive.epi_iff_surjective, AddEquiv.toAddCommGrpIso_hom, CategoryTheory.Preadditive.mono_iff_injective, CategoryTheory.whiskering_preadditiveYoneda, forgetâAddGroup_preservesLimits, Colimits.quotToQuotUlift_Κ, ModuleCat.smulNatTrans_apply_app, zero_apply, id_apply, PresheafOfModules.unitHomEquiv_apply_coe, int_hom_ext_iff, Colimits.Quot.desc_toCocone_desc_app, PresheafOfModules.Sheafify.smul_add, Îź_forget_apply, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, epi_iff_surjective, PresheafOfModules.freeAdjunctionUnit_app, PresheafOfModules.presheaf_obj_coe, tensorObj_eq, forgetâ_addGrp_map_ofHom, FGModuleCat.instFiniteCarrierColimitModuleCatCompForgetâLinearMapIdObjIsFG, CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, forgetâAddCommMon_preservesLimitsOfShape, CategoryTheory.ShortComplex.abLeftHomologyData_f', CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, coyonedaType_obj_map, PresheafOfModules.toPresheaf_map_app_apply, coyonedaType_obj_obj_coe, mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, Colimits.toCocone_Κ_app, Colimits.Quot.Κ_desc, ModuleCat.FilteredColimits.forgetâAddCommGroup_preservesFilteredColimits, Colimits.Quot.map_Κ, ModuleCat.FilteredColimits.colimit_add_mk_eq', kernelIsoKer_inv_comp_Κ, HasLimit.productLimitCone_cone_Ď, ModuleCat.forgetâ_obj_moduleCat_of, forgetâAddGroup_preservesLimit, injective_of_mono, CategoryTheory.ShortComplex.ShortExact.injective_f, epi_iff_range_eq_top, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.Elements.fromFreeYoneda_app_apply, ModuleCat.HasColimit.coconePointSMul_apply, CategoryTheory.ShortComplex.ab_exact_iff, coe_id, forgetâAddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.ShortComplex.ShortExact.surjective_g, CategoryTheory.ShortComplex.zero_apply, Colimits.toCocone_pt_coe, CategoryTheory.ShortComplex.abLeftHomologyData_i, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, ModuleCat.mkOfSMul_smul, instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.sectionsMk_coe, biprodIsoProd_inv_comp_desc, uliftFunctor_map, biprodIsoProd_inv_comp_snd, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎUnitOpensCarrierCarrierCommRingCatRingCatSheaf, hom_comp, uliftFunctor_obj, ModuleCat.reflectsColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimitOfSize, biprodIsoProd_inv_comp_desc_apply, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkâ, CochainComplex.HomComplex.leftHomologyData_H_coe, CochainComplex.HomComplex.leftHomologyData'_K_coe, ofHom_apply, biprodIsoProd_inv_comp_fst_apply, biproductIsoPi_inv_comp_Ď, CategoryTheory.ShortComplex.ab_zero_apply, HasLimit.lift_hom_apply, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forgetâ_addCommGrp_additive, biprodIsoProd_inv_comp_fst, RingCat.forgetâAddCommGroup_preservesLimitsOfSize, CochainComplex.HomComplex.leftHomologyData'_H_coe, ofHom_hom, forgetâ_commMonCat_map_ofHom, forgetâAddCommMon_preservesLimitsOfSize, coyoneda_map_app, Colimits.Quot.desc_quotQuotUliftAddEquiv, forget_map, ModuleCat.forgetâ_reflectsLimits, kernelIsoKer_hom_comp_subtype, ModuleCat.forgetâPreservesColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimit, PresheafOfModules.freeAdjunction_unit_app, ModuleCat.forgetâAddCommGroup_preservesLimit, PresheafOfModules.Sheafify.zero_smul, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, CategoryTheory.whiskering_linearYonedaâ, PresheafOfModules.sections_ext_iff, hom_neg_apply, CommGrpCat.toAddCommGrp_obj_coe, PresheafOfModules.germ_ringCat_smul, ModuleCat.HasColimit.reflectsColimit, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, hom_add_apply, SheafOfModules.pushforwardSections_coe, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.Sheafify.map_smul, PresheafOfModules.germ_smul, PresheafOfModules.toSheafify_app_apply, instIsRightAdjointForgetAddMonoidHomCarrier, forget_isCorepresentable, binaryProductLimitCone_cone_Ď_app_right, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, ker_eq_bot_of_mono, PresheafOfModules.freeAdjunction_homEquiv, ModuleCat.forgetâAddCommGroupIsEquivalence, mono_iff_ker_eq_bot, CategoryTheory.preadditiveCoyoneda_obj, AddEquiv.toAddCommGrpIso_inv, hom_neg, PresheafOfModules.freeObjDesc_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎFreeOpensCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.exact_iff_exact_map_forgetâ, homAddEquiv_apply, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, coyonedaType_map_app, ModuleCat.FilteredColimits.colimit_add_mk_eq, toCommGrp_map, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, AlgebraicGeometry.Scheme.Modules.map_smul, hasLimit_iff_small_sections, hom_zsmul, forget_preservesLimitsOfSize, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forgetâ_map, coyoneda_obj_map, forget_reflects_isos
|
fullyFaihtfulForgetâToAddGrp đ | CompOp | â |
hasForgetToAddCommMonCat đ | CompOp | 3 mathmath: forgetâAddCommMon_preservesLimitsOfShape, forgetâ_commMonCat_map_ofHom, forgetâAddCommMon_preservesLimitsOfSize
|
hasForgetToAddGroup đ | CompOp | 9 mathmath: forgetâAddGroup_preservesLimitsOfShape, forgetâ_map, FilteredColimits.forgetâAddGroup_preservesFilteredColimits, forgetâAddGroup_preservesLimits, forgetâ_addGrp_map_ofHom, forgetâAddGroup_preservesLimit, instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, forgetâAddGroup_preservesLimitsOfSize, instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier
|
instCategory đ | CompOp | 379 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, forgetâAddGroup_preservesLimitsOfShape, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, image.lift_fac, coyoneda_obj_obj_coe, isZero_iff_subsingleton, binaryProductLimitCone_cone_pt, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, ModuleCat.forgetâ_reflectsLimitsOfSize, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, biproductIsoPi_inv_comp_Ď_apply, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda, comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForgetâRingHomCarrierAddMonoidHomCarrier, ModuleCat.forgetâPreservesColimitsOfSize, commGroupAddCommGroupEquivalence_functor, hom_add, PresheafOfModules.toPresheaf_preservesFiniteLimits, instPreservesMonomorphismsFree, ofHom_comp, FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forgetâAddCommGroup_preservesLimitsOfSize, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, ModuleCat.mkOfSMul'_smul, PresheafOfModules.Sheafify.add_smul, CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, hasLimit, injective_of_divisible, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, hasZeroObject, hasLimitsOfSize, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', CategoryTheory.Abelian.extFunctorObj_obj_coe, hom_zero, PresheafOfModules.sections_property, hasLimitsOfShape, instAB4AddCommGrpCat, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, RingCat.forgetâAddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', AlgebraicGeometry.Scheme.Modules.Hom.zero_app, hasColimit_of_small_quot, CochainComplex.HomComplex.leftHomologyData_K_coe, isColimit_iff_bijective_desc, commGroupAddCommGroupEquivalence_counitIso, ModuleCat.forgetâ_addCommGrp_essSurj, hasLimits, CochainComplex.HomComplex.leftHomologyData'_i, neg_hom_apply, forget_preservesLimits, ModuleCat.forgetâAddCommGroup_reflectsLimitOfShape, SheafOfModules.toSheaf_obj_val, forget_preservesLimitsOfShape, coe_comp, instHasFilteredColimitsAddCommGrpCat, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, forgetâ_map, ModuleCat.HasColimit.colimitCocone_Κ_app, Colimits.colimitCocone_Κ_app, PresheafOfModules.toPresheaf_map_toSheafify, ModuleCat.forgetâ_addCommGroup_full, PresheafOfModules.sectionsMap_coe, FilteredColimits.forgetâAddGroup_preservesFilteredColimits, CategoryTheory.ShortComplex.abToCycles_apply_coe, CochainComplex.HomComplex.leftHomologyData_Ď_hom_apply, asHom_injective, PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', SheafOfModules.ΚFree_mapFree_inv_assoc, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, PresheafOfModules.toPresheaf_preservesLimit, ModuleCat.HasColimit.colimitCocone_pt_isModule, PresheafOfModules.toPresheaf_obj_coe, CategoryTheory.Abelian.extFunctorObj_map, CategoryTheory.preadditiveYoneda_obj, ext_iff, uliftFunctor_additive, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, instMonoΚ, SheafOfModules.isSheaf, forget_commGrp_preserves_epi, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, CategoryTheory.preadditiveYonedaMap_app, coyonedaForget_inv_app_app, free_map_coe, instHasFiniteBiproducts, CategoryTheory.ShortComplex.abLeftHomologyData_Ď, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, coyonedaForget_hom_app_app_hom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, instFaithfulUliftFunctor, HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, biprodIsoProd_inv_comp_snd_apply, toCommGrp_obj_coe, CategoryTheory.ShortComplex.exact_iff_of_hasForget, CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, binaryProductLimitCone_isLimit_lift, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, AlgebraicGeometry.Scheme.Modules.isSheaf, binaryProductLimitCone_cone_Ď_app_left, homAddEquiv_symm_apply_hom, CategoryTheory.additive_yonedaObj', hom_sub, instAB4StarAddCommGrpCat, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.faithful_preadditiveCoyoneda, CategoryTheory.faithful_preadditiveYoneda, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, ModuleCat.forgetâAddCommGroup_preservesLimits, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, free_obj_coe, Colimits.quotUliftToQuot_Κ, PresheafOfModules.presheaf_map_apply_coe, hom_id, hom_nsmul, CategoryTheory.preservesLimits_preadditiveCoyoneda_obj, AlgebraicGeometry.Scheme.Modules.restrict_map, HasLimit.productLimitCone_cone_pt_coe, ModuleCat.forgetâ_obj, SheafOfModules.toSheaf_map_val, Colimits.colimitCocone_pt, forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyonedaâ, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, PresheafOfModules.sheafification_map, Colimits.Quot.desc_toCocone_desc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, uliftFunctor_preservesLimitsOfSize, CategoryTheory.Preadditive.epi_iff_surjective, AddEquiv.toAddCommGrpIso_hom, hasColimit, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.Preadditive.mono_iff_injective, CategoryTheory.Abelian.instAdditiveAddCommGrpCatExtFunctorObj, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.whiskering_preadditiveYoneda, forgetâAddGroup_preservesLimits, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, CategoryTheory.Abelian.extFunctor_obj, Colimits.quotToQuotUlift_Κ, ModuleCat.smulNatTrans_apply_app, CategoryTheory.Abelian.extFunctor_map_app, zero_apply, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, CategoryTheory.Abelian.Ext.covariantSequence_exact, id_apply, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, PresheafOfModules.unitHomEquiv_apply_coe, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, int_hom_ext_iff, Colimits.Quot.desc_toCocone_desc_app, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, CategoryTheory.preservesLimits_preadditiveYoneda_obj, PresheafOfModules.Sheafify.smul_add, Îź_forget_apply, CategoryTheory.additive_coyonedaObj', AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, epi_iff_surjective, PresheafOfModules.freeAdjunctionUnit_app, PresheafOfModules.presheaf_obj_coe, tensorObj_eq, AlgebraicGeometry.Scheme.Modules.Hom.id_app, forgetâ_addGrp_map_ofHom, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, CategoryTheory.full_preadditiveCoyoneda, FGModuleCat.instFiniteCarrierColimitModuleCatCompForgetâLinearMapIdObjIsFG, CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, forgetâAddCommMon_preservesLimitsOfShape, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, CategoryTheory.ShortComplex.abLeftHomologyData_f', AlgebraicGeometry.Scheme.Modules.Hom.comp_app, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, coyonedaType_obj_map, PresheafOfModules.toPresheaf_map_app_apply, coyonedaType_obj_obj_coe, mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, Colimits.toCocone_Κ_app, Colimits.Quot.Κ_desc, ModuleCat.FilteredColimits.forgetâAddCommGroup_preservesFilteredColimits, Colimits.Quot.map_Κ, PresheafOfModules.instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, isZero_of_subsingleton, kernelIsoKer_inv_comp_Κ, image.fac, HasLimit.productLimitCone_cone_Ď, ModuleCat.forgetâ_obj_moduleCat_of, forgetâAddGroup_preservesLimit, injective_of_mono, CategoryTheory.ShortComplex.ShortExact.injective_f, epi_iff_range_eq_top, SheafOfModules.Presentation.map_relations_I, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, CategoryTheory.Abelian.Ext.mono_postcomp_mkâ_of_mono, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, PresheafOfModules.Elements.fromFreeYoneda_app_apply, ModuleCat.HasColimit.coconePointSMul_apply, SheafOfModules.ΚFree_mapFree_inv, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, SheafOfModules.Presentation.mapRelations_mapGenerators, CategoryTheory.ShortComplex.ab_exact_iff, leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux, coe_id, forgetâAddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, enoughInjectives, CategoryTheory.ShortComplex.ShortExact.surjective_g, CategoryTheory.ShortComplex.zero_apply, Colimits.toCocone_pt_coe, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, uliftFunctor_preservesLimitsOfShape, CategoryTheory.ShortComplex.abLeftHomologyData_i, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, ofHom_id, injective_as_module_iff, AlgebraicGeometry.Scheme.Modules.restrict_obj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, ModuleCat.mkOfSMul_smul, instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.sectionsMk_coe, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, biprodIsoProd_inv_comp_desc, uliftFunctor_map, AlgebraicGeometry.Scheme.Modules.Hom.add_app, biprodIsoProd_inv_comp_snd, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎUnitOpensCarrierCarrierCommRingCatRingCatSheaf, PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits, CategoryTheory.full_preadditiveYoneda, CategoryTheory.Abelian.Ext.mono_precomp_mkâ_of_epi, SheafOfModules.Presentation.of_isIso_relations, hom_comp, uliftFunctor_obj, uliftFunctor_preservesLimit, ModuleCat.reflectsColimitsOfShape, PresheafOfModules.toPresheaf_preservesColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimitOfSize, biprodIsoProd_inv_comp_desc_apply, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkâ, CochainComplex.HomComplex.leftHomologyData_H_coe, CochainComplex.HomComplex.leftHomologyData'_K_coe, ofHom_apply, hasColimitsOfShape, biprodIsoProd_inv_comp_fst_apply, instPreservesHomologyFunctorAddCommGrpCatColim, SheafOfModules.Presentation.of_isIso_generators, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, instIsLeftAdjointFree, SheafOfModules.map_ΚFree_mapFree_hom, biproductIsoPi_inv_comp_Ď, instIsSerreClassIsFinite, commGroupAddCommGroupEquivalence_unitIso, CategoryTheory.ShortComplex.ab_zero_apply, wellPowered_addCommGrp, HasLimit.lift_hom_apply, hasColimitsOfSize, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forgetâ_addCommGrp_additive, biprodIsoProd_inv_comp_fst, RingCat.forgetâAddCommGroup_preservesLimitsOfSize, CochainComplex.HomComplex_X, CochainComplex.HomComplex.leftHomologyData'_H_coe, forgetâ_commMonCat_map_ofHom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, forgetâAddCommMon_preservesLimitsOfSize, coyoneda_map_app, Colimits.Quot.desc_quotQuotUliftAddEquiv, forget_map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, ModuleCat.forgetâ_reflectsLimits, kernelIsoKer_hom_comp_subtype, ModuleCat.forgetâPreservesColimitsOfShape, CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda, instFullUliftFunctor, CochainComplex.HomComplex.leftHomologyData'_Ď, ModuleCat.forgetâAddCommGroup_reflectsLimit, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, PresheafOfModules.freeAdjunction_unit_app, SheafOfModules.Presentation.map_generators_I, ModuleCat.forgetâAddCommGroup_preservesLimit, PresheafOfModules.Sheafify.zero_smul, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', instAB5AddCommGrpCat, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, PresheafOfModules.toPresheaf_preservesColimitsOfSize, SheafOfModules.map_ΚFree_mapFree_hom_assoc, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, CategoryTheory.whiskering_linearYonedaâ, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, PresheafOfModules.sections_ext_iff, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, hom_neg_apply, CommGrpCat.toAddCommGrp_obj_coe, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, ModuleCat.HasColimit.reflectsColimit, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, hom_add_apply, ofHom_injective, SheafOfModules.pushforwardSections_coe, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.Sheafify.map_smul, PresheafOfModules.germ_smul, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, PresheafOfModules.toSheafify_app_apply, instIsRightAdjointForgetAddMonoidHomCarrier, forget_isCorepresentable, binaryProductLimitCone_cone_Ď_app_right, CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, PresheafOfModules.freeAdjunction_homEquiv, ModuleCat.forgetâAddCommGroupIsEquivalence, instPreservesColimitsOfSizeUliftFunctor, mono_iff_ker_eq_bot, CategoryTheory.preadditiveCoyoneda_obj, instHasExactLimitsOfShapeDiscreteAddCommGrpCat, AlgebraicGeometry.Scheme.Modules.inv_app, AddEquiv.toAddCommGrpIso_inv, hom_neg, PresheafOfModules.freeObjDesc_app, CommGrpCat.toAddCommGrp_map, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎFreeOpensCarrierCarrierCommRingCat, PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf, CategoryTheory.ShortComplex.exact_iff_exact_map_forgetâ, homAddEquiv_apply, CategoryTheory.Abelian.Ext.contravariantSequence_exact, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForgetâLinearMapIdCarrierAddMonoidHomCarrier, SheafOfModules.Presentation.map_Ď_eq, coyonedaType_map_app, commGroupAddCommGroupEquivalence_inverse, hasColimit_iff_small_quot, toCommGrp_map, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, instHasBinaryBiproducts, CochainComplex.HomComplex_d_hom_apply, AlgebraicGeometry.Scheme.Modules.map_smul, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, hasLimit_iff_small_sections, hom_zsmul, forget_preservesLimitsOfSize, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forgetâ_map, coyoneda_obj_map, forget_reflects_isos
|
instCoeAddGrpCat đ | CompOp | â |
instCoeCommMonCat đ | CompOp | â |
instCoeSortType đ | CompOp | â |
instConcreteCategoryAddMonoidHomCarrier đ | CompOp | 145 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, forgetâAddGroup_preservesLimitsOfShape, ModuleCat.forgetâ_reflectsLimitsOfSize, biproductIsoPi_inv_comp_Ď_apply, comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForgetâRingHomCarrierAddMonoidHomCarrier, ModuleCat.forgetâPreservesColimitsOfSize, FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forgetâAddCommGroup_preservesLimitsOfSize, ModuleCat.mkOfSMul'_smul, CategoryTheory.ShortComplex.ShortExact.ab_surjective_g, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, PresheafOfModules.sections_property, RingCat.forgetâAddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', ModuleCat.forgetâ_addCommGrp_essSurj, neg_hom_apply, forget_preservesLimits, ModuleCat.forgetâAddCommGroup_reflectsLimitOfShape, forget_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, coe_comp, forgetâ_map, ModuleCat.HasColimit.colimitCocone_Κ_app, ModuleCat.forgetâ_addCommGroup_full, PresheafOfModules.sectionsMap_coe, FilteredColimits.forgetâAddGroup_preservesFilteredColimits, CategoryTheory.ShortComplex.abToCycles_apply_coe, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, ModuleCat.HasColimit.colimitCocone_pt_isModule, CategoryTheory.preadditiveYoneda_obj, ext_iff, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, forget_commGrp_preserves_epi, coyonedaForget_inv_app_app, free_map_coe, CategoryTheory.ShortComplex.ShortExact.ab_injective_f, coyonedaForget_hom_app_app_hom, biprodIsoProd_inv_comp_snd_apply, CategoryTheory.ShortComplex.exact_iff_of_hasForget, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, ModuleCat.forgetâAddCommGroup_preservesLimits, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mkâ_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, ModuleCat.forgetâ_obj, forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyonedaâ, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Preadditive.epi_iff_surjective, CategoryTheory.Preadditive.mono_iff_injective, CategoryTheory.whiskering_preadditiveYoneda, forgetâAddGroup_preservesLimits, ModuleCat.smulNatTrans_apply_app, zero_apply, id_apply, PresheafOfModules.unitHomEquiv_apply_coe, int_hom_ext_iff, Colimits.Quot.desc_toCocone_desc_app, Îź_forget_apply, epi_iff_surjective, PresheafOfModules.freeAdjunctionUnit_app, forgetâ_addGrp_map_ofHom, FGModuleCat.instFiniteCarrierColimitModuleCatCompForgetâLinearMapIdObjIsFG, forgetâAddCommMon_preservesLimitsOfShape, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, Colimits.Quot.Κ_desc, ModuleCat.FilteredColimits.forgetâAddCommGroup_preservesFilteredColimits, Colimits.Quot.map_Κ, kernelIsoKer_inv_comp_Κ, ModuleCat.forgetâ_obj_moduleCat_of, forgetâAddGroup_preservesLimit, injective_of_mono, CategoryTheory.ShortComplex.ShortExact.injective_f, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.Elements.fromFreeYoneda_app_apply, ModuleCat.HasColimit.coconePointSMul_apply, CategoryTheory.ShortComplex.ab_exact_iff, coe_id, forgetâAddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.ShortComplex.ShortExact.surjective_g, CategoryTheory.ShortComplex.zero_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, ModuleCat.mkOfSMul_smul, instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.sectionsMk_coe, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎUnitOpensCarrierCarrierCommRingCatRingCatSheaf, ModuleCat.reflectsColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimitOfSize, biprodIsoProd_inv_comp_desc_apply, ofHom_apply, biprodIsoProd_inv_comp_fst_apply, CategoryTheory.ShortComplex.ab_zero_apply, HasLimit.lift_hom_apply, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forgetâ_addCommGrp_additive, RingCat.forgetâAddCommGroup_preservesLimitsOfSize, forgetâ_commMonCat_map_ofHom, forgetâAddCommMon_preservesLimitsOfSize, forget_map, ModuleCat.forgetâ_reflectsLimits, kernelIsoKer_hom_comp_subtype, ModuleCat.forgetâPreservesColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimit, PresheafOfModules.freeAdjunction_unit_app, ModuleCat.forgetâAddCommGroup_preservesLimit, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.whiskering_linearYonedaâ, PresheafOfModules.sections_ext_iff, hom_neg_apply, PresheafOfModules.germ_ringCat_smul, ModuleCat.HasColimit.reflectsColimit, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, hom_add_apply, SheafOfModules.pushforwardSections_coe, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.Sheafify.map_smul, PresheafOfModules.germ_smul, PresheafOfModules.toSheafify_app_apply, instIsRightAdjointForgetAddMonoidHomCarrier, forget_isCorepresentable, PresheafOfModules.freeAdjunction_homEquiv, ModuleCat.forgetâAddCommGroupIsEquivalence, CategoryTheory.preadditiveCoyoneda_obj, PresheafOfModules.freeObjDesc_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎFreeOpensCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.exact_iff_exact_map_forgetâ, homAddEquiv_apply, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, AlgebraicGeometry.Scheme.Modules.map_smul, hasLimit_iff_small_sections, forget_preservesLimitsOfSize, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forgetâ_map, forget_reflects_isos
|
instInhabited đ | CompOp | â |
instZeroHom đ | CompOp | 1 mathmath: zero_apply
|
of đ | CompOp | 54 mathmath: binaryProductLimitCone_cone_pt, biproductIsoPi_inv_comp_Ď_apply, asHom_hom_apply, ofHom_comp, injective_of_divisible, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', coe_of, hom_ofHom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Colimits.colimitCocone_Κ_app, CochainComplex.HomComplex.leftHomologyData_Ď_hom_apply, asHom_injective, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', CochainComplex.HomComplex.leftHomologyData_i_hom_apply, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', biprodIsoProd_inv_comp_snd_apply, binaryProductLimitCone_isLimit_lift, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mkâ_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, ModuleCat.forgetâ_obj, Colimits.colimitCocone_pt, int_hom_ext_iff, tensorObj_eq, forgetâ_addGrp_map_ofHom, Colimits.toCocone_Κ_app, kernelIsoKer_inv_comp_Κ, HasLimit.productLimitCone_cone_Ď, ModuleCat.forgetâ_obj_moduleCat_of, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', CategoryTheory.Abelian.Ext.mono_postcomp_mkâ_of_mono, ofHom_id, injective_as_module_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, biprodIsoProd_inv_comp_desc, biprodIsoProd_inv_comp_snd, CategoryTheory.Abelian.Ext.mono_precomp_mkâ_of_epi, uliftFunctor_obj, biprodIsoProd_inv_comp_desc_apply, ofHom_apply, biprodIsoProd_inv_comp_fst_apply, biproductIsoPi_inv_comp_Ď, HasLimit.lift_hom_apply, biprodIsoProd_inv_comp_fst, CochainComplex.HomComplex_X, forgetâ_commMonCat_map_ofHom, coyoneda_map_app, kernelIsoKer_hom_comp_subtype, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', ofHom_injective, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, coyonedaType_map_app, CochainComplex.HomComplex_d_hom_apply, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles
|
ofHom đ | CompOp | 46 mathmath: ofHom_comp, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', CochainComplex.HomComplex.leftHomologyData'_i, hom_ofHom, Colimits.colimitCocone_Κ_app, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', CategoryTheory.Abelian.extFunctorObj_map, CategoryTheory.preadditiveYonedaMap_app, CategoryTheory.ShortComplex.abLeftHomologyData_Ď, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', binaryProductLimitCone_isLimit_lift, binaryProductLimitCone_cone_Ď_app_left, AddEquiv.toAddCommGrpIso_hom, CategoryTheory.Abelian.extFunctor_map_app, forgetâ_addGrp_map_ofHom, CategoryTheory.ShortComplex.abLeftHomologyData_f', coyonedaType_obj_map, Colimits.toCocone_Κ_app, kernelIsoKer_inv_comp_Κ, HasLimit.productLimitCone_cone_Ď, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', CategoryTheory.Abelian.Ext.mono_postcomp_mkâ_of_mono, CategoryTheory.ShortComplex.abLeftHomologyData_i, ofHom_id, biprodIsoProd_inv_comp_desc, uliftFunctor_map, biprodIsoProd_inv_comp_snd, CategoryTheory.Abelian.Ext.mono_precomp_mkâ_of_epi, ofHom_apply, biproductIsoPi_inv_comp_Ď, biprodIsoProd_inv_comp_fst, ofHom_hom, forgetâ_commMonCat_map_ofHom, coyoneda_map_app, kernelIsoKer_hom_comp_subtype, CochainComplex.HomComplex.leftHomologyData'_Ď, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', ofHom_injective, binaryProductLimitCone_cone_Ď_app_right, AddEquiv.toAddCommGrpIso_inv, CommGrpCat.toAddCommGrp_map, coyonedaType_map_app, ModuleCat.forgetâ_map, coyoneda_obj_map
|
str đ | CompOp | 211 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, forgetâAddGroup_preservesLimitsOfShape, coyoneda_obj_obj_coe, binaryProductLimitCone_cone_pt, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, ModuleCat.forgetâ_reflectsLimitsOfSize, biproductIsoPi_inv_comp_Ď_apply, comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForgetâRingHomCarrierAddMonoidHomCarrier, ModuleCat.forgetâPreservesColimitsOfSize, hom_add, asHom_hom_apply, FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forgetâAddCommGroup_preservesLimitsOfSize, ModuleCat.mkOfSMul'_smul, PresheafOfModules.Sheafify.add_smul, CategoryTheory.ShortComplex.ShortExact.ab_surjective_g, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, hom_zero, PresheafOfModules.sections_property, RingCat.forgetâAddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', isColimit_iff_bijective_desc, ModuleCat.forgetâ_addCommGrp_essSurj, neg_hom_apply, forget_preservesLimits, ModuleCat.forgetâAddCommGroup_reflectsLimitOfShape, forget_preservesLimitsOfShape, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, ModuleCat.FilteredColimits.colimit_zero_eq, coe_comp, forgetâ_map, ModuleCat.HasColimit.colimitCocone_Κ_app, Colimits.colimitCocone_Κ_app, ModuleCat.forgetâ_addCommGroup_full, PresheafOfModules.sectionsMap_coe, FilteredColimits.forgetâAddGroup_preservesFilteredColimits, CategoryTheory.ShortComplex.abToCycles_apply_coe, CategoryTheory.ShortComplex.Exact.ab_range_eq_ker, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, ModuleCat.HasColimit.colimitCocone_pt_isModule, CategoryTheory.preadditiveYoneda_obj, ext_iff, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, forget_commGrp_preserves_epi, coyonedaForget_inv_app_app, free_map_coe, CategoryTheory.ShortComplex.ShortExact.ab_injective_f, CategoryTheory.ShortComplex.abLeftHomologyData_Ď, coyonedaForget_hom_app_app_hom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, HasLimit.productLimitCone_isLimit_lift, CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, biprodIsoProd_inv_comp_snd_apply, CategoryTheory.ShortComplex.exact_iff_of_hasForget, binaryProductLimitCone_isLimit_lift, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, binaryProductLimitCone_cone_Ď_app_left, homAddEquiv_symm_apply_hom, hom_sub, ModuleCat.forgetâAddCommGroup_preservesLimits, Colimits.quotUliftToQuot_Κ, PresheafOfModules.presheaf_map_apply_coe, hom_id, hom_nsmul, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mkâ_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, ModuleCat.forgetâ_obj, range_eq_top_of_epi, forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyonedaâ, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, Colimits.Quot.desc_toCocone_desc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Preadditive.epi_iff_surjective, AddEquiv.toAddCommGrpIso_hom, CategoryTheory.Preadditive.mono_iff_injective, CategoryTheory.whiskering_preadditiveYoneda, forgetâAddGroup_preservesLimits, Colimits.quotToQuotUlift_Κ, ModuleCat.smulNatTrans_apply_app, zero_apply, id_apply, PresheafOfModules.unitHomEquiv_apply_coe, int_hom_ext_iff, Colimits.Quot.desc_toCocone_desc_app, PresheafOfModules.Sheafify.smul_add, Îź_forget_apply, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, epi_iff_surjective, PresheafOfModules.freeAdjunctionUnit_app, tensorObj_eq, forgetâ_addGrp_map_ofHom, FGModuleCat.instFiniteCarrierColimitModuleCatCompForgetâLinearMapIdObjIsFG, CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, forgetâAddCommMon_preservesLimitsOfShape, CategoryTheory.ShortComplex.abLeftHomologyData_f', CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, coyonedaType_obj_map, PresheafOfModules.toPresheaf_map_app_apply, mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, Colimits.toCocone_Κ_app, Colimits.Quot.Κ_desc, ModuleCat.FilteredColimits.forgetâAddCommGroup_preservesFilteredColimits, Colimits.Quot.map_Κ, ModuleCat.FilteredColimits.colimit_add_mk_eq', kernelIsoKer_inv_comp_Κ, HasLimit.productLimitCone_cone_Ď, ModuleCat.forgetâ_obj_moduleCat_of, forgetâAddGroup_preservesLimit, injective_of_mono, CategoryTheory.ShortComplex.ShortExact.injective_f, epi_iff_range_eq_top, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.Elements.fromFreeYoneda_app_apply, ModuleCat.HasColimit.coconePointSMul_apply, CategoryTheory.ShortComplex.ab_exact_iff, coe_id, forgetâAddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.ShortComplex.ShortExact.surjective_g, CategoryTheory.ShortComplex.zero_apply, CategoryTheory.ShortComplex.abLeftHomologyData_i, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, ModuleCat.mkOfSMul_smul, instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, PresheafOfModules.sectionsMk_coe, biprodIsoProd_inv_comp_desc, uliftFunctor_map, biprodIsoProd_inv_comp_snd, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎUnitOpensCarrierCarrierCommRingCatRingCatSheaf, hom_comp, uliftFunctor_obj, ModuleCat.reflectsColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimitOfSize, biprodIsoProd_inv_comp_desc_apply, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkâ, ofHom_apply, biprodIsoProd_inv_comp_fst_apply, biproductIsoPi_inv_comp_Ď, CategoryTheory.ShortComplex.ab_zero_apply, HasLimit.lift_hom_apply, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forgetâ_addCommGrp_additive, biprodIsoProd_inv_comp_fst, RingCat.forgetâAddCommGroup_preservesLimitsOfSize, ofHom_hom, forgetâ_commMonCat_map_ofHom, forgetâAddCommMon_preservesLimitsOfSize, coyoneda_map_app, Colimits.Quot.desc_quotQuotUliftAddEquiv, forget_map, ModuleCat.forgetâ_reflectsLimits, kernelIsoKer_hom_comp_subtype, ModuleCat.forgetâPreservesColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimit, PresheafOfModules.freeAdjunction_unit_app, ModuleCat.forgetâAddCommGroup_preservesLimit, PresheafOfModules.Sheafify.zero_smul, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, CategoryTheory.whiskering_linearYonedaâ, PresheafOfModules.sections_ext_iff, hom_neg_apply, PresheafOfModules.germ_ringCat_smul, ModuleCat.HasColimit.reflectsColimit, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, hom_add_apply, SheafOfModules.pushforwardSections_coe, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.Sheafify.map_smul, PresheafOfModules.germ_smul, PresheafOfModules.toSheafify_app_apply, instIsRightAdjointForgetAddMonoidHomCarrier, forget_isCorepresentable, binaryProductLimitCone_cone_Ď_app_right, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, ker_eq_bot_of_mono, PresheafOfModules.freeAdjunction_homEquiv, ModuleCat.forgetâAddCommGroupIsEquivalence, mono_iff_ker_eq_bot, CategoryTheory.preadditiveCoyoneda_obj, AddEquiv.toAddCommGrpIso_inv, hom_neg, PresheafOfModules.freeObjDesc_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎFreeOpensCarrierCarrierCommRingCat, CategoryTheory.ShortComplex.exact_iff_exact_map_forgetâ, homAddEquiv_apply, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, coyonedaType_map_app, ModuleCat.FilteredColimits.colimit_add_mk_eq, toCommGrp_map, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, AlgebraicGeometry.Scheme.Modules.map_smul, hasLimit_iff_small_sections, hom_zsmul, forget_preservesLimitsOfSize, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forgetâ_map, coyoneda_obj_map, forget_reflects_isos
|
uliftFunctor đ | CompOp | 14 mathmath: uliftFunctor_additive, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, instFaithfulUliftFunctor, Colimits.quotUliftToQuot_Κ, uliftFunctor_preservesLimitsOfSize, Colimits.quotToQuotUlift_Κ, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, uliftFunctor_preservesLimitsOfShape, uliftFunctor_map, uliftFunctor_obj, uliftFunctor_preservesLimit, Colimits.Quot.desc_quotQuotUliftAddEquiv, instFullUliftFunctor, instPreservesColimitsOfSizeUliftFunctor
|
| Name | Category | Theorems |
|---|
carrier đ | CompOp | 63 mathmath: AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, forget_grp_preserves_epi, FiniteAddGrp.instFiniteCarrierToAddGrp, uliftFunctor_obj, forgetâ_map, id_apply, forget_preservesLimits, toGrp_obj_coe, tensorObj_eq, uliftFunctor_map, forget_grp_preserves_mono, AddCommGrpCat.forgetâ_map, hom_comp, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, FilteredColimits.colimit_add_mk_eq, FilteredColimits.colimit_neg_mk_eq, forgetâAddMonPreservesLimitsOfSize, isZero_iff_subsingleton, FilteredColimits.forget_preservesFilteredColimits, zero_apply, AddEquiv.toAddGrpIso_hom, forget_preservesLimitsOfShape, binaryProductLimitCone_isLimit_lift, ext_iff, FiniteAddGrp.ofHom_apply, AddCommGrpCat.forgetâAddGroup_preservesLimits, toGrp_map, hasLimit_iff_small_sections, mono_iff_injective, forgetâ_map_ofHom, AddCommGrpCat.forgetâ_addGrp_map_ofHom, forget_reflects_isos, Îź_forget_apply, AddCommGrpCat.forgetâAddGroup_preservesLimit, FilteredColimits.colimit_add_mk_eq', AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddEquiv.toAddGrpIso_inv, FiniteAddGrp.isFinite, neg_hom_apply, hom_neg_apply, subsingleton_of_isZero, forget_preservesLimitsOfSize, coe_of, comp_apply, FilteredColimits.forgetâAddMon_preservesFilteredColimits, ofHom_hom, epi_iff_range_eq_top, epi_iff_surjective, GrpCat.toAddGrp_obj_coe, coe_comp, FilteredColimits.colimit_zero_eq, ker_eq_bot_of_mono, forget_isCorepresentable, instFullMonCatForgetâAddMonoidHomCarrierCarrier, binaryProductLimitCone_cone_pt, hom_id, ofHom_apply, mono_iff_ker_eq_bot, coe_id, forgetâMon_preservesLimits
|
fullyFaihtfulForgetâToAddMonCat đ | CompOp | â |
hasForgetToAddMonCat đ | CompOp | 7 mathmath: forgetâ_map, forgetâAddMonPreservesLimitsOfSize, forgetâ_map_ofHom, instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, FilteredColimits.forgetâAddMon_preservesFilteredColimits, instFullMonCatForgetâAddMonoidHomCarrierCarrier, forgetâMon_preservesLimits
|
instCategory đ | CompOp | 75 mathmath: AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, hasLimits, forget_grp_preserves_epi, hasLimitsOfShape, uliftFunctor_obj, forgetâ_map, id_apply, hasLimitsOfSize, uliftFunctor_preservesLimit, forget_preservesLimits, toGrp_obj_coe, tensorObj_eq, uliftFunctor_map, forget_grp_preserves_mono, AddCommGrpCat.forgetâ_map, hom_comp, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, FilteredColimits.colimit_add_mk_eq, FilteredColimits.colimit_neg_mk_eq, GrpCat.toAddGrp_map, forgetâAddMonPreservesLimitsOfSize, isZero_iff_subsingleton, FilteredColimits.forget_preservesFilteredColimits, zero_apply, AddEquiv.toAddGrpIso_hom, uliftFunctor_preservesLimitsOfShape, forget_preservesLimitsOfShape, binaryProductLimitCone_isLimit_lift, ext_iff, AddCommGrpCat.forgetâAddGroup_preservesLimits, ofHom_injective, toGrp_map, hasLimit_iff_small_sections, mono_iff_injective, uliftFunctor_preservesLimitsOfSize, forgetâ_map_ofHom, groupAddGroupEquivalence_inverse, AddCommGrpCat.forgetâ_addGrp_map_ofHom, isZero_of_subsingleton, forget_reflects_isos, Îź_forget_apply, AddCommGrpCat.forgetâAddGroup_preservesLimit, FilteredColimits.colimit_add_mk_eq', groupAddGroupEquivalence_functor, AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, ofHom_comp, hasZeroObject, instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddEquiv.toAddGrpIso_inv, neg_hom_apply, hom_neg_apply, groupAddGroupEquivalence_unitIso, forget_preservesLimitsOfSize, instFaithfulUliftFunctor, groupAddGroupEquivalence_counitIso, comp_apply, FilteredColimits.forgetâAddMon_preservesFilteredColimits, epi_iff_range_eq_top, epi_iff_surjective, GrpCat.toAddGrp_obj_coe, coe_comp, hasLimit, FilteredColimits.colimit_zero_eq, forget_isCorepresentable, instFullUliftFunctor, ofHom_id, instFullMonCatForgetâAddMonoidHomCarrierCarrier, binaryProductLimitCone_cone_pt, hom_id, ofHom_apply, mono_iff_ker_eq_bot, coe_id, forgetâMon_preservesLimits
|
instCoeMonCat đ | CompOp | â |
instCoeSortType đ | CompOp | â |
instConcreteCategoryAddMonoidHomCarrier đ | CompOp | 38 mathmath: AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, forget_grp_preserves_epi, forgetâ_map, id_apply, forget_preservesLimits, forget_grp_preserves_mono, AddCommGrpCat.forgetâ_map, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, FilteredColimits.colimit_add_mk_eq, forgetâAddMonPreservesLimitsOfSize, FilteredColimits.forget_preservesFilteredColimits, zero_apply, forget_preservesLimitsOfShape, ext_iff, AddCommGrpCat.forgetâAddGroup_preservesLimits, hasLimit_iff_small_sections, mono_iff_injective, forgetâ_map_ofHom, AddCommGrpCat.forgetâ_addGrp_map_ofHom, forget_reflects_isos, Îź_forget_apply, AddCommGrpCat.forgetâAddGroup_preservesLimit, AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, neg_hom_apply, hom_neg_apply, forget_preservesLimitsOfSize, comp_apply, FilteredColimits.forgetâAddMon_preservesFilteredColimits, epi_iff_surjective, coe_comp, forget_isCorepresentable, instFullMonCatForgetâAddMonoidHomCarrierCarrier, ofHom_apply, coe_id, forgetâMon_preservesLimits
|
instInhabited đ | CompOp | â |
instZeroHom đ | CompOp | 1 mathmath: zero_apply
|
of đ | CompOp | 11 mathmath: uliftFunctor_obj, tensorObj_eq, binaryProductLimitCone_isLimit_lift, ofHom_injective, forgetâ_map_ofHom, hom_ofHom, ofHom_comp, coe_of, ofHom_id, binaryProductLimitCone_cone_pt, ofHom_apply
|
ofHom đ | CompOp | 13 mathmath: uliftFunctor_map, GrpCat.toAddGrp_map, AddEquiv.toAddGrpIso_hom, binaryProductLimitCone_isLimit_lift, ofHom_injective, forgetâ_map_ofHom, AddCommGrpCat.forgetâ_addGrp_map_ofHom, hom_ofHom, ofHom_comp, AddEquiv.toAddGrpIso_inv, ofHom_hom, ofHom_id, ofHom_apply
|
str đ | CompOp | 56 mathmath: AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, forget_grp_preserves_epi, uliftFunctor_obj, forgetâ_map, id_apply, forget_preservesLimits, tensorObj_eq, uliftFunctor_map, forget_grp_preserves_mono, AddCommGrpCat.forgetâ_map, hom_comp, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, FilteredColimits.colimit_add_mk_eq, FilteredColimits.colimit_neg_mk_eq, forgetâAddMonPreservesLimitsOfSize, FilteredColimits.forget_preservesFilteredColimits, zero_apply, AddEquiv.toAddGrpIso_hom, forget_preservesLimitsOfShape, binaryProductLimitCone_isLimit_lift, ext_iff, FiniteAddGrp.ofHom_apply, AddCommGrpCat.forgetâAddGroup_preservesLimits, toGrp_map, hasLimit_iff_small_sections, mono_iff_injective, forgetâ_map_ofHom, AddCommGrpCat.forgetâ_addGrp_map_ofHom, forget_reflects_isos, Îź_forget_apply, AddCommGrpCat.forgetâAddGroup_preservesLimit, FilteredColimits.colimit_add_mk_eq', AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddEquiv.toAddGrpIso_inv, neg_hom_apply, hom_neg_apply, forget_preservesLimitsOfSize, comp_apply, FilteredColimits.forgetâAddMon_preservesFilteredColimits, ofHom_hom, epi_iff_range_eq_top, epi_iff_surjective, coe_comp, FilteredColimits.colimit_zero_eq, ker_eq_bot_of_mono, forget_isCorepresentable, instFullMonCatForgetâAddMonoidHomCarrierCarrier, binaryProductLimitCone_cone_pt, hom_id, ofHom_apply, mono_iff_ker_eq_bot, coe_id, forgetâMon_preservesLimits
|
uliftFunctor đ | CompOp | 7 mathmath: uliftFunctor_obj, uliftFunctor_preservesLimit, uliftFunctor_map, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimitsOfSize, instFaithfulUliftFunctor, instFullUliftFunctor
|
| Name | Category | Theorems |
|---|
carrier đ | CompOp | 68 mathmath: uliftFunctor_map, coe_of, forgetâCommMon_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, epi_iff_surjective, hasLimit_iff_small_sections, forget_map, forget_preservesLimits, uliftFunctor_obj, FilteredColimits.forgetâGroup_preservesFilteredColimits, ext_iff, isZero_iff_subsingleton, coe_comp, forgetâGroup_preservesLimit, hom_inv_apply, FilteredColimits.forget_preservesFilteredColimits, Îź_forget_apply, subsingleton_of_isZero, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, hom_id, forgetâCommMon_preservesLimitsOfSize, forget_commGrp_preserves_mono, forgetâGroup_preservesLimits, coyonedaType_map_app, instFullGrpCatForgetâMonoidHomCarrierCarrier, AddCommGrpCat.toCommGrp_obj_coe, mono_iff_injective, forget_isCorepresentable, ofHom_apply, MulEquiv.toCommGrpIso_inv, forget_reflects_isos, range_eq_top_of_epi, inv_hom_apply, hom_comp, tensorObj_eq, coe_id, id_apply, mono_iff_ker_eq_bot, comp_apply, coyonedaForget_hom_app_app_hom, binaryProductLimitCone_cone_pt, CategoryTheory.yonedaCommGrpGrpObj_obj_coe, forgetâGroup_preservesLimitsOfSize, coyoneda_obj_obj_coe, CommMonCat.units_obj_coe, forget_commGrp_preserves_epi, ker_eq_bot_of_mono, coyonedaForget_inv_app_app, MulEquiv.toCommGrpIso_hom, one_apply, coyonedaType_obj_map, instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, binaryProductLimitCone_isLimit_lift, forget_preservesLimitsOfSize, forgetâ_grp_map_ofHom, coyoneda_obj_map, forgetâ_commMonCat_map_ofHom, toAddCommGrp_obj_coe, epi_iff_range_eq_top, coyoneda_map_app, ofHom_hom, forgetâGroup_preservesLimitsOfShape, forgetâ_map, coyonedaType_obj_obj_coe, toAddCommGrp_map, forget_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply
|
fullyFaithfulForgetâToGrp đ | CompOp | â |
hasForgetToCommMonCat đ | CompOp | 3 mathmath: forgetâCommMon_preservesLimitsOfShape, forgetâCommMon_preservesLimitsOfSize, forgetâ_commMonCat_map_ofHom
|
hasForgetToGroup đ | CompOp | 9 mathmath: FilteredColimits.forgetâGroup_preservesFilteredColimits, forgetâGroup_preservesLimit, forgetâGroup_preservesLimits, instFullGrpCatForgetâMonoidHomCarrierCarrier, forgetâGroup_preservesLimitsOfSize, instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, forgetâ_grp_map_ofHom, forgetâGroup_preservesLimitsOfShape, forgetâ_map
|
instCategory đ | CompOp | 91 mathmath: uliftFunctor_map, commGroupAddCommGroupEquivalence_functor, uliftFunctor_preservesLimitsOfSize, forgetâCommMon_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, CategoryTheory.yonedaCommGrpGrpObj_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, epi_iff_surjective, hasLimit_iff_small_sections, forget_map, forget_preservesLimits, isZero_of_subsingleton, uliftFunctor_obj, commGroupAddCommGroupEquivalence_counitIso, FilteredColimits.forgetâGroup_preservesFilteredColimits, ext_iff, isZero_iff_subsingleton, coe_comp, forgetâGroup_preservesLimit, hom_inv_apply, instFaithfulUliftFunctor, uliftFunctor_preservesLimit, FilteredColimits.forget_preservesFilteredColimits, hasLimits, Îź_forget_apply, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, hom_id, forgetâCommMon_preservesLimitsOfSize, forget_commGrp_preserves_mono, forgetâGroup_preservesLimits, coyonedaType_map_app, instFullGrpCatForgetâMonoidHomCarrierCarrier, AddCommGrpCat.toCommGrp_obj_coe, CommMonCat.val_units_map_hom_apply, CommMonCat.val_inv_units_map_hom_apply, mono_iff_injective, forget_isCorepresentable, instFullUliftFunctor, ofHom_apply, MulEquiv.toCommGrpIso_inv, uliftFunctor_preservesLimitsOfShape, forget_reflects_isos, inv_hom_apply, CategoryTheory.yonedaCommGrpGrp_obj, hom_comp, tensorObj_eq, coe_id, id_apply, mono_iff_ker_eq_bot, comp_apply, coyonedaForget_hom_app_app_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, binaryProductLimitCone_cone_pt, CategoryTheory.yonedaCommGrpGrpObj_obj_coe, forgetâGroup_preservesLimitsOfSize, coyoneda_obj_obj_coe, instIsRightAdjointCommGrpCatCommMonCatUnits, CommMonCat.units_obj_coe, commGroupAddCommGroupEquivalence_unitIso, enoughInjectives, forget_commGrp_preserves_epi, CategoryTheory.yonedaCommGrpGrp_map_app, coyonedaForget_inv_app_app, MulEquiv.toCommGrpIso_hom, one_apply, ofHom_id, ofHom_comp, hasLimitsOfSize, coyonedaType_obj_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, binaryProductLimitCone_isLimit_lift, forget_preservesLimitsOfSize, forgetâ_grp_map_ofHom, coyoneda_obj_map, forgetâ_commMonCat_map_ofHom, hasLimit, toAddCommGrp_obj_coe, instHasZeroObject, epi_iff_range_eq_top, coyoneda_map_app, ofHom_injective, forgetâGroup_preservesLimitsOfShape, forgetâ_map, coyonedaType_obj_obj_coe, toAddCommGrp_map, commGroupAddCommGroupEquivalence_inverse, AddCommGrpCat.toCommGrp_map, forget_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply, hasLimitsOfShape
|
instCoeCommMonCat đ | CompOp | â |
instCoeGrpCat đ | CompOp | â |
instCoeSortType đ | CompOp | â |
instConcreteCategoryMonoidHomCarrier đ | CompOp | 36 mathmath: forgetâCommMon_preservesLimitsOfShape, epi_iff_surjective, hasLimit_iff_small_sections, forget_map, forget_preservesLimits, FilteredColimits.forgetâGroup_preservesFilteredColimits, ext_iff, coe_comp, forgetâGroup_preservesLimit, hom_inv_apply, FilteredColimits.forget_preservesFilteredColimits, Îź_forget_apply, forgetâCommMon_preservesLimitsOfSize, forget_commGrp_preserves_mono, forgetâGroup_preservesLimits, instFullGrpCatForgetâMonoidHomCarrierCarrier, mono_iff_injective, forget_isCorepresentable, ofHom_apply, forget_reflects_isos, inv_hom_apply, coe_id, id_apply, comp_apply, coyonedaForget_hom_app_app_hom, forgetâGroup_preservesLimitsOfSize, forget_commGrp_preserves_epi, coyonedaForget_inv_app_app, one_apply, instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, forget_preservesLimitsOfSize, forgetâ_grp_map_ofHom, forgetâ_commMonCat_map_ofHom, forgetâGroup_preservesLimitsOfShape, forgetâ_map, forget_preservesLimitsOfShape
|
instInhabited đ | CompOp | â |
instOneHom đ | CompOp | 1 mathmath: one_apply
|
of đ | CompOp | 16 mathmath: coe_of, uliftFunctor_obj, coyonedaType_map_app, CommMonCat.val_units_map_hom_apply, CommMonCat.val_inv_units_map_hom_apply, hom_ofHom, ofHom_apply, tensorObj_eq, binaryProductLimitCone_cone_pt, ofHom_id, ofHom_comp, binaryProductLimitCone_isLimit_lift, forgetâ_grp_map_ofHom, forgetâ_commMonCat_map_ofHom, coyoneda_map_app, ofHom_injective
|
ofHom đ | CompOp | 19 mathmath: uliftFunctor_map, CategoryTheory.yonedaCommGrpGrpObj_map, coyonedaType_map_app, hom_ofHom, ofHom_apply, MulEquiv.toCommGrpIso_inv, CategoryTheory.yonedaCommGrpGrp_map_app, MulEquiv.toCommGrpIso_hom, ofHom_id, ofHom_comp, coyonedaType_obj_map, binaryProductLimitCone_isLimit_lift, forgetâ_grp_map_ofHom, coyoneda_obj_map, forgetâ_commMonCat_map_ofHom, coyoneda_map_app, ofHom_hom, ofHom_injective, AddCommGrpCat.toCommGrp_map
|
str đ | CompOp | 59 mathmath: uliftFunctor_map, forgetâCommMon_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, epi_iff_surjective, hasLimit_iff_small_sections, forget_map, forget_preservesLimits, uliftFunctor_obj, FilteredColimits.forgetâGroup_preservesFilteredColimits, ext_iff, coe_comp, forgetâGroup_preservesLimit, hom_inv_apply, FilteredColimits.forget_preservesFilteredColimits, Îź_forget_apply, hom_id, forgetâCommMon_preservesLimitsOfSize, forget_commGrp_preserves_mono, forgetâGroup_preservesLimits, coyonedaType_map_app, instFullGrpCatForgetâMonoidHomCarrierCarrier, mono_iff_injective, forget_isCorepresentable, ofHom_apply, MulEquiv.toCommGrpIso_inv, forget_reflects_isos, range_eq_top_of_epi, inv_hom_apply, hom_comp, tensorObj_eq, coe_id, id_apply, mono_iff_ker_eq_bot, comp_apply, coyonedaForget_hom_app_app_hom, binaryProductLimitCone_cone_pt, forgetâGroup_preservesLimitsOfSize, coyoneda_obj_obj_coe, forget_commGrp_preserves_epi, ker_eq_bot_of_mono, coyonedaForget_inv_app_app, MulEquiv.toCommGrpIso_hom, one_apply, coyonedaType_obj_map, instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, binaryProductLimitCone_isLimit_lift, forget_preservesLimitsOfSize, forgetâ_grp_map_ofHom, coyoneda_obj_map, forgetâ_commMonCat_map_ofHom, epi_iff_range_eq_top, coyoneda_map_app, ofHom_hom, forgetâGroup_preservesLimitsOfShape, forgetâ_map, toAddCommGrp_map, forget_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply
|
uliftFunctor đ | CompOp | 7 mathmath: uliftFunctor_map, uliftFunctor_preservesLimitsOfSize, uliftFunctor_obj, instFaithfulUliftFunctor, uliftFunctor_preservesLimit, instFullUliftFunctor, uliftFunctor_preservesLimitsOfShape
|
| Name | Category | Theorems |
|---|
carrier đ | CompOp | 105 mathmath: FilteredColimits.colimit_inv_mk_eq, SurjectiveOfEpiAuxs.Ď_apply_fromCoset, CategoryTheory.PresheafOfGroups.OneCochain.one_ev, surjective_of_epi, ProfiniteGrp.ProfiniteCompletion.lift_eta, forget_reflects_isos, CategoryTheory.PresheafOfGroups.Cochainâ.inv_apply, ofHom_hom, forget_isCorepresentable, SurjectiveOfEpiAuxs.Ď_symm_apply_infinity, SurjectiveOfEpiAuxs.Ď_apply_infinity, AddGrpCat.toGrp_obj_coe, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans, FiniteGrp.isFinite, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, CommGrpCat.forgetâGroup_preservesLimit, CategoryTheory.PresheafOfGroups.Cochainâ.one_apply, hom_id, binaryProductLimitCone_cone_pt, mono_iff_ker_eq_bot, FilteredColimits.forgetâMon_preservesFilteredColimits, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, SurjectiveOfEpiAuxs.g_apply_infinity, toAddGrp_map, SurjectiveOfEpiAuxs.comp_eq, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, ker_eq_bot_of_mono, FiniteGrp.instFiniteCarrierToGrp, ProfiniteGrp.ProfiniteCompletion.preimage_le, binaryProductLimitCone_isLimit_lift, CategoryTheory.essImage_yonedaGrp, subsingleton_of_isZero, tensorObj_eq, forgetâMon_preservesLimits, SurjectiveOfEpiAuxs.agree, forget_preservesLimits, hom_inv_apply, ProfiniteGrp.ProfiniteCompletion.denseRange, CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm, CategoryTheory.yonedaGrp_naturality_assoc, CategoryTheory.PresheafOfGroups.OneCochain.mul_ev, coe_comp, hasLimit_iff_small_sections, coe_of, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, forgetâ_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, ofHom_apply, CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp, mono_iff_injective, instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, FilteredColimits.colimit_mul_mk_eq, inv_hom_apply, CommGrpCat.forgetâGroup_preservesLimitsOfSize, instFullMonCatForgetâMonoidHomCarrierCarrier, forget_grp_preserves_epi, SurjectiveOfEpiAuxs.h_apply_fromCoset, isZero_iff_subsingleton, CategoryTheory.yonedaGrpObj_obj_coe, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, FilteredColimits.forget_preservesFilteredColimits, forget_preservesLimitsOfShape, FiniteGrp.ofHom_apply, MulEquiv.toGrpIso_inv, ext_iff, toAddGrp_obj_coe, CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl, CategoryTheory.PreGaloisCategory.AutGalois.Ď_apply, MonCat.units_obj_coe, forgetâ_map_ofHom, one_apply, forget_map, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, MulEquiv.toGrpIso_hom, CommGrpCat.forgetâ_grp_map_ofHom, ProfiniteGrp.diagram_map, CategoryTheory.PresheafOfGroups.OneCochain.inv_ev, forget_preservesLimitsOfSize, SurjectiveOfEpiAuxs.mul_smul, FilteredColimits.colimit_mul_mk_eq', uliftFunctor_map, epi_iff_range_eq_top, SurjectiveOfEpiAuxs.g_apply_fromCoset, epi_iff_surjective, FilteredColimits.colimit_one_eq, SurjectiveOfEpiAuxs.Ď_symm_apply_fromCoset, id_apply, Îź_forget_apply, SurjectiveOfEpiAuxs.one_smul, hom_comp, forgetâMon_preservesLimitsOfSize, CommGrpCat.forgetâGroup_preservesLimitsOfShape, comp_apply, CommGrpCat.forgetâ_map, uliftFunctor_obj, forget_grp_preserves_mono, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe, coe_id, CategoryTheory.PresheafOfGroups.Cochainâ.mul_apply, CategoryTheory.yonedaGrp_naturality, instIsRightAdjointForgetMonoidHomCarrier, ProfiniteGrp.diagram_obj
|
fullyFaithfulForgetâToMonCat đ | CompOp | â |
hasForgetToMonCat đ | CompOp | 7 mathmath: FilteredColimits.forgetâMon_preservesFilteredColimits, forgetâMon_preservesLimits, forgetâ_map, instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, instFullMonCatForgetâMonoidHomCarrierCarrier, forgetâ_map_ofHom, forgetâMon_preservesLimitsOfSize
|
instCategory đ | CompOp | 113 mathmath: FilteredColimits.colimit_inv_mk_eq, CategoryTheory.PresheafOfGroups.OneCochain.one_ev, surjective_of_epi, CategoryTheory.yonedaGrp_obj, ProfiniteGrp.ProfiniteCompletion.lift_eta, forget_reflects_isos, CategoryTheory.PresheafOfGroups.Cochainâ.inv_apply, CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, forget_isCorepresentable, AddGrpCat.toGrp_obj_coe, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, CommGrpCat.forgetâGroup_preservesLimit, CategoryTheory.PresheafOfGroups.Cochainâ.one_apply, hom_id, binaryProductLimitCone_cone_pt, mono_iff_ker_eq_bot, isZero_of_subsingleton, FilteredColimits.forgetâMon_preservesFilteredColimits, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, toAddGrp_map, SurjectiveOfEpiAuxs.comp_eq, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, uliftFunctor_preservesLimitsOfSize, binaryProductLimitCone_isLimit_lift, CategoryTheory.essImage_yonedaGrp, tensorObj_eq, forgetâMon_preservesLimits, forget_preservesLimits, hom_inv_apply, CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm, hasLimitsOfShape, AddGrpCat.toGrp_map, CategoryTheory.yonedaGrp_naturality_assoc, CategoryTheory.PresheafOfGroups.OneCochain.mul_ev, coe_comp, hasLimit_iff_small_sections, uliftFunctor_preservesLimitsOfShape, groupAddGroupEquivalence_inverse, ProfiniteGrp.profiniteCompletion_map, ofHom_comp, CategoryTheory.yonedaGrpObj_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, forgetâ_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, groupAddGroupEquivalence_functor, ofHom_apply, CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp, mono_iff_injective, uliftFunctor_preservesLimit, instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp, FilteredColimits.colimit_mul_mk_eq, inv_hom_apply, MonCat.val_units_map_hom_apply, CommGrpCat.forgetâGroup_preservesLimitsOfSize, instHasZeroObject, instFullMonCatForgetâMonoidHomCarrierCarrier, groupAddGroupEquivalence_unitIso, ofHom_id, forget_grp_preserves_epi, isZero_iff_subsingleton, groupAddGroupEquivalence_counitIso, CategoryTheory.yonedaGrpObj_obj_coe, FilteredColimits.forget_preservesFilteredColimits, hasLimitsOfSize, forget_preservesLimitsOfShape, MulEquiv.toGrpIso_inv, ext_iff, MonCat.val_inv_units_map_hom_apply, ofHom_injective, toAddGrp_obj_coe, CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl, CategoryTheory.PreGaloisCategory.AutGalois.Ď_apply, MonCat.units_obj_coe, forgetâ_map_ofHom, one_apply, forget_map, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, MulEquiv.toGrpIso_hom, CommGrpCat.forgetâ_grp_map_ofHom, CategoryTheory.PresheafOfGroups.OneCochain.inv_ev, forget_preservesLimitsOfSize, FilteredColimits.colimit_mul_mk_eq', uliftFunctor_map, CategoryTheory.PreGaloisCategory.autGaloisSystem_map, instFaithfulUliftFunctor, ProfiniteGrp.profiniteCompletion_obj, CategoryTheory.yonedaGrp_map_app, epi_iff_range_eq_top, instIsRightAdjointGrpCatMonCatUnits, epi_iff_surjective, FilteredColimits.colimit_one_eq, hasLimit, id_apply, Îź_forget_apply, hom_comp, forgetâMon_preservesLimitsOfSize, CommGrpCat.forgetâGroup_preservesLimitsOfShape, comp_apply, CommGrpCat.forgetâ_map, uliftFunctor_obj, forget_grp_preserves_mono, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe, hasLimits, coe_id, CategoryTheory.PresheafOfGroups.Cochainâ.mul_apply, instFullUliftFunctor, CategoryTheory.yonedaGrp_naturality, instIsRightAdjointForgetMonoidHomCarrier
|
instCoeMonCat đ | CompOp | â |
instCoeSortType đ | CompOp | â |
instConcreteCategoryMonoidHomCarrier đ | CompOp | 52 mathmath: surjective_of_epi, ProfiniteGrp.ProfiniteCompletion.lift_eta, forget_reflects_isos, forget_isCorepresentable, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, CommGrpCat.forgetâGroup_preservesLimit, FilteredColimits.forgetâMon_preservesFilteredColimits, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, CategoryTheory.essImage_yonedaGrp, forgetâMon_preservesLimits, forget_preservesLimits, hom_inv_apply, CategoryTheory.yonedaGrp_naturality_assoc, coe_comp, hasLimit_iff_small_sections, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, forgetâ_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, ofHom_apply, CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp, mono_iff_injective, instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, FilteredColimits.colimit_mul_mk_eq, inv_hom_apply, CommGrpCat.forgetâGroup_preservesLimitsOfSize, instFullMonCatForgetâMonoidHomCarrierCarrier, forget_grp_preserves_epi, FilteredColimits.forget_preservesFilteredColimits, forget_preservesLimitsOfShape, ext_iff, CategoryTheory.PreGaloisCategory.AutGalois.Ď_apply, forgetâ_map_ofHom, one_apply, forget_map, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, CommGrpCat.forgetâ_grp_map_ofHom, forget_preservesLimitsOfSize, epi_iff_surjective, id_apply, Îź_forget_apply, forgetâMon_preservesLimitsOfSize, CommGrpCat.forgetâGroup_preservesLimitsOfShape, comp_apply, CommGrpCat.forgetâ_map, forget_grp_preserves_mono, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, coe_id, CategoryTheory.yonedaGrp_naturality, instIsRightAdjointForgetMonoidHomCarrier
|
instInhabited đ | CompOp | â |
instOneHom đ | CompOp | 1 mathmath: one_apply
|
of đ | CompOp | 17 mathmath: ProfiniteGrp.ProfiniteCompletion.lift_eta, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, hom_ofHom, binaryProductLimitCone_cone_pt, SurjectiveOfEpiAuxs.comp_eq, binaryProductLimitCone_isLimit_lift, tensorObj_eq, coe_of, ProfiniteGrp.profiniteCompletion_map, ofHom_comp, ofHom_apply, MonCat.val_units_map_hom_apply, ofHom_id, MonCat.val_inv_units_map_hom_apply, ofHom_injective, forgetâ_map_ofHom, uliftFunctor_obj
|
ofHom đ | CompOp | 19 mathmath: ofHom_hom, hom_ofHom, SurjectiveOfEpiAuxs.comp_eq, binaryProductLimitCone_isLimit_lift, AddGrpCat.toGrp_map, ofHom_comp, CategoryTheory.yonedaGrpObj_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, ofHom_apply, ofHom_id, MulEquiv.toGrpIso_inv, ofHom_injective, forgetâ_map_ofHom, MulEquiv.toGrpIso_hom, CommGrpCat.forgetâ_grp_map_ofHom, uliftFunctor_map, CategoryTheory.PreGaloisCategory.autGaloisSystem_map, CategoryTheory.yonedaGrp_map_app
|
str đ | CompOp | 94 mathmath: FilteredColimits.colimit_inv_mk_eq, SurjectiveOfEpiAuxs.Ď_apply_fromCoset, CategoryTheory.PresheafOfGroups.OneCochain.one_ev, surjective_of_epi, ProfiniteGrp.ProfiniteCompletion.lift_eta, forget_reflects_isos, CategoryTheory.PresheafOfGroups.Cochainâ.inv_apply, ofHom_hom, forget_isCorepresentable, SurjectiveOfEpiAuxs.Ď_symm_apply_infinity, SurjectiveOfEpiAuxs.Ď_apply_infinity, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, CommGrpCat.forgetâGroup_preservesLimit, CategoryTheory.PresheafOfGroups.Cochainâ.one_apply, hom_id, binaryProductLimitCone_cone_pt, mono_iff_ker_eq_bot, FilteredColimits.forgetâMon_preservesFilteredColimits, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, SurjectiveOfEpiAuxs.g_apply_infinity, toAddGrp_map, SurjectiveOfEpiAuxs.comp_eq, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, ker_eq_bot_of_mono, ProfiniteGrp.ProfiniteCompletion.preimage_le, binaryProductLimitCone_isLimit_lift, CategoryTheory.essImage_yonedaGrp, tensorObj_eq, forgetâMon_preservesLimits, SurjectiveOfEpiAuxs.agree, forget_preservesLimits, hom_inv_apply, CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm, CategoryTheory.yonedaGrp_naturality_assoc, CategoryTheory.PresheafOfGroups.OneCochain.mul_ev, coe_comp, hasLimit_iff_small_sections, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, forgetâ_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, ofHom_apply, CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp, mono_iff_injective, instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, FilteredColimits.colimit_mul_mk_eq, inv_hom_apply, CommGrpCat.forgetâGroup_preservesLimitsOfSize, instFullMonCatForgetâMonoidHomCarrierCarrier, forget_grp_preserves_epi, SurjectiveOfEpiAuxs.h_apply_fromCoset, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, FilteredColimits.forget_preservesFilteredColimits, forget_preservesLimitsOfShape, FiniteGrp.ofHom_apply, MulEquiv.toGrpIso_inv, ext_iff, CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl, CategoryTheory.PreGaloisCategory.AutGalois.Ď_apply, forgetâ_map_ofHom, one_apply, forget_map, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, MulEquiv.toGrpIso_hom, CommGrpCat.forgetâ_grp_map_ofHom, ProfiniteGrp.diagram_map, CategoryTheory.PresheafOfGroups.OneCochain.inv_ev, forget_preservesLimitsOfSize, SurjectiveOfEpiAuxs.mul_smul, FilteredColimits.colimit_mul_mk_eq', uliftFunctor_map, epi_iff_range_eq_top, SurjectiveOfEpiAuxs.g_apply_fromCoset, epi_iff_surjective, FilteredColimits.colimit_one_eq, SurjectiveOfEpiAuxs.Ď_symm_apply_fromCoset, id_apply, Îź_forget_apply, SurjectiveOfEpiAuxs.one_smul, hom_comp, forgetâMon_preservesLimitsOfSize, CommGrpCat.forgetâGroup_preservesLimitsOfShape, comp_apply, CommGrpCat.forgetâ_map, uliftFunctor_obj, forget_grp_preserves_mono, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, coe_id, CategoryTheory.PresheafOfGroups.Cochainâ.mul_apply, CategoryTheory.yonedaGrp_naturality, instIsRightAdjointForgetMonoidHomCarrier, ProfiniteGrp.diagram_obj
|
uliftFunctor đ | CompOp | 7 mathmath: uliftFunctor_preservesLimitsOfSize, uliftFunctor_preservesLimitsOfShape, uliftFunctor_preservesLimit, uliftFunctor_map, instFaithfulUliftFunctor, uliftFunctor_obj, instFullUliftFunctor
|
| Name | Category | Theorems |
|---|
AddCommGrpCat đ | CompData | 286 mathmath: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, AddCommGrpCat.image.lift_fac, AddCommGrpCat.coyoneda_obj_obj_coe, AddCommGrpCat.isZero_iff_subsingleton, AddCommGrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, ModuleCat.forgetâ_reflectsLimitsOfSize, AddCommGrpCat.biproductIsoPi_inv_comp_Ď_apply, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda, AddCommGrpCat.comp_apply, RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForgetâRingHomCarrierAddMonoidHomCarrier, ModuleCat.forgetâPreservesColimitsOfSize, commGroupAddCommGroupEquivalence_functor, AddCommGrpCat.hom_add, AddCommGrpCat.instPreservesMonomorphismsFree, AddCommGrpCat.ofHom_comp, AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits, ModuleCat.forgetâAddCommGroup_preservesLimitsOfSize, ModuleCat.mkOfSMul'_smul, PresheafOfModules.Sheafify.add_smul, CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda, AddCommGrpCat.hasLimit, AddCommGrpCat.injective_of_divisible, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, AddCommGrpCat.hasZeroObject, AddCommGrpCat.hasLimitsOfSize, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', CategoryTheory.Abelian.extFunctorObj_obj_coe, AddCommGrpCat.hom_zero, AddCommGrpCat.hasLimitsOfShape, instAB4AddCommGrpCat, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, RingCat.forgetâAddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', AddCommGrpCat.hasColimit_of_small_quot, CochainComplex.HomComplex.leftHomologyData_K_coe, AddCommGrpCat.isColimit_iff_bijective_desc, commGroupAddCommGroupEquivalence_counitIso, ModuleCat.forgetâ_addCommGrp_essSurj, AddCommGrpCat.hasLimits, CochainComplex.HomComplex.leftHomologyData'_i, AddCommGrpCat.neg_hom_apply, AddCommGrpCat.forget_preservesLimits, ModuleCat.forgetâAddCommGroup_reflectsLimitOfShape, SheafOfModules.toSheaf_obj_val, AddCommGrpCat.forget_preservesLimitsOfShape, AddCommGrpCat.coe_comp, instHasFilteredColimitsAddCommGrpCat, AddCommGrpCat.forgetâ_map, ModuleCat.HasColimit.colimitCocone_Κ_app, AddCommGrpCat.Colimits.colimitCocone_Κ_app, ModuleCat.forgetâ_addCommGroup_full, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, CochainComplex.HomComplex.leftHomologyData_Ď_hom_apply, AddCommGrpCat.asHom_injective, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', SheafOfModules.ΚFree_mapFree_inv_assoc, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, ModuleCat.smul_naturality, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, ModuleCat.HasColimit.colimitCocone_pt_isModule, CategoryTheory.Abelian.extFunctorObj_map, CategoryTheory.preadditiveYoneda_obj, AddCommGrpCat.ext_iff, AddCommGrpCat.uliftFunctor_additive, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, AddCommGrpCat.instMonoΚ, AddCommGrpCat.forget_commGrp_preserves_epi, CategoryTheory.preadditiveYonedaMap_app, AddCommGrpCat.coyonedaForget_inv_app_app, AddCommGrpCat.free_map_coe, AddCommGrpCat.instHasFiniteBiproducts, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, AddCommGrpCat.coyonedaForget_hom_app_app_hom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, AddCommGrpCat.instFaithfulUliftFunctor, AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply, AddCommGrpCat.toCommGrp_obj_coe, CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, AddCommGrpCat.binaryProductLimitCone_isLimit_lift, AddCommGrpCat.binaryProductLimitCone_cone_Ď_app_left, AddCommGrpCat.homAddEquiv_symm_apply_hom, CategoryTheory.additive_yonedaObj', AddCommGrpCat.hom_sub, instAB4StarAddCommGrpCat, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.faithful_preadditiveCoyoneda, CategoryTheory.faithful_preadditiveYoneda, ModuleCat.forgetâAddCommGroup_preservesLimits, AddCommGrpCat.free_obj_coe, AddCommGrpCat.Colimits.quotUliftToQuot_Κ, AddCommGrpCat.hom_id, AddCommGrpCat.hom_nsmul, CategoryTheory.preservesLimits_preadditiveCoyoneda_obj, AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe, ModuleCat.forgetâ_obj, SheafOfModules.toSheaf_map_val, AddCommGrpCat.Colimits.colimitCocone_pt, AddCommGrpCat.forget_commGrp_preserves_mono, CategoryTheory.whiskering_linearCoyonedaâ, PresheafOfModules.sheafification_map, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, AddCommGrpCat.uliftFunctor_preservesLimitsOfSize, AddEquiv.toAddCommGrpIso_hom, AddCommGrpCat.hasColimit, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.Abelian.instAdditiveAddCommGrpCatExtFunctorObj, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.whiskering_preadditiveYoneda, AddCommGrpCat.forgetâAddGroup_preservesLimits, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, CategoryTheory.Abelian.extFunctor_obj, AddCommGrpCat.Colimits.quotToQuotUlift_Κ, ModuleCat.smulNatTrans_apply_app, CategoryTheory.Abelian.extFunctor_map_app, AddCommGrpCat.zero_apply, CategoryTheory.Abelian.Ext.covariantSequence_exact, AddCommGrpCat.id_apply, AddCommGrpCat.int_hom_ext_iff, AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app, CategoryTheory.preservesLimits_preadditiveYoneda_obj, PresheafOfModules.Sheafify.smul_add, AddCommGrpCat.Îź_forget_apply, CategoryTheory.additive_coyonedaObj', AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.tensorObj_eq, AddCommGrpCat.forgetâ_addGrp_map_ofHom, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, CategoryTheory.full_preadditiveCoyoneda, FGModuleCat.instFiniteCarrierColimitModuleCatCompForgetâLinearMapIdObjIsFG, AddCommGrpCat.forgetâAddCommMon_preservesLimitsOfShape, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, AddCommGrpCat.coyonedaType_obj_map, AddCommGrpCat.coyonedaType_obj_obj_coe, AddCommGrpCat.mono_iff_injective, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, AddCommGrpCat.Colimits.toCocone_Κ_app, AddCommGrpCat.Colimits.Quot.Κ_desc, ModuleCat.FilteredColimits.forgetâAddCommGroup_preservesFilteredColimits, AddCommGrpCat.Colimits.Quot.map_Κ, AddCommGrpCat.isZero_of_subsingleton, AddCommGrpCat.kernelIsoKer_inv_comp_Κ, AddCommGrpCat.image.fac, AddCommGrpCat.HasLimit.productLimitCone_cone_Ď, ModuleCat.forgetâ_obj_moduleCat_of, AddCommGrpCat.forgetâAddGroup_preservesLimit, AddCommGrpCat.injective_of_mono, AddCommGrpCat.epi_iff_range_eq_top, SheafOfModules.Presentation.map_relations_I, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, CategoryTheory.Abelian.Ext.covariant_sequence_exactâ', AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, CategoryTheory.Abelian.Ext.mono_postcomp_mkâ_of_mono, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, ModuleCat.HasColimit.coconePointSMul_apply, SheafOfModules.ΚFree_mapFree_inv, SheafOfModules.Presentation.mapRelations_mapGenerators, AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux, AddCommGrpCat.coe_id, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForgetâLinearMapIdCarrierAddMonoidHomCarrier, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, AddCommGrpCat.enoughInjectives, AddCommGrpCat.Colimits.toCocone_pt_coe, AddCommGrpCat.uliftFunctor_preservesLimitsOfShape, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, AddCommGrpCat.ofHom_id, AddCommGrpCat.injective_as_module_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, ModuleCat.mkOfSMul_smul, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.biprodIsoProd_inv_comp_desc, AddCommGrpCat.uliftFunctor_map, AddCommGrpCat.biprodIsoProd_inv_comp_snd, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎUnitOpensCarrierCarrierCommRingCatRingCatSheaf, CategoryTheory.full_preadditiveYoneda, CategoryTheory.Abelian.Ext.mono_precomp_mkâ_of_epi, SheafOfModules.Presentation.of_isIso_relations, AddCommGrpCat.hom_comp, AddCommGrpCat.uliftFunctor_obj, AddCommGrpCat.uliftFunctor_preservesLimit, ModuleCat.reflectsColimitsOfShape, ModuleCat.forgetâAddCommGroup_reflectsLimitOfSize, AddCommGrpCat.biprodIsoProd_inv_comp_desc_apply, CochainComplex.HomComplex.leftHomologyData_H_coe, CochainComplex.HomComplex.leftHomologyData'_K_coe, AddCommGrpCat.ofHom_apply, AddCommGrpCat.hasColimitsOfShape, AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply, instPreservesHomologyFunctorAddCommGrpCatColim, SheafOfModules.Presentation.of_isIso_generators, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, AddCommGrpCat.instIsLeftAdjointFree, SheafOfModules.map_ΚFree_mapFree_hom, AddCommGrpCat.biproductIsoPi_inv_comp_Ď, AddCommGrpCat.instIsSerreClassIsFinite, commGroupAddCommGroupEquivalence_unitIso, AddCommGrpCat.wellPowered_addCommGrp, AddCommGrpCat.HasLimit.lift_hom_apply, AddCommGrpCat.hasColimitsOfSize, ModuleCat.HasColimit.colimitCocone_pt_carrier, ModuleCat.forgetâ_addCommGrp_additive, AddCommGrpCat.biprodIsoProd_inv_comp_fst, RingCat.forgetâAddCommGroup_preservesLimitsOfSize, CochainComplex.HomComplex_X, CochainComplex.HomComplex.leftHomologyData'_H_coe, AddCommGrpCat.forgetâ_commMonCat_map_ofHom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, AddCommGrpCat.forgetâAddCommMon_preservesLimitsOfSize, AddCommGrpCat.coyoneda_map_app, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, AddCommGrpCat.forget_map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, ModuleCat.forgetâ_reflectsLimits, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, ModuleCat.forgetâPreservesColimitsOfShape, CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda, AddCommGrpCat.instFullUliftFunctor, CochainComplex.HomComplex.leftHomologyData'_Ď, ModuleCat.forgetâAddCommGroup_reflectsLimit, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, SheafOfModules.Presentation.map_generators_I, ModuleCat.forgetâAddCommGroup_preservesLimit, PresheafOfModules.Sheafify.zero_smul, CategoryTheory.Abelian.Ext.contravariant_sequence_exactâ', instAB5AddCommGrpCat, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_Xâ, SheafOfModules.map_ΚFree_mapFree_hom_assoc, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.whiskering_linearYonedaâ, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, AddCommGrpCat.hom_neg_apply, CommGrpCat.toAddCommGrp_obj_coe, ModuleCat.HasColimit.reflectsColimit, AddCommGrpCat.hom_add_apply, AddCommGrpCat.ofHom_injective, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.Sheafify.map_smul, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, PresheafOfModules.toSheafify_app_apply, AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier, AddCommGrpCat.forget_isCorepresentable, AddCommGrpCat.binaryProductLimitCone_cone_Ď_app_right, CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj, ModuleCat.forgetâAddCommGroupIsEquivalence, AddCommGrpCat.instPreservesColimitsOfSizeUliftFunctor, AddCommGrpCat.mono_iff_ker_eq_bot, CategoryTheory.preadditiveCoyoneda_obj, instHasExactLimitsOfShapeDiscreteAddCommGrpCat, AddEquiv.toAddCommGrpIso_inv, AddCommGrpCat.hom_neg, CommGrpCat.toAddCommGrp_map, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeÎFreeOpensCarrierCarrierCommRingCat, AddCommGrpCat.homAddEquiv_apply, CategoryTheory.Abelian.Ext.contravariantSequence_exact, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, SheafOfModules.Presentation.map_Ď_eq, AddCommGrpCat.coyonedaType_map_app, commGroupAddCommGroupEquivalence_inverse, AddCommGrpCat.hasColimit_iff_small_quot, AddCommGrpCat.toCommGrp_map, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, AddCommGrpCat.instHasBinaryBiproducts, CochainComplex.HomComplex_d_hom_apply, PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification, AddCommGrpCat.hasLimit_iff_small_sections, AddCommGrpCat.hom_zsmul, AddCommGrpCat.forget_preservesLimitsOfSize, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, CategoryTheory.whiskering_preadditiveCoyoneda, ModuleCat.forgetâ_map, AddCommGrpCat.coyoneda_obj_map, AddCommGrpCat.forget_reflects_isos
|
AddCommGrpMax đ | CompOp | â |
AddCommGrpMaxAux đ | CompOp | â |
AddGrpCat đ | CompData | 75 mathmath: AddCommGrpCat.forgetâAddGroup_preservesLimitsOfShape, AddGrpCat.hasLimits, AddGrpCat.forget_grp_preserves_epi, AddGrpCat.hasLimitsOfShape, AddGrpCat.uliftFunctor_obj, AddGrpCat.forgetâ_map, AddGrpCat.id_apply, AddGrpCat.hasLimitsOfSize, AddGrpCat.uliftFunctor_preservesLimit, AddGrpCat.forget_preservesLimits, AddGrpCat.toGrp_obj_coe, AddGrpCat.tensorObj_eq, AddGrpCat.uliftFunctor_map, AddGrpCat.forget_grp_preserves_mono, AddCommGrpCat.forgetâ_map, AddGrpCat.hom_comp, AddCommGrpCat.FilteredColimits.forgetâAddGroup_preservesFilteredColimits, AddGrpCat.FilteredColimits.colimit_add_mk_eq, AddGrpCat.FilteredColimits.colimit_neg_mk_eq, GrpCat.toAddGrp_map, AddGrpCat.forgetâAddMonPreservesLimitsOfSize, AddGrpCat.isZero_iff_subsingleton, AddGrpCat.FilteredColimits.forget_preservesFilteredColimits, AddGrpCat.zero_apply, AddEquiv.toAddGrpIso_hom, AddGrpCat.uliftFunctor_preservesLimitsOfShape, AddGrpCat.forget_preservesLimitsOfShape, AddGrpCat.binaryProductLimitCone_isLimit_lift, AddGrpCat.ext_iff, AddCommGrpCat.forgetâAddGroup_preservesLimits, AddGrpCat.ofHom_injective, AddGrpCat.toGrp_map, AddGrpCat.hasLimit_iff_small_sections, AddGrpCat.mono_iff_injective, AddGrpCat.uliftFunctor_preservesLimitsOfSize, AddGrpCat.forgetâ_map_ofHom, groupAddGroupEquivalence_inverse, AddCommGrpCat.forgetâ_addGrp_map_ofHom, AddGrpCat.isZero_of_subsingleton, AddGrpCat.forget_reflects_isos, AddGrpCat.Îź_forget_apply, AddCommGrpCat.forgetâAddGroup_preservesLimit, AddGrpCat.FilteredColimits.colimit_add_mk_eq', groupAddGroupEquivalence_functor, AddCommGrpCat.instFullAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddCommGrpCat.forgetâAddGroup_preservesLimitsOfSize, AddGrpCat.ofHom_comp, AddGrpCat.hasZeroObject, AddGrpCat.instSmallElemForallObjCompMonCatForgetâAddMonoidHomCarrierCarrierForgetSections, AddCommGrpCat.instReflectsIsomorphismsAddGrpCatForgetâAddMonoidHomCarrierCarrier, AddEquiv.toAddGrpIso_inv, AddGrpCat.neg_hom_apply, AddGrpCat.hom_neg_apply, groupAddGroupEquivalence_unitIso, AddGrpCat.forget_preservesLimitsOfSize, AddGrpCat.instFaithfulUliftFunctor, groupAddGroupEquivalence_counitIso, AddGrpCat.comp_apply, AddGrpCat.FilteredColimits.forgetâAddMon_preservesFilteredColimits, AddGrpCat.epi_iff_range_eq_top, AddGrpCat.epi_iff_surjective, GrpCat.toAddGrp_obj_coe, AddGrpCat.coe_comp, AddGrpCat.hasLimit, AddGrpCat.FilteredColimits.colimit_zero_eq, AddGrpCat.forget_isCorepresentable, AddGrpCat.instFullUliftFunctor, AddGrpCat.ofHom_id, AddGrpCat.instFullMonCatForgetâAddMonoidHomCarrierCarrier, AddGrpCat.binaryProductLimitCone_cone_pt, AddGrpCat.hom_id, AddGrpCat.ofHom_apply, AddGrpCat.mono_iff_ker_eq_bot, AddGrpCat.coe_id, AddGrpCat.forgetâMon_preservesLimits
|
AddGrpMax đ | CompOp | â |
CommGrpCat đ | CompData | 91 mathmath: CommGrpCat.uliftFunctor_map, commGroupAddCommGroupEquivalence_functor, CommGrpCat.uliftFunctor_preservesLimitsOfSize, CommGrpCat.forgetâCommMon_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, CategoryTheory.yonedaCommGrpGrpObj_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CommGrpCat.epi_iff_surjective, CommGrpCat.hasLimit_iff_small_sections, CommGrpCat.forget_map, CommGrpCat.forget_preservesLimits, CommGrpCat.isZero_of_subsingleton, CommGrpCat.uliftFunctor_obj, commGroupAddCommGroupEquivalence_counitIso, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, CommGrpCat.ext_iff, CommGrpCat.isZero_iff_subsingleton, CommGrpCat.coe_comp, CommGrpCat.forgetâGroup_preservesLimit, CommGrpCat.hom_inv_apply, CommGrpCat.instFaithfulUliftFunctor, CommGrpCat.uliftFunctor_preservesLimit, CommGrpCat.FilteredColimits.forget_preservesFilteredColimits, CommGrpCat.hasLimits, CommGrpCat.Îź_forget_apply, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, CommGrpCat.hom_id, CommGrpCat.forgetâCommMon_preservesLimitsOfSize, CommGrpCat.forget_commGrp_preserves_mono, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.coyonedaType_map_app, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, AddCommGrpCat.toCommGrp_obj_coe, CommMonCat.val_units_map_hom_apply, CommMonCat.val_inv_units_map_hom_apply, CommGrpCat.mono_iff_injective, CommGrpCat.forget_isCorepresentable, CommGrpCat.instFullUliftFunctor, CommGrpCat.ofHom_apply, MulEquiv.toCommGrpIso_inv, CommGrpCat.uliftFunctor_preservesLimitsOfShape, CommGrpCat.forget_reflects_isos, CommGrpCat.inv_hom_apply, CategoryTheory.yonedaCommGrpGrp_obj, CommGrpCat.hom_comp, CommGrpCat.tensorObj_eq, CommGrpCat.coe_id, CommGrpCat.id_apply, CommGrpCat.mono_iff_ker_eq_bot, CommGrpCat.comp_apply, CommGrpCat.coyonedaForget_hom_app_app_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, CommGrpCat.binaryProductLimitCone_cone_pt, CategoryTheory.yonedaCommGrpGrpObj_obj_coe, CommGrpCat.forgetâGroup_preservesLimitsOfSize, CommGrpCat.coyoneda_obj_obj_coe, instIsRightAdjointCommGrpCatCommMonCatUnits, CommMonCat.units_obj_coe, commGroupAddCommGroupEquivalence_unitIso, CommGrpCat.enoughInjectives, CommGrpCat.forget_commGrp_preserves_epi, CategoryTheory.yonedaCommGrpGrp_map_app, CommGrpCat.coyonedaForget_inv_app_app, MulEquiv.toCommGrpIso_hom, CommGrpCat.one_apply, CommGrpCat.ofHom_id, CommGrpCat.ofHom_comp, CommGrpCat.hasLimitsOfSize, CommGrpCat.coyonedaType_obj_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, CommGrpCat.binaryProductLimitCone_isLimit_lift, CommGrpCat.forget_preservesLimitsOfSize, CommGrpCat.forgetâ_grp_map_ofHom, CommGrpCat.coyoneda_obj_map, CommGrpCat.forgetâ_commMonCat_map_ofHom, CommGrpCat.hasLimit, CommGrpCat.toAddCommGrp_obj_coe, CommGrpCat.instHasZeroObject, CommGrpCat.epi_iff_range_eq_top, CommGrpCat.coyoneda_map_app, CommGrpCat.ofHom_injective, CommGrpCat.forgetâGroup_preservesLimitsOfShape, CommGrpCat.forgetâ_map, CommGrpCat.coyonedaType_obj_obj_coe, CommGrpCat.toAddCommGrp_map, commGroupAddCommGroupEquivalence_inverse, AddCommGrpCat.toCommGrp_map, CommGrpCat.forget_preservesLimitsOfShape, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply, CommGrpCat.hasLimitsOfShape
|
CommGrpMax đ | CompOp | â |
GrpCat đ | CompData | 113 mathmath: GrpCat.FilteredColimits.colimit_inv_mk_eq, CategoryTheory.PresheafOfGroups.OneCochain.one_ev, GrpCat.surjective_of_epi, CategoryTheory.yonedaGrp_obj, ProfiniteGrp.ProfiniteCompletion.lift_eta, GrpCat.forget_reflects_isos, CategoryTheory.PresheafOfGroups.Cochainâ.inv_apply, CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, GrpCat.forget_isCorepresentable, AddGrpCat.toGrp_obj_coe, CommGrpCat.FilteredColimits.forgetâGroup_preservesFilteredColimits, CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, CommGrpCat.forgetâGroup_preservesLimit, CategoryTheory.PresheafOfGroups.Cochainâ.one_apply, GrpCat.hom_id, GrpCat.binaryProductLimitCone_cone_pt, GrpCat.mono_iff_ker_eq_bot, GrpCat.isZero_of_subsingleton, GrpCat.FilteredColimits.forgetâMon_preservesFilteredColimits, CommGrpCat.forgetâGroup_preservesLimits, CommGrpCat.instFullGrpCatForgetâMonoidHomCarrierCarrier, GrpCat.toAddGrp_map, GrpCat.SurjectiveOfEpiAuxs.comp_eq, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, GrpCat.uliftFunctor_preservesLimitsOfSize, GrpCat.binaryProductLimitCone_isLimit_lift, CategoryTheory.essImage_yonedaGrp, GrpCat.tensorObj_eq, GrpCat.forgetâMon_preservesLimits, GrpCat.forget_preservesLimits, GrpCat.hom_inv_apply, CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm, GrpCat.hasLimitsOfShape, AddGrpCat.toGrp_map, CategoryTheory.yonedaGrp_naturality_assoc, CategoryTheory.PresheafOfGroups.OneCochain.mul_ev, GrpCat.coe_comp, GrpCat.hasLimit_iff_small_sections, GrpCat.uliftFunctor_preservesLimitsOfShape, groupAddGroupEquivalence_inverse, ProfiniteGrp.profiniteCompletion_map, GrpCat.ofHom_comp, CategoryTheory.yonedaGrpObj_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, GrpCat.forgetâ_map, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, groupAddGroupEquivalence_functor, GrpCat.ofHom_apply, CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp, GrpCat.mono_iff_injective, GrpCat.uliftFunctor_preservesLimit, GrpCat.instSmallElemForallObjCompMonCatForgetâMonoidHomCarrierCarrierForgetSections, CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp, GrpCat.FilteredColimits.colimit_mul_mk_eq, GrpCat.inv_hom_apply, MonCat.val_units_map_hom_apply, CommGrpCat.forgetâGroup_preservesLimitsOfSize, GrpCat.instHasZeroObject, GrpCat.instFullMonCatForgetâMonoidHomCarrierCarrier, groupAddGroupEquivalence_unitIso, GrpCat.ofHom_id, GrpCat.forget_grp_preserves_epi, GrpCat.isZero_iff_subsingleton, groupAddGroupEquivalence_counitIso, CategoryTheory.yonedaGrpObj_obj_coe, GrpCat.FilteredColimits.forget_preservesFilteredColimits, GrpCat.hasLimitsOfSize, GrpCat.forget_preservesLimitsOfShape, MulEquiv.toGrpIso_inv, GrpCat.ext_iff, MonCat.val_inv_units_map_hom_apply, GrpCat.ofHom_injective, GrpCat.toAddGrp_obj_coe, CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl, CategoryTheory.PreGaloisCategory.AutGalois.Ď_apply, MonCat.units_obj_coe, GrpCat.forgetâ_map_ofHom, GrpCat.one_apply, GrpCat.forget_map, CommGrpCat.instReflectsIsomorphismsGrpCatForgetâMonoidHomCarrierCarrier, MulEquiv.toGrpIso_hom, CommGrpCat.forgetâ_grp_map_ofHom, CategoryTheory.PresheafOfGroups.OneCochain.inv_ev, GrpCat.forget_preservesLimitsOfSize, GrpCat.FilteredColimits.colimit_mul_mk_eq', GrpCat.uliftFunctor_map, CategoryTheory.PreGaloisCategory.autGaloisSystem_map, GrpCat.instFaithfulUliftFunctor, ProfiniteGrp.profiniteCompletion_obj, CategoryTheory.yonedaGrp_map_app, GrpCat.epi_iff_range_eq_top, instIsRightAdjointGrpCatMonCatUnits, GrpCat.epi_iff_surjective, GrpCat.FilteredColimits.colimit_one_eq, GrpCat.hasLimit, GrpCat.id_apply, GrpCat.Îź_forget_apply, GrpCat.hom_comp, GrpCat.forgetâMon_preservesLimitsOfSize, CommGrpCat.forgetâGroup_preservesLimitsOfShape, GrpCat.comp_apply, CommGrpCat.forgetâ_map, GrpCat.uliftFunctor_obj, GrpCat.forget_grp_preserves_mono, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, CategoryTheory.PreGaloisCategory.autGaloisSystem_obj_coe, GrpCat.hasLimits, GrpCat.coe_id, CategoryTheory.PresheafOfGroups.Cochainâ.mul_apply, GrpCat.instFullUliftFunctor, CategoryTheory.yonedaGrp_naturality, GrpCat.instIsRightAdjointForgetMonoidHomCarrier
|
GrpMax đ | CompOp | â |
GrpMaxAux đ | CompOp | â |
addEquivIsoAddCommGroupIso đ | CompOp | â |
addEquivIsoAddGroupIso đ | CompOp | â |
mulEquivIsoCommGroupIso đ | CompOp | â |
mulEquivIsoGroupIso đ | CompOp | â |