Basic

📁 Source: Mathlib/Topology/Category/LightProfinite/Basic.lean

Statistics

Metric	Count
Definitions toLightProfinite, toLightProfiniteFullyFaithful, LightDiagram, LightDiagram', diagram, toLightFunctor, toProfinite, cone, diagram, equivSmall, hasForget, instCategory, isLimit, toProfinite, LightProfinite, createsCountableLimits, equivDiagram, instInhabited, isoOfBijective, limitCone, limitConeIsLimit, of, toLightDiagram, toTopCat, instCategoryLightDiagram', lightDiagramToLightProfinite, lightDiagramToProfinite, lightProfiniteToCompHaus, lightProfiniteToLightDiagram, lightToProfinite, lightToProfiniteFullyFaithful	31
Theorems toLightProfinite_map_hom_hom_apply, comp_hom_hom_hom_apply, id_hom_hom_hom_apply, epi_iff_surjective, forget_reflectsIsomorphisms, instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, instCountableDiscreteQuotient, instHasCountableLimits, instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, instPreservesEpimorphismsProfiniteLightToProfinite, instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace, instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology, instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, isClosedMap, isIso_of_bijective, instEssSurjLightDiagram'LightDiagramToLightFunctor, instEssentiallySmallLightDiagram, instEssentiallySmallLightProfinite, instFaithfulFintypeCatLightProfiniteToLightProfinite, instFaithfulLightDiagram'LightDiagramToLightFunctor, instFaithfulLightDiagramProfiniteLightDiagramToProfinite, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj, instFullFintypeCatLightProfiniteToLightProfinite, instFullLightDiagram'LightDiagramToLightFunctor, instFullLightDiagramProfiniteLightDiagramToProfinite, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, lightDiagramToLightProfinite_map, lightDiagramToLightProfinite_obj, lightDiagramToProfinite_map, lightDiagramToProfinite_obj, lightProfiniteToLightDiagram_map, lightProfiniteToLightDiagram_obj	37
Total	68

FintypeCat

Definitions

Name	Category	Theorems
toLightProfinite 📖	CompOp	23 math math: LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, LightCondensed.isoFinYoneda_inv_app, instFaithfulFintypeCatLightProfiniteToLightProfinite, LightCondensed.finYoneda_map, LightProfinite.Extend.cocone_ι_app, LightProfinite.Extend.functor_map, LightCondensed.isoLocallyConstantOfIsColimit_inv, toLightProfinite_map_hom_hom_apply, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, LightProfinite.Extend.functorOp_map, LightCondensed.lanPresheafNatIso_hom_app, LightProfinite.Extend.cocone_pt, LightCondensed.lanPresheafExt_inv, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, LightProfinite.Extend.functor_initial, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, LightCondensed.lanPresheafExt_hom, instFullFintypeCatLightProfiniteToLightProfinite, LightProfinite.Extend.functorOp_final
toLightProfiniteFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLightProfinite_map_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite botTopology ContinuousMap.instFunLike TopCat.Hom.hom CompHausLike.toTop TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CompHausLike.of CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.Functor.map FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category LightProfinite CompHausLike.category toLightProfinite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ConcreteCategory.hom CategoryTheory.Types.instFunLike concreteCategoryFintype	—	—

LightDiagram

Definitions

Name	Category	Theorems
cone 📖	CompOp	3 math math: lightDiagramToLightProfinite_obj, lightDiagramToLightProfinite_map, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone
diagram 📖	CompOp	3 math math: lightDiagramToLightProfinite_obj, lightDiagramToLightProfinite_map, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone
equivSmall 📖	CompOp	—
hasForget 📖	CompOp	—
instCategory 📖	CompOp	17 math math: instFaithfulLightDiagramProfiniteLightDiagramToProfinite, lightDiagramToProfinite_map, lightProfiniteToLightDiagram_map, lightDiagramToLightProfinite_obj, lightDiagramToProfinite_obj, instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, instEssentiallySmallLightDiagram, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, lightProfiniteToLightDiagram_obj, id_hom_hom_hom_apply, lightDiagramToLightProfinite_map, instFullLightDiagramProfiniteLightDiagramToProfinite, comp_hom_hom_hom_apply, instEssSurjLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, instFaithfulLightDiagram'LightDiagramToLightFunctor
isLimit 📖	CompOp	—
toProfinite 📖	CompOp	6 math math: lightDiagramToProfinite_map, lightProfiniteToLightDiagram_map, lightDiagramToProfinite_obj, id_hom_hom_hom_apply, lightDiagramToLightProfinite_map, comp_hom_hom_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory LightDiagram Profinite CompHausLike.category CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory TopCat.Hom.hom'	—	—
id_hom_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory LightDiagram Profinite CompHausLike.category CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory	—	—

