Documentation Verification Report

Completion

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

Statistics

Metric	Count
Definitions `toFiniteIndexNormalAddSubgroup`, `toFiniteIndexNormalSubgroup`, `adjunction`, `completion`, `diagram`, `eta`, `etaFn`, `finiteGrpDiagram`, `homEquiv`, `preimage`, `quotientMap`, `profiniteCompletion`	12
Theorems `toFiniteIndexNormalAddSubgroup_injective`, `toFiniteIndexNormalAddSubgroup_mono`, `toFiniteIndexNormalSubgroup_injective`, `toFiniteIndexNormalSubgroup_mono`, `denseRange`, `etaFn_injective_iff_residuallyFinite`, `lift_eta`, `lift_eta_assoc`, `lift_unique`, `mono_eta_iff_residuallyFinite`, `preimage_le`, `profiniteCompletion_map`, `profiniteCompletion_obj`	13
Total	25

OpenNormalAddSubgroup

Definitions

Name	Category	Theorems
`toFiniteIndexNormalAddSubgroup` 📖	CompOp	2 math math: `toFiniteIndexNormalAddSubgroup_injective`, `toFiniteIndexNormalAddSubgroup_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFiniteIndexNormalAddSubgroup_injective` 📖	mathematical	—	`OpenNormalAddSubgroup` `FiniteIndexNormalAddSubgroup` `toFiniteIndexNormalAddSubgroup`	—	`toAddSubgroup_injective`
`toFiniteIndexNormalAddSubgroup_mono` 📖	mathematical	`OpenNormalAddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderOpenNormalAddSubgroup`	`FiniteIndexNormalAddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `FiniteIndexNormalAddSubgroup.instPartialOrderFiniteIndexNormalAddSubgroup` `toFiniteIndexNormalAddSubgroup`	—	—

OpenNormalSubgroup

Definitions

Name	Category	Theorems
`toFiniteIndexNormalSubgroup` 📖	CompOp	2 math math: `toFiniteIndexNormalSubgroup_injective`, `toFiniteIndexNormalSubgroup_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFiniteIndexNormalSubgroup_injective` 📖	mathematical	—	`OpenNormalSubgroup` `FiniteIndexNormalSubgroup` `toFiniteIndexNormalSubgroup`	—	`toSubgroup_injective`
`toFiniteIndexNormalSubgroup_mono` 📖	mathematical	`OpenNormalSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderOpenNormalSubgroup`	`FiniteIndexNormalSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup` `toFiniteIndexNormalSubgroup`	—	—

ProfiniteGrp

Definitions

Name	Category	Theorems
`profiniteCompletion` 📖	CompOp	2 math math: `profiniteCompletion_map`, `profiniteCompletion_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`profiniteCompletion_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `GrpCat` `GrpCat.instCategory` `ProfiniteGrp` `instCategoryProfiniteGrp` `profiniteCompletion` `ProfiniteCompletion.lift` `ProfiniteCompletion.completion` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `GrpCat.of` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `toProfinite` `group` `ProfiniteCompletion.eta`	—	—
`profiniteCompletion_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `GrpCat` `GrpCat.instCategory` `ProfiniteGrp` `instCategoryProfiniteGrp` `profiniteCompletion` `ProfiniteCompletion.completion`	—	—

