Functors

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

Statistics

Metric	Count
Definitions toCondensed, instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightProfiniteToLightCondSet, lightProfiniteToLightCondSetFullyFaithful, lightProfiniteToLightCondSetIsoTopCatToLightCondSet	5
Theorems instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom	6
Total	11

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	14 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_symm_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.internallyProjective_iff_tensor_condition, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.free_internallyProjective_iff_tensor_condition', lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.internallyProjective_iff_tensor_condition', lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom
lightProfiniteToLightCondSetFullyFaithful 📖	CompOp	—
lightProfiniteToLightCondSetIsoTopCatToLightCondSet 📖	CompOp	2 math math: lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom

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	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular CategoryTheory.coherentTopology.subcanonical CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda
instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet 📖	mathematical	—	CategoryTheory.Functor.Full LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightCondSet instCategoryLightCondensed CategoryTheory.types lightProfiniteToLightCondSet	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular CategoryTheory.coherentTopology.subcanonical CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda
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.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory CategoryTheory.Limits.hasCountableLimits_of_hasLimits Profinite.hasLimits CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint CategoryTheory.Adjunction.isRightAdjoint
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_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.Sheaf.instCategorySheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf LightCondSet instCategoryLightCondensed lightProfiniteToLightCondSet CategoryTheory.Functor.comp topCatToLightCondSet CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom lightProfiniteToLightCondSetIsoTopCatToLightCondSet CompHausLike.toTop CategoryTheory.ConcreteCategory.hom TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.InducedCategory.Hom.hom	—	—
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_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.Sheaf.instCategorySheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf LightCondSet instCategoryLightCondensed CategoryTheory.Functor.comp LightProfinite.toTopCat topCatToLightCondSet lightProfiniteToLightCondSet CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv lightProfiniteToLightCondSetIsoTopCatToLightCondSet	—	—

---

← Back to Index