AsLimit

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

Statistics

Metric	Count
Definitions asLimit, asLimitAux, asLimitCone, asLimitConeAux, component, diagram, fintypeDiagram, isoMapCone, lim, proj, transitionMap, transitionMapLE	12
Theorems lightToProfinite_map_proj_eq, proj_comp_transitionMap, proj_comp_transitionMap', proj_comp_transitionMapLE, proj_comp_transitionMapLE', proj_surjective, surjective_transitionMap, surjective_transitionMapLE	8
Total	20

LightProfinite

Definitions

Name	Category	Theorems
asLimit 📖	CompOp	—
asLimitAux 📖	CompOp	—
asLimitCone 📖	CompOp	3 math math: LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, instEpiAppOppositeNatπAsLimitCone
asLimitConeAux 📖	CompOp	—
component 📖	CompOp	4 math math: proj_comp_transitionMapLE', surjective_transitionMapLE, surjective_transitionMap, proj_comp_transitionMap'
diagram 📖	CompOp	8 math math: proj_comp_transitionMap, proj_comp_transitionMapLE', lightToProfinite_map_proj_eq, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, proj_surjective, proj_comp_transitionMapLE, instEpiAppOppositeNatπAsLimitCone, proj_comp_transitionMap'
fintypeDiagram 📖	CompOp	1 math math: LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp
isoMapCone 📖	CompOp	—
lim 📖	CompOp	—
proj 📖	CompOp	6 math math: proj_comp_transitionMap, proj_comp_transitionMapLE', lightToProfinite_map_proj_eq, proj_surjective, proj_comp_transitionMapLE, proj_comp_transitionMap'
transitionMap 📖	CompOp	2 math math: surjective_transitionMap, proj_comp_transitionMap'
transitionMapLE 📖	CompOp	2 math math: proj_comp_transitionMapLE', surjective_transitionMapLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lightToProfinite_map_proj_eq 📖	mathematical	—	CategoryTheory.Functor.map LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology Profinite lightToProfinite CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder diagram Opposite.op proj CategoryTheory.NatTrans.app DiscreteQuotient CompHausLike.toTop PartialOrder.toPreorder DiscreteQuotient.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Profinite.diagram Profinite.asLimitCone CategoryTheory.Limits.Cone.π CategoryTheory.Limits.IsCofiltered.sequentialFunctor instCountableDiscreteQuotient	—	instCountableDiscreteQuotient CategoryTheory.liftedLimitMapsToOriginal_inv_map_π CategoryTheory.countableCategoryOpposite CategoryTheory.instCountableCategoryNat
proj_comp_transitionMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp LightProfinite CategoryTheory.Category.toCategoryStruct CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder diagram Opposite.op proj CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Opposite.unop CategoryTheory.homOfLE	—	CategoryTheory.Limits.Cone.w
proj_comp_transitionMap' 📖	mathematical	—	component DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory transitionMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder diagram Opposite.op proj	—	proj_comp_transitionMap
proj_comp_transitionMapLE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp LightProfinite CategoryTheory.Category.toCategoryStruct CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder diagram Opposite.op proj CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Opposite.unop CategoryTheory.homOfLE	—	CategoryTheory.Limits.Cone.w
proj_comp_transitionMapLE' 📖	mathematical	—	component DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory transitionMapLE CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder diagram Opposite.op proj	—	proj_comp_transitionMapLE
proj_surjective 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology diagram Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory proj	—	instCountableDiscreteQuotient lightToProfinite_map_proj_eq DiscreteQuotient.proj_surjective
surjective_transitionMap 📖	mathematical	—	component DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory transitionMap	—	Function.Surjective.of_comp proj_comp_transitionMap' proj_surjective
surjective_transitionMapLE 📖	mathematical	—	component DFunLike.coe CategoryTheory.ConcreteCategory.hom LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory transitionMapLE	—	Function.Surjective.of_comp proj_comp_transitionMapLE' proj_surjective

---

← Back to Index