Mathlib Map

Theorems · Theorem · Lie groups

ProfiniteGrp.ofHom_id

∀ {X : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X] [inst_3 : CompactSpace X]
  [inst_4 : TotallyDisconnectedSpace X],
  ProfiniteGrp.ofHom (ContinuousMonoidHom.id X) = CategoryTheory.CategoryStruct.id (ProfiniteGrp.of X)
Defined in
Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Cited by
0 results in Mathlib
Foundations
Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupTopologicalSpaceIsTopologicalGroupCompactSpaceTotallyDisconnectedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Quiver.Hom · cited by 32603Quiver.HomTopologicalSpace · cited by 24529TopologicalSpaceGroup · cited by 6238GroupCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCompactSpace · cited by 593CompactSpaceIsTopologicalGroup · cited by 469IsTopologicalGroupTotallyDisconnectedSpace · cited by 295TotallyDisconnectedSpaceProfiniteGrp · cited by 47ProfiniteGrpContinuousMonoidHom.id · cited by 8ContinuousMonoidHom.idProfiniteGrp.of · cited by 8ProfiniteGrp.ofProfiniteGrp.ofHom · cited by 5ProfiniteGrp.ofHomProfiniteGrp.ofHom_idCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.