Documentation Verification Report

Limits

📁 Source: Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

Statistics

Metric	Count
Definitions `cone`, `continuousMulEquivLimittoFiniteQuotientFunctor`, `diagram`, `isLimitCone`, `isoLimittoFiniteQuotientFunctor`, `proj`, `toFiniteQuotientFunctor`, `toLimit`, `toLimitFun`	9
Theorems `cone_pt`, `cone_π_app`, `denseRange_toLimit`, `diagram_map`, `diagram_obj`, `isIso_toLimit`, `toLimitFun_continuous`, `toLimit_injective`, `toLimit_surjective`	9
Total	18

ProfiniteGrp

Definitions

Name	Category	Theorems
`cone` 📖	CompOp	2 math math: `cone_pt`, `cone_π_app`
`continuousMulEquivLimittoFiniteQuotientFunctor` 📖	CompOp	—
`diagram` 📖	CompOp	9 math math: `toLimit_surjective`, `denseRange_toLimit`, `cone_pt`, `cone_π_app`, `toLimit_injective`, `toLimitFun_continuous`, `diagram_map`, `isIso_toLimit`, `diagram_obj`
`isLimitCone` 📖	CompOp	—
`isoLimittoFiniteQuotientFunctor` 📖	CompOp	—
`proj` 📖	CompOp	1 math math: `cone_π_app`
`toFiniteQuotientFunctor` 📖	CompOp	2 math math: `diagram_map`, `diagram_obj`
`toLimit` 📖	CompOp	4 math math: `toLimit_surjective`, `denseRange_toLimit`, `toLimit_injective`, `isIso_toLimit`
`toLimitFun` 📖	CompOp	1 math math: `toLimitFun_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `ProfiniteGrp` `instCategoryProfiniteGrp` `diagram` `cone`	—	—
`cone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `ProfiniteGrp` `instCategoryProfiniteGrp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `diagram` `CategoryTheory.Limits.Cone.π` `cone` `proj`	—	—
`denseRange_toLimit` 📖	mathematical	—	`DenseRange` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `limit` `OpenNormalSubgroup` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `diagram` `instTopologicalSpaceSubtype` `Subgroup` `Pi.group` `CategoryTheory.Functor.obj` `ProfiniteGrp` `instCategoryProfiniteGrp` `SetLike.instMembership` `Subgroup.instSetLike` `limitConePtAux` `Pi.topologicalSpace` `DFunLike.coe` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `Hom.hom` `toLimit`	—	`dense_iff_inter_open` `isOpen_pi_iff` `Subgroup.normal_iInf_normal` `OpenNormalSubgroup.isNormal'` `Subgroup.coe_iInf` `isOpen_iInter_of_finite` `Finite.of_fintype` `OpenSubgroup.isOpen'` `QuotientGroup.mk'_surjective` `iInf_le` `Set.mem_of_eq_of_mem`
`diagram_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `ProfiniteGrp` `instCategoryProfiniteGrp` `diagram` `FiniteGrp` `FiniteGrp.instCategory` `CategoryTheory.forget₂` `MonoidHom` `GrpCat.carrier` `FiniteGrp.toGrp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp` `ContinuousMonoidHom` `ContinuousMonoidHom.instFunLike` `instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `CategoryTheory.Functor.obj` `toFiniteQuotientFunctor`	—	—
`diagram_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `ProfiniteGrp` `instCategoryProfiniteGrp` `diagram` `FiniteGrp` `FiniteGrp.instCategory` `CategoryTheory.forget₂` `MonoidHom` `GrpCat.carrier` `FiniteGrp.toGrp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp` `ContinuousMonoidHom` `ContinuousMonoidHom.instFunLike` `instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `toFiniteQuotientFunctor`	—	—
`isIso_toLimit` 📖	mathematical	—	`CategoryTheory.IsIso` `ProfiniteGrp` `instCategoryProfiniteGrp` `limit` `OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `diagram` `toLimit`	—	`CategoryTheory.ConcreteCategory.isIso_iff_bijective` `instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `toLimit_injective` `toLimit_surjective`
`toLimitFun_continuous` 📖	mathematical	—	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `limit` `OpenNormalSubgroup` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `diagram` `instTopologicalSpaceSubtype` `Subgroup` `Pi.group` `CategoryTheory.Functor.obj` `ProfiniteGrp` `instCategoryProfiniteGrp` `SetLike.instMembership` `Subgroup.instSetLike` `limitConePtAux` `Pi.topologicalSpace` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `toLimitFun`	—	`continuous_induced_rng` `continuous_pi` `Set.biUnion_preimage_singleton` `isOpen_iUnion` `Set.ext` `QuotientGroup.out_eq'` `QuotientGroup.eq` `Set.mem_smul_set_iff_inv_smul_mem` `IsOpen.leftCoset` `IsTopologicalGroup.toContinuousMul` `topologicalGroup` `OpenSubgroup.isOpen'`
`toLimit_injective` 📖	mathematical	—	`TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `limit` `OpenNormalSubgroup` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `diagram` `DFunLike.coe` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `Hom.hom` `toLimit`	—	`MonoidHom.ker_eq_bot_iff` `Subgroup.eq_bot_iff_forall` `exist_openNormalSubgroup_sub_open_nhds_of_one` `topologicalGroup` `CompHausLike.is_compact` `Profinite.instTotallyDisconnectedSpaceCarrierToTop` `isOpen_compl_singleton` `TotallyDisconnectedSpace.t1Space` `Set.mem_compl_singleton_iff` `QuotientGroup.eq_one_iff`
`toLimit_surjective` 📖	mathematical	—	`TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `limit` `OpenNormalSubgroup` `group` `Preorder.smallCategory` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup` `diagram` `DFunLike.coe` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `Hom.hom` `toLimit`	—	`IsClosedMap.isClosed_range` `Continuous.isClosedMap` `CompHausLike.is_compact` `instT2SpaceSubtype` `Pi.t2Space` `CompHausLike.is_hausdorff` `ContinuousMonoidHom.continuous_toFun` `Set.range_eq_univ` `closure_eq_iff_isClosed` `Dense.closure_eq` `denseRange_toLimit`

---

← Back to Index