Functors

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

Statistics

Metric	Count
Definitions toCondensed, instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightProfiniteToLightCondSet, lightProfiniteToLightCondSetFullyFaithful, lightProfiniteToLightCondSetIsoTopCatToLightCondSet	5
Theorems instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom	7
Total	12

LightProfinite

Definitions

Name	Category	Theorems
toCondensed 📖	CompOp	10 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, LightCondensed.ihomPoints_symm_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, LightCondensed.internallyProjective_iff_tensor_condition, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondensed.ihomPoints_symm_apply, LightCondensed.ihom_map_val_app, LightCondensed.internallyProjective_iff_tensor_condition'

(root)

Definitions

Name	Category	Theorems
instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	CompOp	—
lightProfiniteToLightCondSet 📖	CompOp	15 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_symm_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.free_internallyProjective_iff_tensor_condition', lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.internallyProjective_iff_tensor_condition'
lightProfiniteToLightCondSetFullyFaithful 📖	CompOp	—
lightProfiniteToLightCondSetIsoTopCatToLightCondSet 📖	CompOp	2 math math: lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	mathematical	—	CategoryTheory.Functor.Faithful LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	—
instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	mathematical	—	CategoryTheory.Functor.Full LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	—
instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteCoproducts LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	—
instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory CategoryTheory.instCountableCategoryOfFinCategory
instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	CategoryTheory.Limits.preservesLimitsOfShape_of_natIso CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Adjunction.isRightAdjoint
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CategoryTheory.Functor.obj CompHausLike TotallyDisconnectedSpace TopCat.str SecondCountableTopology CompHausLike.category TopCat TopCat.instCategory CompHausLike.compHausLikeToTop Opposite.unop LightProfinite LightProfinite.toTopCat ContinuousMap.instFunLike CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf LightCondSet instCategoryLightCondensed lightProfiniteToLightCondSet CategoryTheory.Functor.comp topCatToLightCondSet CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Iso.hom lightProfiniteToLightCondSetIsoTopCatToLightCondSet CompHausLike.toTop CategoryTheory.ConcreteCategory.hom TopCat.instConcreteCategoryContinuousMapCarrier	—	—
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom 📖	mathematical	—	TopCat.Hom.hom TopCat.of TopCat.carrier TopCat.str CategoryTheory.InducedCategory.Hom.hom CompHausLike TotallyDisconnectedSpace SecondCountableTopology TopCat TopCat.instCategory CompHausLike.toTop Opposite.unop LightProfinite CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf LightCondSet instCategoryLightCondensed CategoryTheory.Functor.comp LightProfinite.toTopCat topCatToLightCondSet lightProfiniteToLightCondSet CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Iso.inv lightProfiniteToLightCondSetIsoTopCatToLightCondSet	—	—

---

← Back to Index