Basic

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

Statistics

Metric	Count
Definitions LightCondSet, LightCondensed, instCategoryLightCondensed	3
Theorems hom_naturality_apply, comp_hom, comp_val, hom_ext, hom_ext_iff, id_hom, id_val	7
Total	10

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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality_apply

LightCondensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.comp LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed	—	—
comp_val 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.comp LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed	—	comp_hom
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—	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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	hom_ext
id_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.id LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed	—	—
id_val 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.id LightCondensed CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed	—	id_hom

(root)

Definitions

Name	Category	Theorems
LightCondSet 📖	CompOp	38 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, LightCondensed.ihomPoints_symm_comp, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightCondSet.instFaithfulTopCatTopCatToLightCondSet, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, LightCondMod.instPreservesEpimorphismsLightCondSetForget, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instIsRegularEpiCategoryLightCondSet, instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, LightCondSet.LocallyConstant.instFaithfulFunctor, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, instHasLimitsOfSizeLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, LightCondensed.forget_map_hom_app, LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat, LightCondMod.instReflectsEpimorphismsLightCondSetForget, LightCondensed.forget_obj_obj_map, LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_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', LightCondMod.isDiscrete_iff_isDiscrete_forget, lightCondSetToTopCat_map
LightCondensed 📖	CompOp	16 math math: LightCondMod.isDiscrete_tfae, LightCondensed.discrete_map, LightCondensed.comp_hom, 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.id_hom, LightCondensed.underlying_map, LightCondensed.instSmallHom
instCategoryLightCondensed 📖	CompOp	63 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, 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, instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, LightCondensed.comp_hom, LightCondSet.LocallyConstant.instFaithfulFunctor, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, instHasLimitsOfSizeLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete, LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, LightCondensed.forget_map_hom_app, LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat, LightCondMod.instReflectsEpimorphismsLightCondSetForget, LightCondensed.forget_obj_obj_map, LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete, LightCondensed.underlying_obj, LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete, instHasLimitsOfSizeLightCondMod_1, LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, 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, LightCondensed.epi_π_app_zero_of_epi, 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, LightCondensed.id_hom, LightCondensed.instIsGrothendieckAbelianLightCondMod, LightCondensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, lightCondSetToTopCat_map, LightCondensed.instSmallHom, LightCondensed.instEpiLightCondModMapNat

---

← Back to Index