Conjugacies of flows #
This file collects general consequences of an inducing map that semiconjugates two flows. These lemmas transport asymptotic trajectory behavior, enabling stable and unstable sets to be transferred through coordinate conjugacies.
Main declarations #
Topology.IsInducing.tendsto_flow_iff: an inducing semiconjugacy transports convergence of flow trajectories in either direction.Homeomorph.tendsto_flow_iff: a homeomorphic semiconjugacy transports convergence of flow trajectories in either direction.Homeomorph.map_flow_symm: the inverse of a homeomorphic semiconjugacy satisfies the conjugacy equation in the reverse direction.
theorem
Topology.IsInducing.tendsto_flow_iff
{τ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[TopologicalSpace τ]
[TopologicalSpace α]
[TopologicalSpace β]
[AddMonoid τ]
{φ : Flow τ α}
{ψ : Flow τ β}
{f : α → β}
(hf : IsInducing f)
(hconj : Flow.IsSemiconjugacy f φ ψ)
{l : Filter τ}
{x y : α}
:
Filter.Tendsto (fun (t : τ) => ψ.toFun t (f y)) l (nhds (f x)) ↔ Filter.Tendsto (fun (t : τ) => φ.toFun t y) l (nhds x)
An inducing semiconjugacy transports convergence of flow trajectories in either direction.
theorem
Homeomorph.tendsto_flow_iff
{τ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[TopologicalSpace τ]
[TopologicalSpace α]
[TopologicalSpace β]
[AddMonoid τ]
{φ : Flow τ α}
{ψ : Flow τ β}
(e : α ≃ₜ β)
(hconj : Flow.IsSemiconjugacy (⇑e) φ ψ)
{l : Filter τ}
{x y : α}
:
Filter.Tendsto (fun (t : τ) => ψ.toFun t (e y)) l (nhds (e x)) ↔ Filter.Tendsto (fun (t : τ) => φ.toFun t y) l (nhds x)
A homeomorphic semiconjugacy transports convergence of flow trajectories in either direction.
theorem
Homeomorph.map_flow_symm
{τ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[TopologicalSpace τ]
[TopologicalSpace α]
[TopologicalSpace β]
[AddMonoid τ]
{φ : Flow τ α}
{ψ : Flow τ β}
(e : α ≃ₜ β)
(hconj : Flow.IsSemiconjugacy (⇑e) φ ψ)
(t : τ)
(y : β)
:
The inverse of a homeomorphic semiconjugacy is a semiconjugacy in the reverse direction.