Transporting graphs along a flow #
A graph over the range of an idempotent continuous linear map is embedded. Each fixed-time map of a flow is a homeomorphism, so translating such a graph and transporting it along the flow keeps it embedded. This is the topological part of transporting local stable and unstable disks along orbits.
Main declarations #
Flow.isEmbedding_graph: flowing a graph over the range of an idempotent continuous linear map gives another topological embedding.
theorem
Flow.isEmbedding_graph
{E : Type u_1}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[Module ℝ E]
(φ : Flow ℝ E)
(P : E →L[ℝ] E)
(hP : IsIdempotentElem P)
(g : E → E)
(hPg : ∀ v ∈ (↑P).range, P (g v) = 0)
(hg : ContinuousOn g ↑(↑P).range)
(x : E)
(t : ℝ)
:
Topology.IsEmbedding fun (v : ↥(↑P).range) => φ.toFun t (x + (↑v + g ↑v))
A graph over the range of an idempotent continuous linear map remains embedded after translation and transport by any fixed time of a flow.