Basic

📁 Source: Mathlib/Condensed/Light/Basic.lean

Statistics

Metric	Count
Definitions LightCondSet, LightCondensed, instCategoryLightCondensed	3
Theorems hom_naturality_apply, comp_val, hom_ext, hom_ext_iff, id_val	5
Total	8

LightCondSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality_apply

LightCondensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.CategoryStruct.comp LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf.val	—	—
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val	—	—	CategoryTheory.Sheaf.hom_ext CategoryTheory.NatTrans.ext'
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val	—	hom_ext
id_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.CategoryStruct.id LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf.val	—	—

(root)

Definitions

Name	Category	Theorems
LightCondSet 📖	CompOp	37 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, LightCondensed.forget_obj_val_map, LightCondensed.ihomPoints_symm_comp, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightCondSet.instFaithfulTopCatTopCatToLightCondSet, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, LightCondMod.instPreservesEpimorphismsLightCondSetForget, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instIsRegularEpiCategoryLightCondSet, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, LightCondSet.LocallyConstant.instFaithfulFunctor, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instHasLimitsOfSizeLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.forget_map_val_app, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat, LightCondMod.instReflectsEpimorphismsLightCondSetForget, LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, LightCondensed.ihomPoints_symm_apply, lightCondSetToTopCat_obj_carrier, LightCondensed.ihom_map_val_app, instHasFiniteLimitsLightCondSet, LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone, LightCondSet.LocallyConstant.instFullFunctor, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondSet.isDiscrete_tfae, LightCondensed.internallyProjective_iff_tensor_condition', lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, LightCondMod.isDiscrete_iff_isDiscrete_forget, lightCondSetToTopCat_map
LightCondensed 📖	CompOp	14 math math: LightCondMod.isDiscrete_tfae, LightCondensed.discrete_map, LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete, LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete, LightCondensed.underlying_obj, LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete, LightCondensed.discrete_obj, LightCondSet.isDiscrete_tfae, LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete, LightCondensed.id_val, LightCondensed.comp_val, LightCondensed.underlying_map, LightCondensed.instSmallHom
instCategoryLightCondensed 📖	CompOp	58 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, LightCondensed.forget_obj_val_map, LightCondensed.ihomPoints_symm_comp, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightCondSet.instFaithfulTopCatTopCatToLightCondSet, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, LightCondMod.instPreservesEpimorphismsLightCondSetForget, LightCondMod.isDiscrete_tfae, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instIsRegularEpiCategoryLightCondSet, LightCondensed.discrete_map, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, LightCondSet.LocallyConstant.instFaithfulFunctor, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instHasLimitsOfSizeLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete, LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.forget_map_val_app, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat, LightCondMod.instReflectsEpimorphismsLightCondSetForget, LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, LightCondensed.underlying_obj, LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete, instHasLimitsOfSizeLightCondMod_1, LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, lightCondSetToTopCat_obj_carrier, LightCondMod.LocallyConstant.instFullModuleCatFunctor, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, instHasFiniteLimitsLightCondSet, instHasFiniteLimitsLightCondMod, LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone, LightCondSet.LocallyConstant.instFullFunctor, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, instHasLimitsOfSizeLightCondMod, LightCondSet.isDiscrete_tfae, LightCondensed.instCountableAB4StarLightCondMod, LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete, LightCondensed.id_val, LightCondensed.internallyProjective_iff_tensor_condition', LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, LightCondensed.instIsGrothendieckAbelianLightCondMod, LightCondensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, lightCondSetToTopCat_map, LightCondensed.instSmallHom

---

← Back to Index