Documentation Verification Report

Extend

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

Statistics

Metric	Count
Definitions `cocone`, `cone`, `functor`, `functorOp`, `isColimitCocone`, `isLimitCone`, `asLimit'`, `asLimitCone'`, `diagram'`, `fintypeDiagram'`, `lim'`	11
Theorems `cocone_pt`, `cocone_ι_app`, `cone_pt`, `cone_π_app`, `functorOp_final`, `functorOp_map`, `functorOp_obj`, `functor_initial`, `functor_map`, `functor_obj`, `exists_hom`, `instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`	12
Total	23

Profinite

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Profinite` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.toProfinite` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Functor.map`	—	`IsLocallyConstant.iff_continuous` `ContinuousMap.continuous` `exists_locallyConstant` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext` `LocallyConstant.congr_fun`
`instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone` 📖	mathematical	—	`CategoryTheory.Epi` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `DiscreteQuotient` `CompHausLike.toTop` `Preorder.smallCategory` `PartialOrder.toPreorder` `DiscreteQuotient.instPartialOrder` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `diagram` `asLimitCone` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	—	`epi_iff_surjective` `DiscreteQuotient.proj_surjective`

Profinite.Extend

Definitions

Name	Category	Theorems
`cocone` 📖	CompOp	4 math math: `cocone_pt`, `Condensed.lanPresheafNatIso_hom_app`, `cocone_ι_app`, `Condensed.lanPresheafIso_hom`
`cone` 📖	CompOp	2 math math: `cone_π_app`, `cone_pt`
`functor` 📖	CompOp	3 math math: `functor_obj`, `functor_initial`, `functor_map`
`functorOp` 📖	CompOp	4 math math: `functorOp_map`, `functorOp_obj`, `Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp`, `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` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.op` `FintypeCat.toProfinite` `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` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.op` `FintypeCat.toProfinite` `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`	—	—
`cone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.StructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `FintypeCat.toProfinite` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.comp` `CategoryTheory.StructuredArrow.proj` `cone` `CategoryTheory.Functor.obj`	—	—
`cone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.StructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `FintypeCat.toProfinite` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.comp` `CategoryTheory.StructuredArrow.proj` `CategoryTheory.Limits.Cone.π` `cone` `CategoryTheory.Functor.map` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit`	—	—
`functorOp_final` 📖	mathematical	`CategoryTheory.Epi` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.toProfinite` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	`CategoryTheory.Functor.Final` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CostructuredArrow` `CategoryTheory.Functor.op` `Opposite.op` `CategoryTheory.instCategoryCostructuredArrow` `functorOp`	—	`functor_initial` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Functor.final_comp` `CategoryTheory.Functor.final_op_of_initial` `CategoryTheory.Functor.final_of_isRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence`
`functorOp_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CostructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.op` `FintypeCat.toProfinite` `Opposite.op` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.instCategoryCostructuredArrow` `functorOp` `CategoryTheory.CostructuredArrow.homMk` `CategoryTheory.Functor.obj` `Opposite.unop` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π` `Quiver.Hom.unop` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.StructuredArrow.homMk`	—	—
`functorOp_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CostructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.op` `FintypeCat.toProfinite` `Opposite.op` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.instCategoryCostructuredArrow` `functorOp` `Opposite.unop` `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` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.toProfinite` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π`	`CategoryTheory.Functor.Initial` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow` `functor`	—	`CategoryTheory.Functor.initial_iff_of_isCofiltered` `CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty` `CategoryTheory.instIsCofilteredULiftHom` `CategoryTheory.instIsCofilteredULift` `Profinite.exists_hom` `CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_injective` `instFaithfulFintypeCatProfiniteToProfinite` `CategoryTheory.Epi.left_cancellation` `CategoryTheory.Functor.initial_of_equivalence_comp` `CategoryTheory.Equivalence.isEquivalence_inverse`
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.StructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `FintypeCat.toProfinite` `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` `CategoryTheory.StructuredArrow` `FintypeCat` `FintypeCat.instCategory` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `FintypeCat.toProfinite` `CategoryTheory.instCategoryStructuredArrow` `functor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π`	—	—

---

← Back to Index