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', instFintypeCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, instFintypeCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfCarrier, lightDiagramToLightProfinite, lightDiagramToProfinite, lightProfiniteToCompHaus, lightProfiniteToLightDiagram, lightToProfinite, lightToProfiniteFullyFaithful	33
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, instFullFintypeCatLightProfiniteToLightProfinite, instFullLightDiagram'LightDiagramToLightFunctor, instFullLightDiagramProfiniteLightDiagramToProfinite, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, lightDiagramToLightProfinite_map, lightDiagramToLightProfinite_obj, lightDiagramToProfinite_map, lightDiagramToProfinite_obj, lightProfiniteToLightDiagram_map, lightProfiniteToLightDiagram_obj	35
Total	68

FintypeCat

Definitions

Name	Category	Theorems
toLightProfinite 📖	CompOp	19 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, LightProfinite.Extend.functorOp_map, LightCondensed.lanPresheafNatIso_hom_app, LightProfinite.Extend.cocone_pt, LightCondensed.lanPresheafExt_inv, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, LightCondensed.lanPresheafExt_hom, instFullFintypeCatLightProfiniteToLightProfinite
toLightProfiniteFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLightProfinite_map_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap carrier 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 instCategory LightProfinite CompHausLike.category toLightProfinite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom 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	11 math math: LightCondensed.isoFinYonedaComponents_hom_apply, LightCondSet.continuous_coinducingCoprod, LightCondSet.topCatAdjunctionUnit_val_app_apply, lightDiagramToLightProfinite_obj, LightCondensed.isoFinYonedaComponents_inv_comp, LightCondensed.underlying_obj, lightCondSetToTopCat_obj_carrier, lightDiagramToLightProfinite_map, LightCondSet.topCatAdjunctionUnit_val_app, LightCondensed.underlying_map, LightCondSet.toTopCatMap_hom_apply
toLightDiagram 📖	CompOp	2 math math: lightProfiniteToLightDiagram_map, lightProfiniteToLightDiagram_obj
toTopCat 📖	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
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 CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape CategoryTheory.countableCategoryOpposite CategoryTheory.instCountableCategoryNat CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory CategoryTheory.Limits.hasCountableLimits_of_hasLimits Profinite.hasLimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
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	—	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	101 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.forget_obj_val_map, 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, LightProfinite.proj_comp_transitionMapLE', LightProfinite.Extend.cocone_ι_app, Profinite.injective_of_light, LightCondSet.topCatAdjunctionUnit_val_app_apply, lightProfiniteToLightDiagram_map, LightProfinite.isClosedMap, lightDiagramToLightProfinite_obj, LightProfinite.lightToProfinite_map_proj_eq, LightProfinite.effectiveEpi_iff_surjective, LightCondensed.internallyProjective_iff_tensor_condition, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instCountableDiscreteQuotient, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.hasSheafify, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.isoFinYonedaComponents_inv_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.Extend.functor_map, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, LightCondensed.forget_map_val_app, LightCondensed.isoLocallyConstantOfIsColimit_inv, FintypeCat.toLightProfinite_map_hom_hom_apply, LightProfinite.injective, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, LightProfinite.surjective_transitionMapLE, LightCondensed.free_internallyProjective_iff_tensor_condition', LightProfinite.instHasCountableLimits, LightProfinite.forget_reflectsIsomorphisms, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, LightProfinite.Extend.functorOp_map, instEssentiallySmallLightProfinite, LightCondensed.hom_ext_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, LightCondensed.underlying_obj, LightCondSet.hom_naturality_apply, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, LightCondensed.equalizerCondition, LightCondMod.hom_naturality_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, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, LightCondensed.lanPresheafExt_inv, LightProfinite.epi_iff_surjective, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_val_app, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instPreregular, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, LightCondensed.id_val, 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, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, LightCondensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, LightCondSet.toTopCatMap_hom_apply, LightCondensed.lanPresheafExt_hom, LightProfinite.proj_comp_transitionMap', instFullFintypeCatLightProfiniteToLightProfinite, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology
instCategoryLightDiagram' 📖	CompOp	4 math math: instFullLightDiagram'LightDiagramToLightFunctor, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, instEssSurjLightDiagram'LightDiagramToLightFunctor, instFaithfulLightDiagram'LightDiagramToLightFunctor
instFintypeCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite 📖	CompOp	—
instFintypeCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfCarrier 📖	CompOp	—
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 FintypeCat.instCategory 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
instFullFintypeCatLightProfiniteToLightProfinite 📖	mathematical	—	CategoryTheory.Functor.Full FintypeCat FintypeCat.instCategory 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 FintypeCat.instCategory 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 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 FintypeCat.instCategory 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 FintypeCat.instCategory 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