The free pro-p group on no generators

The free pro-p group on an empty type is trivial. Its universal property makes every continuous endomorphism equal: two such maps agree on the empty set of generators. In particular it is topologically isomorphic to the one-element group.

This is the zero-generator case of the free pro-p construction used in finite-rank presentations. The argument works for any empty type and does not require p to be prime.

instance TauCeti.freeProP.instSubsingletonOfIsEmpty (p : ℕ) (X : Type u) [IsEmpty X] : Subsingleton (freeProP p X)

A free pro-p group on an empty type has only one element.

noncomputable def TauCeti.freeProP.equivPUnitOfIsEmpty (p : ℕ) (X : Type u) [IsEmpty X] : freeProP p X ≃ₜ* PUnit.{u_1 + 1}

The free pro-p group on an empty type is the one-element group, including its topology.

Equations

• TauCeti.freeProP.equivPUnitOfIsEmpty p X = ContinuousMulEquiv.ofUnique