LightDiagram'

Definitions

Name	Category	Theorems
diagram 📖	CompOp	—
toLightFunctor 📖	CompOp	4 math math: instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instEssSurjLightDiagram'LightDiagramToLightFunctor, instFaithfulLightDiagram'LightDiagramToLightFunctor
toProfinite 📖	CompOp	—

LightProfinite

Definitions

Name	Category	Theorems
createsCountableLimits 📖	CompOp	—
equivDiagram 📖	CompOp	—
instInhabited 📖	CompOp	—
isoOfBijective 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—
of 📖	CompOp	12 math math: LightCondensed.isoFinYonedaComponents_hom_apply, LightCondSet.continuous_coinducingCoprod, lightDiagramToLightProfinite_obj, LightCondensed.isoFinYonedaComponents_inv_comp, LightCondSet.topCatAdjunctionUnit_hom_app_apply, LightCondensed.underlying_obj, lightCondSetToTopCat_obj_carrier, lightDiagramToLightProfinite_map, LightCondSet.topCatAdjunctionUnit_hom_app, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj, LightCondensed.underlying_map, LightCondSet.toTopCatMap_hom_apply
toLightDiagram 📖	CompOp	2 math math: lightProfiniteToLightDiagram_map, lightProfiniteToLightDiagram_obj
toTopCat 📖	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
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq IsCompact.isClosed CompHausLike.is_hausdorff isCompact_range CompHausLike.is_compact ContinuousMap.continuous Set.mem_compl IsClosed.compl_mem_nhds TopologicalSpace.IsTopologicalBasis.mem_nhds_iff isTopologicalBasis_isClopen instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology ULift.compactSpace Finite.compactSpace Finite.of_fintype ULift.instT2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyFin TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyULift TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableULift instCountableFin TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace LocallyConstant.continuous continuous_const CategoryTheory.cancel_epi CategoryTheory.ConcreteCategory.ext ContinuousMap.ext ULift.ext ContinuousMap.continuous_toFun CompHausLike.hom_ofHom top_ne_bot Fin.instNontrivial Nat.instAtLeastTwoHAddOfNat CategoryTheory.epi_iff_surjective CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget
forget_reflectsIsomorphisms 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.forget ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	—	isIso_of_bijective CategoryTheory.isIso_iff_bijective
instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology 📖	mathematical	—	Countable TopologicalSpace.Clopens TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str SecondCountableTopology	—	TopologicalSpace.Clopens.countable_iff_secondCountable CompHausLike.is_compact CompHausLike.is_hausdorff instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace
instCountableDiscreteQuotient 📖	mathematical	—	Countable DiscreteQuotient TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Functor.obj LightProfinite CompHausLike.category SecondCountableTopology Profinite lightToProfinite	—	Function.Injective.countable Finset.countable instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology CompHausLike.is_compact
instHasCountableLimits 📖	mathematical	—	CategoryTheory.Limits.HasCountableLimits LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	—
instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology 📖	mathematical	—	CompHausLike.HasProp TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	—
instPreservesEpimorphismsProfiniteLightToProfinite 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology Profinite lightToProfinite	—	Profinite.epi_iff_surjective epi_iff_surjective
instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.forget ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	—	CategoryTheory.Limits.preservesLimitsOfSize_shrink Profinite.forget_preservesLimits
instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace 📖	mathematical	—	SecondCountableTopology TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str	—	CompHausLike.prop
instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology 📖	mathematical	—	TotallyDisconnectedSpace TopCat.carrier CompHausLike.toTop TopCat.str SecondCountableTopology	—	CompHausLike.prop
instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus 📖	mathematical	—	TotallyDisconnectedSpace TopCat.carrier CompHausLike.toTop CategoryTheory.Limits.Cone.pt CompHaus CompHausLike.category CategoryTheory.Functor.comp LightProfinite TopCat.str SecondCountableTopology lightProfiniteToCompHaus CompHaus.limitCone	—	Subtype.totallyDisconnectedSpace Pi.totallyDisconnectedSpace instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology
isClosedMap 📖	mathematical	—	IsClosedMap TopCat.str CompHausLike.toTop TotallyDisconnectedSpace TopCat.carrier SecondCountableTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory	—	CompHausLike.isClosedMap
isIso_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.IsIso LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	CategoryTheory.isIso_of_fully_faithful CompHausLike.instFullToCompHausLike CompHausLike.instFaithfulToCompHausLike CompHausLike.isIso_of_bijective

