A semiconjugacy is a map between two state spaces that respects one update step. A conjugacy adds an inverse, so the change of coordinates can be undone.

Let \(f : X \to X\) and \(g : Y \to Y\). A map \(\varphi : X \to Y\) semiconjugates \(f\) to \(g\) when

\[ \varphi(f(x))=g(\varphi(x)) \qquad\text{for every }x\in X. \]

This relation is directional. It transports a source orbit to a target orbit, but it does not promise that the source state can be reconstructed.

Start with a quarter-turn factor

Take four compass directions and update them by a clockwise quarter turn:

\[ \text{north}\mapsto\text{east}\mapsto\text{south} \mapsto\text{west}\mapsto\text{north}. \]

Project north and south to the vertical axis, and east and west to the horizontal axis. The target update toggles its axis. Updating and then projecting agrees with projecting and then toggling in all four cases.

The projection is onto: each target axis has a source direction. It is not one-to-one: north and south share an image, as do east and west. The target retains axis alternation and loses orientation.

The left panel merges north and south into vertical and east and west into horizontal; the right panel maps vertical and horizontal bijectively to false and true with arrows in both directions.
FigureThe inverse boundary: semiconjugacy may identify different source states. Conjugacy requires an invertible map. Topological conjugacy adds continuity of both the map and its inverse; it still does not claim that numerical distances are preserved.

One step gives every forward iterate

If the one-step square commutes, then for every \(n \in \mathbb N\),

\[ \varphi(f^n(x))=g^n(\varphi(x)). \]

This follows by induction. The case (n=0) uses identity iterates. The next case applies the one-step equation after the preceding iterate equality.

The natural-number clock is unchanged. Semiconjugacy is not the broader idea of orbit equivalence with a time reparameterization.

Add continuity and surjectivity separately

The algebraic equation alone has no topology. A topological semiconjugacy adds continuity of \(\varphi\). Continuity is what sends a convergent source orbit to a convergent target orbit.

A topological factor map adds surjectivity as well. Surjectivity says that every target state has at least one source representative. It is needed when a transported conclusion quantifies over every target start, such as global attraction.

Surjectivity does not recover information. The quarter-turn projection is surjective and still merges opposite directions.

Conjugacy is reversible

A topological conjugacy uses a homeomorphism \(e : X \simeq_{\mathrm{top}} Y\): a bijection whose forward and inverse maps are continuous. It satisfies

\[ e(f(x))=g(e(x)). \]

The inverse homeomorphism semiconjugates \(g\) back to \(f\). This gives two-way statements for corresponding fixed points, specified periods, point attraction, basins, and local or global attracting fixed points in the project module.

The word “specified” matters for periods. IsPeriodicPt f n p says that \(n\) is a period of \(p\), not necessarily its least positive period. A many-to-one factor can collapse a least period even though it maps every specified-period point forward.

In Lean

Mathlib supplies the algebraic predicate; the project adds the topological packages.

One idea, three languages Read across, then read the syntax map
A human says
The coordinate map sends one source update to one target update.
On paper
\(\varphi(f(x))=g(\varphi(x))\) for every \(x\in X\).
In Lean
Function.Semiconj φ f g :=\n  ∀ x, φ (f x) = g (φ x)
Syntax map
φ maps source states to target states. f and g are the two update rules. The proposition can be applied to x to obtain the displayed equality.

The topological interfaces are:

def IsTopologicalSemiconjugacy (φ : X → Y) (f : X → X) (g : Y → Y) : Prop :=
  Continuous φ ∧ Function.Semiconj φ f g

def IsTopologicalFactorMap (φ : X → Y) (f : X → X) (g : Y → Y) : Prop :=
  IsTopologicalSemiconjugacy φ f g ∧ Function.Surjective φ

def IsTopologicalConjugacy (e : X ≃ₜ Y) (f : X → X) (g : Y → Y) : Prop :=
  Function.Semiconj e f g

X ≃ₜ Y is Mathlib’s homeomorphism type. Its data include the function, its inverse, both inverse identities, and continuity in both directions.

Try it in the repository

Create a reader worksheet containing:

import NonlinearDynamics.Deterministic.Discrete.Conjugacy

#check Function.Semiconj
#check IsTopologicalSemiconjugacy
#check IsTopologicalFactorMap
#check IsTopologicalConjugacy
#check semiconj_iterate_apply
#check IsTopologicalConjugacy.isAttractedTo_iff

This is a full project check using pinned Lean and Mathlib dependencies. Initial setup may require substantial disk space and build time.

Try it in the repository NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean
The copied checks form a reader worksheet. The authoritative source is NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean; the command below checks the complete module with the repository’s pinned environment.
Full project check, from the repository root
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Deterministic/Discrete/Conjugacy.lean

Resource note: this exact file uses the repository's pinned Lean and Mathlib dependencies. Initial project setup can require substantial disk space and build time. For a lightweight first step on macOS or Linux, use the page's standalone Lean-core or Std tutorial.

For a standalone tutorial, run the quarter-turn-factor.lean file in the paired Deep Dive. It imports only Std, checks the four-state factor, and constructs an invertible encoding of the two-axis system.

Boundaries that prevent common mistakes

  • A semiconjugacy need not be injective or surjective.
  • A factor map is surjective but may remain many-to-one.
  • Orbit transport is forward unless inverse data are supplied.
  • A bijection without continuity does not transport topological limits.
  • A homeomorphism preserves topology, not a selected metric or convergence rate.
  • A specified period need not be the least positive period.
  • Dynamical conjugacy is not matrix similarity, complex conjugation, or unitary conjugation.

This chapter establishes no preservation theorem for forward stability , entropy, mixing, transitivity, chaos, symbolic coding, structural robustness, measure conjugacy, stochastic systems, or differential equations. It gives no algorithm for finding a conjugacy.

Continue with Conjugacy, Semiconjugacy, and Orbit Transport in Discrete Time or inspect the declaration-complete Research Note. Then see bifurcation point for the parameter-space use of conjugacy invariance.

References