| Name | Category | Theorems |
|---|
Precoherent 📖 | CompData | 5 mathmath: Functor.reflects_precoherent, CompHausLike.precoherent, Equivalence.instPrecoherentSmallModel, instPrecoherentOfFinitaryPreExtensiveOfPreregular, Equivalence.precoherent
|
Preregular 📖 | CompData | 10 mathmath: instPreregularOfPrecoherentOfHasFiniteCoproducts, Profinite.instPreregular, Stonean.instPreregular, instPreregular, CompHaus.instPreregular, Equivalence.preregular, LightProfinite.instPreregular, Functor.reflects_preregular, CompHausLike.preregular, Equivalence.instPreregularSmallModel
|
coherentCoverage 📖 | CompOp | — |
coherentTopology 📖 | CompOp | 154 mathmath: extensive_regular_generate_coherent, LightCondensed.ihomPoints_apply, Condensed.instPreservesFiniteProductsOppositeStoneanObjFunctorIsSheafCoherentTopology, CompHausLike.LocallyConstant.functor_obj_obj, Presheaf.coherentExtensiveEquivalence_inverse_map_hom, condensedSetToTopCat_obj_carrier, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology, Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app, Condensed.hom_ext_iff, LightCondensed.ihomPoints_symm_comp, CondensedSet.topCatAdjunctionUnit_hom_app_apply, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, CondensedMod.isDiscrete_tfae, Equivalence.precoherent_isSheaf_iff_of_essentiallySmall, CondensedSet.hom_naturality_apply, CompHausLike.LocallyConstant.adjunction_counit, CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_sub_apply, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.discrete_map, Condensed.instPreservesFiniteProductsOppositeProfiniteObjFunctorIsSheafCoherentTopology, LightCondMod.isDiscrete_tfae, Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj, coherentTopology.eq_induced, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, LightCondensed.discrete_map, Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, Condensed.epi_iff_surjective_on_stonean, Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp, Condensed.id_hom, Condensed.isSheafStonean, LightCondensed.comp_hom, CondensedMod.isDiscrete_iff_isDiscrete_forget, Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts, LightCondensed.ofSheafLightProfinite_obj, Presheaf.isSheaf_coherent_iff_regular_and_extensive, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, Presheaf.isSheaf_coherent_of_projective_comp, Presheaf.isSheaf_iff_extensiveSheaf_of_projective, topCatToSheafCompHausLike_map_hom_app, Presheaf.coherentExtensiveEquivalence_functor_obj_obj, LightProfinite.hasSheafify, CondensedMod.epi_iff_surjective_on_stonean, Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology, Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, CompHausLike.LocallyConstant.counit_app_hom_app, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, CondensedSet.epi_iff_surjective_on_stonean, Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app, coherentTopology.instIsDenseSubsite, CompHausLike.LocallyConstant.functor_map_hom, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zero_apply, Condensed.comp_val, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_add_apply, Presheaf.isSheaf_coherent_of_projective_of_comp, CondensedMod.hom_naturality_apply, TopCat.toSheafCompHausLike_obj_obj, topCatToSheafCompHausLike_obj, Condensed.epi_iff_locallySurjective_on_compHaus, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, LightCondensed.forget_map_hom_app, coherentTopology.subcanonical, LightCondensed.forget_obj_obj_map, coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, Presheaf.coherentExtensiveEquivalence_functor_map_hom, CompHausLike.LocallyConstant.adjunction_left_triangle, Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_nsmul_apply, CondensedSet.continuous_coinducingCoprod, coherentTopology.isSheaf_yoneda_obj, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_neg_apply, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, LightCondSet.topCatAdjunctionUnit_hom_app_apply, Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective, LightCondensed.hom_ext_iff, LightCondensed.underlying_obj, LightCondSet.hom_naturality_apply, CondensedSet.isDiscrete_tfae, Equivalence.precoherent_isSheaf_iff, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isModule_smul_apply, coherentTopology.mem_sieves_of_hasEffectiveEpiFamily, coherentTopology.epi_π_app_zero_of_epi, LightCondensed.equalizerCondition, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zsmul_apply, LightCondMod.hom_naturality_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, coherentTopology.instIsCoverDense, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, lightCondSetToTopCat_obj_carrier, Equivalence.sheafCongrPrecoherent_functor_obj_obj_map, Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map, LightCondensed.ihom_map_val_app, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CondensedMod.epi_iff_locallySurjective_on_compHaus, TopCat.toSheafCompHausLike_obj_map, Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, Equivalence.sheafCongrPrecoherent_functor_map_hom_app, Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, isSheaf_coherent, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, coherentTopology.coverPreserving, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CompHausLike.LocallyConstant.unit_app, LightCondSet.isDiscrete_tfae, coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, LightCondSet.topCatAdjunctionUnit_hom_app, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, Condensed.underlying_obj, LightCondensed.id_val, LightCondensed.ofSheafForgetLightProfinite_obj, Condensed.comp_hom, coherentTopology.presheafIsLocallySurjective_iff, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CondensedSet.toTopCatMap_hom_apply, LightProfinite.hasSheafify_type, LightCondensed.comp_val, LightCondensed.id_hom, Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app, LightCondensed.underlying_map, coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, Condensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, Presheaf.isSheaf_coherent_of_hasPullbacks_comp, coherentTopology.isLocallySurjective_iff, LightCondSet.toTopCatMap_hom_apply, CondensedSet.epi_iff_locallySurjective_on_compHaus, CondensedSet.topCatAdjunctionUnit_hom_app, Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, Condensed.isSheafProfinite, Condensed.id_val, Equivalence.instIsDenseSubsiteCoherentTopologyInverse, Condensed.instPreservesFiniteProductsOppositeCompHausObjFunctorIsSheafCoherentTopology, Condensed.instAB4CondensedMod, CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply, Condensed.equalizerCondition_profinite, Condensed.equalizerCondition, Condensed.discrete_obj, CompHausLike.LocallyConstant.adjunction_unit, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology
|
extensiveCoverage 📖 | CompOp | 1 mathmath: extensive_regular_generate_coherent
|
extensiveTopology 📖 | CompOp | 21 mathmath: Presheaf.coherentExtensiveEquivalence_inverse_map_hom, Presieve.isSheaf_iff_preservesFiniteProducts, extensiveTopology.mem_sieves_iff_contains_colimit_cofan, Presheaf.isSheaf_iff_preservesFiniteProducts, extensiveTopology.isSheaf_yoneda_obj, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, Presheaf.isSheaf_coherent_iff_regular_and_extensive, Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, Presheaf.isSheaf_iff_extensiveSheaf_of_projective, extensiveTopology.subcanonical, Presheaf.coherentExtensiveEquivalence_functor_obj_obj, Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, isSheaf_pointwiseColimit, Presheaf.coherentExtensiveEquivalence_functor_map_hom, extensiveTopology.isLocallySurjective_iff, instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, extensiveTopology.presheafIsLocallySurjective_iff, Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology, Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app
|
regularCoverage 📖 | CompOp | 1 mathmath: extensive_regular_generate_coherent
|
regularTopology 📖 | CompOp | 29 mathmath: Equivalence.preregular_isSheaf_iff, Equivalence.sheafCongrPreregular_functor_obj_obj_obj, Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app, regularTopology.instIsCoverDense, Presheaf.isSheaf_coherent_iff_regular_and_extensive, regularTopology.subcanonical, Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app, regularTopology.mem_sieves_iff_hasEffectiveEpi, regularTopology.isSheaf_of_projective, Equivalence.sheafCongrPreregular_inverse_obj_obj_obj, regularTopology.isLocallySurjective_iff, regularTopology.equalizerCondition_iff_isSheaf, regularTopology.isSheaf_yoneda_obj, Equivalence.sheafCongrPreregular_inverse_map_hom_app, regularTopology.isLocallySurjective_sheaf_of_types, Equivalence.sheafCongrPreregular_inverse_obj_obj_map, Equivalence.sheafCongrPreregular_functor_map_hom_app, Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app, regularTopology.coverPreserving, Equivalence.instIsDenseSubsiteRegularTopologyInverse, regularTopology.instIsDenseSubsite, Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app, regularTopology.mem_sieves_of_hasEffectiveEpi, regularTopology.eq_induced, regularTopology.exists_effectiveEpi_iff_mem_induced, Equivalence.preregular_isSheaf_iff_of_essentiallySmall, coherentTopology.presheafIsLocallySurjective_iff, Equivalence.sheafCongrPreregular_functor_obj_obj_map, coherentTopology.isLocallySurjective_iff
|