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 FintypeCat.instCategory 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 FintypeCat.instCategory 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 FintypeCat.instCategory FintypeCat.toLightProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Functor.Final CategoryTheory.CostructuredArrow CategoryTheory.Functor.op Opposite.op CategoryTheory.instCategoryCostructuredArrow functorOp	—	functor_initial CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.final_comp CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.final_op_of_initial
functorOp_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory Nat.instPreorder CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory 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 FintypeCat.instCategory 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 FintypeCat.instCategory FintypeCat.toLightProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Functor.Initial CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow functor	—	CategoryTheory.Functor.initial_iff_comp_equivalence CategoryTheory.StructuredArrow.isEquivalence_post CompHausLike.instFullToCompHausLike CompHausLike.instFaithfulToCompHausLike CategoryTheory.Functor.map_epi LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite 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 FintypeCat.instCategory 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 FintypeCat.instCategory 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