(root)

Definitions

Name	Category	Theorems
LightDiagram 📖	CompData	17 math math: instFaithfulLightDiagramProfiniteLightDiagramToProfinite, lightDiagramToProfinite_map, lightProfiniteToLightDiagram_map, lightDiagramToLightProfinite_obj, lightDiagramToProfinite_obj, instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, instEssentiallySmallLightDiagram, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, lightProfiniteToLightDiagram_obj, LightDiagram.id_hom_hom_hom_apply, lightDiagramToLightProfinite_map, instFullLightDiagramProfiniteLightDiagramToProfinite, LightDiagram.comp_hom_hom_hom_apply, instEssSurjLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, instFaithfulLightDiagram'LightDiagramToLightFunctor
LightDiagram' 📖	CompData	4 math math: instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instEssSurjLightDiagram'LightDiagramToLightFunctor, instFaithfulLightDiagram'LightDiagramToLightFunctor
LightProfinite 📖	CompOp	111 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightProfinite.proj_comp_transitionMap, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, LightCondensed.isoFinYonedaComponents_hom_apply, LightCondensed.ihomPoints_apply, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteObjFunctorIsSheafCoherentTopology, LightCondensed.ihomPoints_symm_comp, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.isoFinYoneda_inv_app, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, instFaithfulFintypeCatLightProfiniteToLightProfinite, LightCondensed.finYoneda_map, LightCondMod.isDiscrete_tfae, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightCondensed.discrete_map, instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.proj_comp_transitionMapLE', LightProfinite.Extend.cocone_ι_app, Profinite.injective_of_light, lightProfiniteToLightDiagram_map, LightProfinite.isClosedMap, lightDiagramToLightProfinite_obj, LightCondensed.comp_hom, LightProfinite.lightToProfinite_map_proj_eq, LightCondensed.ofSheafLightProfinite_obj, LightProfinite.effectiveEpi_iff_surjective, LightCondensed.internallyProjective_iff_tensor_condition, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instCountableDiscreteQuotient, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.hasSheafify, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.isoFinYonedaComponents_inv_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.Extend.functor_map, LightCondensed.isoLocallyConstantOfIsColimit_inv, FintypeCat.toLightProfinite_map_hom_hom_apply, LightProfinite.injective, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, LightCondensed.forget_map_hom_app, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite, LightCondensed.forget_obj_obj_map, LightProfinite.surjective_transitionMapLE, LightCondensed.free_internallyProjective_iff_tensor_condition', LightProfinite.instHasCountableLimits, LightProfinite.forget_reflectsIsomorphisms, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, LightCondSet.topCatAdjunctionUnit_hom_app_apply, LightProfinite.Extend.functorOp_map, instEssentiallySmallLightProfinite, LightCondensed.hom_ext_iff, LightCondensed.underlying_obj, LightCondSet.hom_naturality_apply, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, LightCondensed.equalizerCondition, LightCondMod.hom_naturality_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, lightProfiniteToLightDiagram_obj, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightCondensed.lanPresheafNatIso_hom_app, lightCondSetToTopCat_obj_carrier, LightProfinite.Extend.cocone_pt, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, LightProfinite.isIso_of_bijective, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, LightCondensed.lanPresheafExt_inv, LightProfinite.epi_iff_surjective, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, LightProfinite.Extend.functor_initial, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_hom_app, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instPreregular, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, LightCondensed.id_val, LightCondensed.ofSheafForgetLightProfinite_obj, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, LightProfinite.proj_surjective, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, LightCondensed.internallyProjective_iff_tensor_condition', LightProfinite.hasSheafify_type, LightCondensed.comp_val, LightCondensed.id_hom, LightCondensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, LightCondSet.toTopCatMap_hom_apply, LightCondensed.lanPresheafExt_hom, LightProfinite.proj_comp_transitionMap', instFullFintypeCatLightProfiniteToLightProfinite, LightProfinite.Extend.functorOp_final, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology
instCategoryLightDiagram' 📖	CompOp	4 math math: instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instEssSurjLightDiagram'LightDiagramToLightFunctor, instFaithfulLightDiagram'LightDiagramToLightFunctor
lightDiagramToLightProfinite 📖	CompOp	3 math math: lightDiagramToLightProfinite_obj, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, lightDiagramToLightProfinite_map
lightDiagramToProfinite 📖	CompOp	4 math math: instFaithfulLightDiagramProfiniteLightDiagramToProfinite, lightDiagramToProfinite_map, lightDiagramToProfinite_obj, instFullLightDiagramProfiniteLightDiagramToProfinite
lightProfiniteToCompHaus 📖	CompOp	1 math math: LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus
lightProfiniteToLightDiagram 📖	CompOp	3 math math: lightProfiniteToLightDiagram_map, lightProfiniteToLightDiagram_obj, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram
lightToProfinite 📖	CompOp	4 math math: Profinite.injective_of_light, LightProfinite.lightToProfinite_map_proj_eq, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instCountableDiscreteQuotient
lightToProfiniteFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEssSurjLightDiagram'LightDiagramToLightFunctor 📖	mathematical	—	CategoryTheory.Functor.EssSurj LightDiagram' LightDiagram instCategoryLightDiagram' LightDiagram.instCategory LightDiagram'.toLightFunctor	—	instFullLightDiagramProfiniteLightDiagramToProfinite instFaithfulLightDiagramProfiniteLightDiagramToProfinite CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory CategoryTheory.Limits.hasCountableLimits_of_hasLimits Profinite.hasLimits CategoryTheory.countableCategoryOpposite CategoryTheory.instCountableCategoryNat CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instEssentiallySmallLightDiagram 📖	mathematical	—	CategoryTheory.EssentiallySmall LightDiagram LightDiagram.instCategory	—	—
instEssentiallySmallLightProfinite 📖	mathematical	—	CategoryTheory.EssentiallySmall LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	—
instFaithfulFintypeCatLightProfiniteToLightProfinite 📖	mathematical	—	CategoryTheory.Functor.Faithful FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology FintypeCat.toLightProfinite	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulLightDiagram'LightDiagramToLightFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful LightDiagram' instCategoryLightDiagram' LightDiagram LightDiagram.instCategory LightDiagram'.toLightFunctor	—	Equiv.injective
instFaithfulLightDiagramProfiniteLightDiagramToProfinite 📖	mathematical	—	CategoryTheory.Functor.Faithful LightDiagram LightDiagram.instCategory Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str lightDiagramToProfinite	—	CategoryTheory.InducedCategory.faithful
instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite 📖	mathematical	—	Finite TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str SecondCountableTopology CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types LightProfinite CompHausLike.category FintypeCat.toLightProfinite	—	—
instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj 📖	mathematical	—	Finite TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str SecondCountableTopology LightProfinite.of CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types FintypeCat.botTopology Finite.compactSpace instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace FintypeCat.discreteTopology TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace Finite.to_countable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace	—	—
instFullFintypeCatLightProfiniteToLightProfinite 📖	mathematical	—	CategoryTheory.Functor.Full FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology FintypeCat.toLightProfinite	—	CategoryTheory.Functor.FullyFaithful.full
instFullLightDiagram'LightDiagramToLightFunctor 📖	mathematical	—	CategoryTheory.Functor.Full LightDiagram' instCategoryLightDiagram' LightDiagram LightDiagram.instCategory LightDiagram'.toLightFunctor	—	—
instFullLightDiagramProfiniteLightDiagramToProfinite 📖	mathematical	—	CategoryTheory.Functor.Full LightDiagram LightDiagram.instCategory Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str lightDiagramToProfinite	—	CategoryTheory.InducedCategory.full
instIsEquivalenceLightDiagram'LightDiagramToLightFunctor 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence LightDiagram' instCategoryLightDiagram' LightDiagram LightDiagram.instCategory LightDiagram'.toLightFunctor	—	instFaithfulLightDiagram'LightDiagramToLightFunctor instFullLightDiagram'LightDiagramToLightFunctor instEssSurjLightDiagram'LightDiagramToLightFunctor
instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence LightDiagram LightDiagram.instCategory LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology lightDiagramToLightProfinite	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightDiagram LightDiagram.instCategory lightProfiniteToLightDiagram	—	CategoryTheory.Equivalence.isEquivalence_functor
instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone 📖	mathematical	—	SecondCountableTopology TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder Profinite CompHausLike.category CategoryTheory.Functor.comp FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightDiagram.diagram FintypeCat.toProfinite LightDiagram.cone	—	TopologicalSpace.Clopens.countable_iff_secondCountable CompHausLike.is_compact CompHausLike.is_hausdorff Profinite.instTotallyDisconnectedSpaceCarrierToTop Countable.of_equiv Function.Surjective.countable instCountableSigma instCountableNat Finite.to_countable Finite.of_injective Pi.finite instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj Finite.of_fintype LocallyConstant.coe_injective Profinite.exists_locallyConstant CategoryTheory.isCofiltered_op_of_isFiltered CategoryTheory.isFiltered_of_directed_le_nonempty instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
lightDiagramToLightProfinite_map 📖	mathematical	—	CategoryTheory.Functor.map LightDiagram LightDiagram.instCategory LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology lightDiagramToLightProfinite CategoryTheory.InducedCategory.homMk CompHausLike TopCat TopCat.instCategory CompHausLike.toTop LightProfinite.of CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder Profinite CategoryTheory.Functor.comp FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightDiagram.diagram FintypeCat.toProfinite LightDiagram.cone instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone CategoryTheory.InducedCategory.Hom.hom LightDiagram.toProfinite	—	instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone
lightDiagramToLightProfinite_obj 📖	mathematical	—	CategoryTheory.Functor.obj LightDiagram LightDiagram.instCategory LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology lightDiagramToLightProfinite LightProfinite.of CompHausLike.toTop CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder Profinite CategoryTheory.Functor.comp FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightDiagram.diagram FintypeCat.toProfinite LightDiagram.cone instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone	—	—
lightDiagramToProfinite_map 📖	mathematical	—	CategoryTheory.Functor.map LightDiagram LightDiagram.instCategory Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str lightDiagramToProfinite CategoryTheory.InducedCategory.Hom.hom LightDiagram.toProfinite	—	—
lightDiagramToProfinite_obj 📖	mathematical	—	CategoryTheory.Functor.obj LightDiagram LightDiagram.instCategory Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str lightDiagramToProfinite LightDiagram.toProfinite	—	—
lightProfiniteToLightDiagram_map 📖	mathematical	—	CategoryTheory.Functor.map LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightDiagram LightDiagram.instCategory lightProfiniteToLightDiagram CategoryTheory.InducedCategory.homMk Profinite LightDiagram.toProfinite LightProfinite.toLightDiagram CompHausLike TopCat TopCat.instCategory CompHausLike.toTop CategoryTheory.InducedCategory.Hom.hom	—	—
lightProfiniteToLightDiagram_obj 📖	mathematical	—	CategoryTheory.Functor.obj LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology LightDiagram LightDiagram.instCategory lightProfiniteToLightDiagram LightProfinite.toLightDiagram	—	—

---

← Back to Index