ProfiniteGrp.ProfiniteCompletion

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	—
`completion` 📖	CompOp	7 math math: `lift_eta`, `lift_eta_assoc`, `denseRange`, `etaFn_injective_iff_residuallyFinite`, `ProfiniteGrp.profiniteCompletion_map`, `mono_eta_iff_residuallyFinite`, `ProfiniteGrp.profiniteCompletion_obj`
`diagram` 📖	CompOp	—
`eta` 📖	CompOp	4 math math: `lift_eta`, `lift_eta_assoc`, `ProfiniteGrp.profiniteCompletion_map`, `mono_eta_iff_residuallyFinite`
`etaFn` 📖	CompOp	2 math math: `denseRange`, `etaFn_injective_iff_residuallyFinite`
`finiteGrpDiagram` 📖	CompOp	—
`homEquiv` 📖	CompOp	—
`preimage` 📖	CompOp	1 math math: `preimage_le`
`quotientMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denseRange` 📖	mathematical	—	`DenseRange` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `GrpCat.carrier` `etaFn`	—	`dense_iff_inter_open` `isOpen_pi_iff` `Set.mem_preimage` `Subgroup.normal_iInf_normal` `FiniteIndexNormalSubgroup.instNormal` `Subgroup.finiteIndex_iInf` `Finite.of_fintype` `FiniteIndexNormalSubgroup.instFiniteIndex` `QuotientGroup.mk'_surjective` `iInf_le` `Set.mem_of_eq_of_mem`
`etaFn_injective_iff_residuallyFinite` 📖	mathematical	—	`GrpCat.carrier` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `etaFn` `Group.ResiduallyFinite` `GrpCat.str`	—	`GrpCat.mono_iff_injective` `mono_eta_iff_residuallyFinite`
`lift_eta` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `GrpCat` `CategoryTheory.Category.toCategoryStruct` `GrpCat.instCategory` `GrpCat.of` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `ProfiniteGrp.group` `CategoryTheory.Functor.obj` `ProfiniteGrp` `instCategoryProfiniteGrp` `CategoryTheory.forget₂` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier` `eta` `CategoryTheory.Functor.map` `lift`	—	`CategoryTheory.Iso.cancel_iso_hom_right` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap` `CategoryTheory.Iso.inv_hom_id`
`lift_eta_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `GrpCat` `CategoryTheory.Category.toCategoryStruct` `GrpCat.instCategory` `GrpCat.of` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `ProfiniteGrp.group` `eta` `CategoryTheory.Functor.obj` `ProfiniteGrp` `instCategoryProfiniteGrp` `CategoryTheory.forget₂` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier` `CategoryTheory.Functor.map` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_eta`
`lift_unique` 📖	—	`CategoryTheory.CategoryStruct.comp` `GrpCat` `CategoryTheory.Category.toCategoryStruct` `GrpCat.instCategory` `GrpCat.of` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `ProfiniteGrp.group` `CategoryTheory.Functor.obj` `ProfiniteGrp` `instCategoryProfiniteGrp` `CategoryTheory.forget₂` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ContinuousMonoidHom.instFunLike` `instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier` `eta` `CategoryTheory.Functor.map`	—	—	`ProfiniteGrp.hom_ext` `ContinuousMonoidHom.ext` `DenseRange.equalizer` `CompHausLike.is_hausdorff` `denseRange` `ContinuousMonoidHom.continuous_toFun` `CategoryTheory.ConcreteCategory.congr_hom`
`mono_eta_iff_residuallyFinite` 📖	mathematical	—	`CategoryTheory.Mono` `GrpCat` `GrpCat.instCategory` `GrpCat.of` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `completion` `ProfiniteGrp.group` `eta` `Group.ResiduallyFinite` `GrpCat.carrier` `GrpCat.str`	—	`GrpCat.mono_iff_injective` `injective_iff_map_eq_one` `MonoidHom.instMonoidHomClass` `Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup` `QuotientGroup.eq_one_iff` `FiniteIndexNormalSubgroup.instNormal`
`preimage_le` 📖	mathematical	`OpenNormalSubgroup` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `ProfiniteGrp.toProfinite` `ProfiniteGrp.group` `Preorder.toLE` `PartialOrder.toPreorder` `OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup`	`FiniteIndexNormalSubgroup` `GrpCat.carrier` `GrpCat.str` `Preorder.toLE` `PartialOrder.toPreorder` `FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup` `preimage`	—	`FiniteIndexNormalSubgroup.comap_mono`

---

← Back to Index