Commit 2026-02-07 15:49 66cbf962

View on Github →

feat: Profinite completion of groups (#34893)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/FiniteIndexNormalSubgroup.lean

added structure FiniteIndexNormalAddSubgroup

added def FiniteIndexNormalSubgroup.comap

added theorem FiniteIndexNormalSubgroup.comap_comp

added theorem FiniteIndexNormalSubgroup.comap_id

added theorem FiniteIndexNormalSubgroup.comap_mono

added def FiniteIndexNormalSubgroup.ofSubgroup

added theorem FiniteIndexNormalSubgroup.toSubgroup_comap

added theorem FiniteIndexNormalSubgroup.toSubgroup_injective

added theorem FiniteIndexNormalSubgroup.toSubgroup_ofSubgroup

added structure FiniteIndexNormalSubgroup

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

added def ProfiniteGrp.ofFiniteGrpHom

Created Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean

added def OpenNormalSubgroup.toFiniteIndexNormalSubgroup

added theorem OpenNormalSubgroup.toFiniteIndexNormalSubgroup_injective

added theorem OpenNormalSubgroup.toFiniteIndexNormalSubgroup_mono

added def ProfiniteGrp.ProfiniteCompletion.adjunction

added def ProfiniteGrp.ProfiniteCompletion.completion

added theorem ProfiniteGrp.ProfiniteCompletion.denseRange

added def ProfiniteGrp.ProfiniteCompletion.diagram

added def ProfiniteGrp.ProfiniteCompletion.eta

added def ProfiniteGrp.ProfiniteCompletion.etaFn

added def ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram

added def ProfiniteGrp.ProfiniteCompletion.homEquiv

added def ProfiniteGrp.ProfiniteCompletion.lift

added theorem ProfiniteGrp.ProfiniteCompletion.lift_eta

added theorem ProfiniteGrp.ProfiniteCompletion.lift_unique

added def ProfiniteGrp.ProfiniteCompletion.preimage

added theorem ProfiniteGrp.ProfiniteCompletion.preimage_le

added def ProfiniteGrp.ProfiniteCompletion.quotientMap

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

added def ProfiniteGrp.cone

added def ProfiniteGrp.diagram

added def ProfiniteGrp.proj

modified def ProfiniteGrp.toLimit

added def ProfiniteGrp.toLimitFun

added theorem ProfiniteGrp.toLimitFun_continuous

deleted def ProfiniteGrp.toLimit_fun

deleted theorem ProfiniteGrp.toLimit_fun_continuous

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean