Semiconjugacy of homeomorphisms

This file relates integer powers of homeomorphisms to integer powers of their underlying permutations. In particular, a map intertwining two homeomorphisms also intertwines all of their integer powers.

Main declarations

• Homeomorph.coe_zpow: the underlying function of a power of a homeomorphism is the underlying function of the corresponding power of its underlying equivalence.
• Function.Semiconj.homeomorph_zpow_right: semiconjugacy of homeomorphisms is preserved by integer powers.

theorem Homeomorph.coe_zpow {X : Type u_1} [TopologicalSpace X] (f : X ≃ₜ X) (n : ℤ) : ⇑(f ^ n) = ⇑(f.toEquiv ^ n)

The underlying function of an integer power of a homeomorphism is the underlying function of the corresponding power of its underlying equivalence.

theorem Function.Semiconj.homeomorph_zpow_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X ≃ₜ X} {g : Y ≃ₜ Y} {u : X → Y} (h : Semiconj u ⇑f ⇑g) (n : ℤ) : Semiconj u ⇑(f ^ n) ⇑(g ^ n)

A map intertwining two homeomorphisms also intertwines all of their integer powers.