| 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 | 134 mathmath: extensive_regular_generate_coherent, Equivalence.sheafCongrPrecoherent_counitIso_hom_app_val_app, Presheaf.coherentExtensiveEquivalence_functor_map_val, LightCondensed.ihomPoints_apply, condensedSetToTopCat_obj_carrier, Condensed.hom_ext_iff, LightCondensed.forget_obj_val_map, LightCondensed.ihomPoints_symm_comp, 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, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.discrete_map, LightCondMod.isDiscrete_tfae, coherentTopology.eq_induced, TopCat.toSheafCompHausLike_val_obj, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, LightCondensed.discrete_map, Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, Condensed.epi_iff_surjective_on_stonean, LightCondSet.topCatAdjunctionUnit_val_app_apply, Condensed.isSheafStonean, Equivalence.sheafCongrPrecoherent_functor_obj_val_obj, CompHausLike.LocallyConstantModule.functor_map_val, CompHausLike.LocallyConstant.functor_map_val, Condensed.instPreservesFiniteProductsOppositeCompHausVal, Presheaf.coherentExtensiveEquivalence_counitIso, topCatToSheafCompHausLike_map_val_app, CondensedMod.isDiscrete_iff_isDiscrete_forget, Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts, Presheaf.isSheaf_coherent_iff_regular_and_extensive, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, Presheaf.isSheaf_iff_extensiveSheaf_of_projective, Presheaf.coherentExtensiveEquivalence_inverse_map_val, Equivalence.sheafCongrPrecoherent_functor_obj_val_map, LightProfinite.hasSheafify, CondensedMod.epi_iff_surjective_on_stonean, CompHausLike.LocallyConstant.functor_obj_val, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, CondensedSet.epi_iff_surjective_on_stonean, Equivalence.sheafCongrPrecoherent_inverse_map_val_app, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, CompHausLike.LocallyConstantModule.functor_obj_val, CondensedSet.topCatAdjunctionUnit_val_app_apply, coherentTopology.instIsDenseSubsite, Equivalence.sheafCongrPrecoherent_inverse_obj_val_obj, LightCondensed.forget_map_val_app, Condensed.comp_val, CondensedMod.hom_naturality_apply, topCatToSheafCompHausLike_obj, Condensed.epi_iff_locallySurjective_on_compHaus, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, coherentTopology.subcanonical, coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, LightCondensed.ofSheafForgetLightProfinite_val, CompHausLike.LocallyConstant.adjunction_left_triangle, Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits, Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app, CondensedSet.continuous_coinducingCoprod, coherentTopology.isSheaf_yoneda_obj, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective, CondensedSet.topCatAdjunctionUnit_val_app, LightCondensed.hom_ext_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, LightCondensed.underlying_obj, Equivalence.sheafCongrPrecoherent_unitIso_inv_app_val_app, LightCondSet.hom_naturality_apply, CondensedSet.isDiscrete_tfae, Equivalence.precoherent_isSheaf_iff, coherentTopology.mem_sieves_of_hasEffectiveEpiFamily, Presheaf.coherentExtensiveEquivalence_unitIso, LightCondensed.equalizerCondition, Presheaf.instPreservesFiniteProductsOppositeVal, LightCondMod.hom_naturality_apply, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, coherentTopology.instIsCoverDense, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, Presheaf.coherentExtensiveEquivalence_functor_obj_val, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, Equivalence.sheafCongrPrecoherent_inverse_obj_val_map, lightCondSetToTopCat_obj_carrier, Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CompHausLike.LocallyConstant.counit_app_val, Condensed.instPreservesFiniteProductsOppositeStoneanVal, CondensedMod.epi_iff_locallySurjective_on_compHaus, TopCat.toSheafCompHausLike_val_map, isSheaf_coherent, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, coherentTopology.coverPreserving, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CompHausLike.LocallyConstant.unit_app, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_val_app, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, Condensed.underlying_obj, LightCondensed.id_val, coherentTopology.presheafIsLocallySurjective_iff, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CondensedSet.toTopCatMap_hom_apply, LightProfinite.hasSheafify_type, LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, Equivalence.sheafCongrPrecoherent_functor_map_val_app, LightCondensed.underlying_map, coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, Condensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, coherentTopology.isLocallySurjective_iff, LightCondSet.toTopCatMap_hom_apply, CondensedSet.epi_iff_locallySurjective_on_compHaus, Presheaf.coherentExtensiveEquivalence_inverse_obj_val, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.isSheafProfinite, Condensed.id_val, Equivalence.instIsDenseSubsiteCoherentTopologyInverse, Condensed.instAB4CondensedMod, Condensed.equalizerCondition_profinite, Condensed.equalizerCondition, LightCondensed.ofSheafLightProfinite_val, Condensed.discrete_obj, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, CompHausLike.LocallyConstant.adjunction_unit, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology
|
extensiveCoverage 📖 | CompOp | 1 mathmath: extensive_regular_generate_coherent
|
extensiveTopology 📖 | CompOp | 19 mathmath: Presheaf.coherentExtensiveEquivalence_functor_map_val, instPreservesFiniteProductsOppositeVal, Presieve.isSheaf_iff_preservesFiniteProducts, extensiveTopology.mem_sieves_iff_contains_colimit_cofan, Presheaf.isSheaf_iff_preservesFiniteProducts, extensiveTopology.isSheaf_yoneda_obj, Presheaf.coherentExtensiveEquivalence_counitIso, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, Presheaf.isSheaf_coherent_iff_regular_and_extensive, Presheaf.isSheaf_iff_extensiveSheaf_of_projective, Presheaf.coherentExtensiveEquivalence_inverse_map_val, extensiveTopology.subcanonical, isSheaf_pointwiseColimit, extensiveTopology.isLocallySurjective_iff, instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, extensiveTopology.presheafIsLocallySurjective_iff, Presheaf.coherentExtensiveEquivalence_unitIso, Presheaf.coherentExtensiveEquivalence_functor_obj_val, Presheaf.coherentExtensiveEquivalence_inverse_obj_val
|
regularCoverage 📖 | CompOp | 1 mathmath: extensive_regular_generate_coherent
|
regularTopology 📖 | CompOp | 29 mathmath: Equivalence.preregular_isSheaf_iff, Equivalence.sheafCongrPreregular_counitIso_inv_app_val_app, Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app, Equivalence.sheafCongrPreregular_inverse_obj_val_map, regularTopology.instIsCoverDense, Presheaf.isSheaf_coherent_iff_regular_and_extensive, Equivalence.sheafCongrPreregular_functor_obj_val_obj, regularTopology.subcanonical, Equivalence.sheafCongrPreregular_functor_map_val_app, Equivalence.sheafCongrPreregular_inverse_map_val_app, regularTopology.mem_sieves_iff_hasEffectiveEpi, Equivalence.sheafCongrPreregular_functor_obj_val_map, regularTopology.isSheaf_of_projective, regularTopology.isLocallySurjective_iff, regularTopology.equalizerCondition_iff_isSheaf, regularTopology.isSheaf_yoneda_obj, regularTopology.isLocallySurjective_sheaf_of_types, Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app, regularTopology.coverPreserving, Equivalence.instIsDenseSubsiteRegularTopologyInverse, regularTopology.instIsDenseSubsite, Equivalence.sheafCongrPreregular_inverse_obj_val_obj, 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_unitIso_inv_app_val_app, coherentTopology.isLocallySurjective_iff
|