Theorems · Definition · Lie groups

ProfiniteAddGrp.ofHom

{X Y : Type u} →
  [inst : AddGroup X] →
    [inst_1 : TopologicalSpace X] →
      [inst_2 : IsTopologicalAddGroup X] →
        [inst_3 : CompactSpace X] →
          [inst_4 : TotallyDisconnectedSpace X] →
            [inst_5 : AddGroup Y] →
              [inst_6 : TopologicalSpace Y] →
                [inst_7 : IsTopologicalAddGroup Y] →
                  [inst_8 : CompactSpace Y] →
                    [inst_9 : TotallyDisconnectedSpace Y] → (X →ₜ+ Y) → (ProfiniteAddGrp.of X ⟶ ProfiniteAddGrp.of Y)

Typecheck a ContinuousAddMonoidHom as a morphism in ProfiniteAddGrp.

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpaceAddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpace