Theorems · Definition · Lie groups

ProfiniteGrp.ProfiniteCompletion.quotientMap

{G : GrpCat} →
  {P : ProfiniteGrp.{u}} →
    (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) →
      (H : OpenNormalSubgroup ↑P.toProfinite.toTop) →
        FiniteGrp.of (↑G ⧸ (ProfiniteGrp.ProfiniteCompletion.preimage f H).toSubgroup) ⟶
          FiniteGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup)

The induced map on finite quotients coming from a morphism to P.

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Cited by

1 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound