Free pro-p groups across universes

The free pro-p group freeProP p X lives in the universe of its generating type X, and its universal property TauCeti.freeProP.lift only reaches pro-p groups in that universe. A topologically finitely generated pro-p group G : Type u therefore gets its minimal presentations on generating types in Type u, such as ULift.{u} (Fin n), while the normal-form relators of the Demushkin classification are words in freeProP p (Fin n). This file identifies the two free pro-p groups: TauCeti.freeProP.uliftEquiv is the topological isomorphism freeProP p (ULift X) ≃ₜ* freeProP p X matching the generator at ⟨x⟩ with the generator at x.

Main declarations

• TauCeti.freeProP.uliftEquiv: the topological isomorphism freeProP p (ULift X) ≃ₜ* freeProP p X.
• TauCeti.freeProP.uliftEquiv_of, TauCeti.freeProP.uliftEquiv_symm_of: it matches the generators.

noncomputable def TauCeti.freeProP.uliftEquiv (p : ℕ) (X : Type u) : freeProP p (ULift.{v, u} X) ≃ₜ* freeProP p X

Free pro-p groups across universes. The free pro-p group on the universe lift of X is topologically isomorphic to the free pro-p group on X, by the isomorphism matching the generator at ⟨x⟩ with the generator at x.

Equations

• TauCeti.freeProP.uliftEquiv p X = (MulEquiv.ofBijective ↑(TauCeti.freeProP.uliftDown✝ p X) ⋯).toContinuousMulEquiv ⋯

@[simp]

theorem TauCeti.freeProP.uliftEquiv_of (p : ℕ) (X : Type u) (x : ULift.{v, u} X) : (uliftEquiv p X) (of x) = of x.down

The universe-lift isomorphism carries the generator at ⟨x⟩ to the generator at x.

@[simp]

theorem TauCeti.freeProP.uliftEquiv_symm_of (p : ℕ) (X : Type u) (x : X) : (uliftEquiv p X).symm (of x) = of { down := x }

The inverse of the universe-lift isomorphism carries the generator at x to the generator at ⟨x⟩.