Extend

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

Statistics

Metric	Count
Definitions cocone, cone, functor, functorOp, isColimitCocone, isLimitCone, asLimit', asLimitCone', diagram', fintypeDiagram', lim'	11
Theorems cocone_pt, cocone_ι_app, functorOp_final, functorOp_map, functorOp_obj, functor_initial, functor_map, functor_obj, instEpiAppOppositeNatπAsLimitCone	9
Total	20

LightProfinite

Definitions

Name	Category	Theorems
asLimit' 📖	CompOp	—
asLimitCone' 📖	CompOp	—
diagram' 📖	CompOp	—
fintypeDiagram' 📖	CompOp	—
lim' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEpiAppOppositeNatπAsLimitCone 📖	mathematical	—	CategoryTheory.Epi LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt diagram asLimitCone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	epi_iff_surjective proj_surjective

LightProfinite.Extend

Definitions

Name	Category	Theorems
cocone 📖	CompOp	4 math math: LightCondensed.lanPresheafIso_hom, cocone_ι_app, LightCondensed.lanPresheafNatIso_hom_app, cocone_pt
cone 📖	CompOp	—
functor 📖	CompOp	3 math math: functor_map, functor_initial, functor_obj
functorOp 📖	CompOp	4 math math: functorOp_obj, functorOp_map, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, functorOp_final
isColimitCocone 📖	CompOp	—
isLimitCone 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj cocone CategoryTheory.Functor.obj	—	—
cocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι cocone CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
functorOp_final 📖	mathematical	CategoryTheory.Epi LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite FintypeCat.toLightProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Functor.Final Preorder.smallCategory Nat.instPreorder CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow functorOp	—	functor_initial CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.final_comp CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence
functorOp_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory Nat.instPreorder CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow functorOp CategoryTheory.CostructuredArrow.homMk CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.homMk	—	—
functorOp_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory Nat.instPreorder CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow functorOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	—
functor_initial 📖	mathematical	CategoryTheory.Epi LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite FintypeCat.toLightProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Functor.Initial Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.StructuredArrow FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat.toLightProfinite CategoryTheory.instCategoryStructuredArrow functor	—	CategoryTheory.Functor.initial_iff_comp_equivalence CategoryTheory.StructuredArrow.isEquivalence_post CompHausLike.instFullToCompHausLike CompHausLike.instFaithfulToCompHausLike Profinite.Extend.functor_initial CategoryTheory.isCofiltered_op_of_isFiltered CategoryTheory.isFiltered_of_directed_le_nonempty instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.countableCategoryOpposite CategoryTheory.instCountableCategoryNat CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory CategoryTheory.Limits.hasCountableLimits_of_hasLimits Profinite.hasLimits
functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.StructuredArrow FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat.toLightProfinite CategoryTheory.instCategoryStructuredArrow functor CategoryTheory.StructuredArrow.homMk CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.StructuredArrow FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat.toLightProfinite CategoryTheory.instCategoryStructuredArrow functor CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	—

---

← Back to Index