Basic

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

Statistics

Metric	Count
Definitions toProfinite, toProfiniteObj, botTopology, toProfinite, toProfiniteFullyFaithful, instInhabited, limitCone, limitConeIsLimit, of, pi, createsLimits, reflective, toCompHausEquivalence, toProfiniteAdjToCompHaus, toTopCat, createsLimits, reflective, profiniteToCompHaus	18
Theorems toProfinite_obj', discreteTopology, toProfinite_map_hom_hom_apply, epi_iff_surjective, forget_preservesLimits, hasColimits, hasLimits, instHasPropTotallyDisconnectedSpaceCarrier, instTotallyDisconnectedSpaceCarrierToTop, instFaithfulFintypeCatProfiniteToProfinite, instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite, instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj, instFullFintypeCatProfiniteToProfinite, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus	14
Total	32

CompHaus

Definitions

Name	Category	Theorems
toProfinite 📖	CompOp	1 math math: toProfinite_obj'
toProfiniteObj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toProfinite_obj' 📖	mathematical	—	TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Functor.obj CompHaus CompHausLike.category Profinite toProfinite ConnectedComponents	—	—

FintypeCat

Definitions

Name	Category	Theorems
botTopology 📖	CompOp	5 math math: instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj, toProfinite_map_hom_hom_apply, toLightProfinite_map_hom_hom_apply, discreteTopology, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj
toProfinite 📖	CompOp	30 math math: Profinite.Extend.cocone_pt, instFullFintypeCatProfiniteToProfinite, Profinite.Extend.functorOp_map, Profinite.Extend.cone_π_app, Condensed.lanPresheafExt_inv, instFaithfulFintypeCatProfiniteToProfinite, lightDiagramToLightProfinite_obj, Profinite.Extend.functorOp_obj, Condensed.finYoneda_map, toProfinite_map_hom_hom_apply, Condensed.isColimitLocallyConstantPresheaf_desc_apply, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, Condensed.isoLocallyConstantOfIsColimit_inv, Condensed.lanPresheafNatIso_hom_app, Profinite.Extend.functor_obj, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, Profinite.Extend.functorOp_final, Profinite.Extend.cocone_ι_app, instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite, Condensed.isoFinYoneda_hom_app, Profinite.Extend.cone_pt, lightDiagramToLightProfinite_map, Condensed.lanPresheafExt_hom, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, Condensed.isoFinYoneda_inv_app, Profinite.Extend.functor_initial, Profinite.Extend.functor_map, Condensed.locallyConstantIsoFinYoneda_hom_app, Condensed.lanPresheafIso_hom, Profinite.exists_hom
toProfiniteFullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology 📖	mathematical	—	DiscreteTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite botTopology	—	—
toProfinite_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 CompHausLike.of CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.Functor.map FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Profinite CompHausLike.category toProfinite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ConcreteCategory.hom CategoryTheory.Types.instFunLike concreteCategoryFintype	—	—

Profinite

Definitions

Name	Category	Theorems
instInhabited 📖	CompOp	—
limitCone 📖	CompOp	4 math math: isIso_indexCone_lift, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, isIso_asLimitCone_lift
limitConeIsLimit 📖	CompOp	2 math math: isIso_indexCone_lift, isIso_asLimitCone_lift
of 📖	CompOp	4 math math: Condensed.isoFinYonedaComponents_hom_apply, instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj, projective_ultrafilter, Condensed.isoFinYonedaComponents_inv_comp
pi 📖	CompOp	—
toCompHausEquivalence 📖	CompOp	—
toProfiniteAdjToCompHaus 📖	CompOp	—
toTopCat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str 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 instTotallyDisconnectedSpaceCarrierToTop ULift.compactSpace Finite.compactSpace Finite.of_fintype ULift.instT2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyFin TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyULift instHasPropTotallyDisconnectedSpaceCarrier LocallyConstant.continuous continuous_const CategoryTheory.cancel_epi CategoryTheory.ConcreteCategory.ext ContinuousMap.ext ULift.ext ContinuousMap.continuous_toFun CategoryTheory.ConcreteCategory.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_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types CategoryTheory.forget ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	—	CategoryTheory.Limits.comp_preservesLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint TopCat.forget_preservesLimits
hasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	CategoryTheory.hasColimits_of_reflective CompHaus.hasColimits
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	CategoryTheory.hasLimits_of_hasLimits_createsLimits TopCat.topCat_hasLimits
instHasPropTotallyDisconnectedSpaceCarrier 📖	mathematical	—	CompHausLike.HasProp TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	—
instTotallyDisconnectedSpaceCarrierToTop 📖	mathematical	—	TotallyDisconnectedSpace TopCat.carrier CompHausLike.toTop TopCat.str	—	CompHausLike.prop

Profinite.toCompHaus

Definitions

Name	Category	Theorems
createsLimits 📖	CompOp	—
reflective 📖	CompOp	—

Profinite.toTopCat

Definitions

Name	Category	Theorems
createsLimits 📖	CompOp	—
reflective 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
profiniteToCompHaus 📖	CompOp	7 math math: CondensedMod.isDiscrete_tfae, Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, CondensedSet.isDiscrete_tfae, Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus, Condensed.isSheafProfinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulFintypeCatProfiniteToProfinite 📖	mathematical	—	CategoryTheory.Functor.Faithful FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str FintypeCat.toProfinite	—	CategoryTheory.Functor.FullyFaithful.faithful
instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite 📖	mathematical	—	Finite TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Profinite CompHausLike.category FintypeCat.toProfinite	—	—
instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj 📖	mathematical	—	Finite TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str Profinite.of CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types FintypeCat.botTopology Finite.compactSpace FintypeCat.instFiniteObj TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace FintypeCat.discreteTopology TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete	—	—
instFullFintypeCatProfiniteToProfinite 📖	mathematical	—	CategoryTheory.Functor.Full FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str FintypeCat.toProfinite	—	CategoryTheory.Functor.FullyFaithful.full
instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus 📖	mathematical	—	TotallyDisconnectedSpace TopCat.carrier CompHausLike.toTop CategoryTheory.Functor.obj Profinite CompHausLike.category TopCat.str CompHaus profiniteToCompHaus	—	CompHausLike.prop

---

← Back to Index