Graphs over the range of a projection

A continuous map from the range of an idempotent continuous linear map into its kernel has an embedded graph. The projection is a continuous left inverse of its graph parameterization.

Main declarations

• ContinuousLinearMap.isEmbedding_graph: the graph parameterization over the range of a projection is an embedding.
• ContinuousLinearMap.graphHomeomorph: the part of the range of a projection lying in a set s is homeomorphic to the graph over it, with inverse given by the projection.
• ContinuousLinearMap.projectionGraphChart: the ambient coordinate change z ↦ z - g (P z) straightens the graph on an open cylinder over its parameter set.

theorem ContinuousLinearMap.isEmbedding_graph {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M] (P : M →L[R] M) (hP : IsIdempotentElem P) (g : M → M) (hPg : ∀ v ∈ Set.range ⇑P, P (g v) = 0) (hg : ContinuousOn g (Set.range ⇑P)) : Topology.IsEmbedding fun (v : ↑(Set.range ⇑P)) => ↑v + g ↑v

A graph over the range of a continuous projection is embedded when its vertical component lies in the kernel of the projection.

noncomputable def ContinuousLinearMap.graphHomeomorph {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M] (P : M →L[R] M) (hP : IsIdempotentElem P) (g : M → M) (hPg : ∀ v ∈ Set.range ⇑P, P (g v) = 0) (hg : ContinuousOn g (Set.range ⇑P)) (s : Set M) : ↑(Subtype.val ⁻¹' s) ≃ₜ ↑((fun (v : M) => v + g v) '' (Set.range ⇑P ∩ s))

The graph over the part of the range of a continuous projection lying in s is homeomorphic to that part, when the vertical component of the graph lies in the kernel of the projection.

Equations

• P.graphHomeomorph hP g hPg hg s = (Homeomorph.setCongr ⋯).trans ((⋯.homeomorphOfSubsetRange ⋯).trans (Homeomorph.setCongr ⋯))

@[simp]

theorem ContinuousLinearMap.coe_graphHomeomorph_apply {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M] (P : M →L[R] M) (hP : IsIdempotentElem P) (g : M → M) (hPg : ∀ v ∈ Set.range ⇑P, P (g v) = 0) (hg : ContinuousOn g (Set.range ⇑P)) (s : Set M) (v : ↑(Subtype.val ⁻¹' s)) : ↑((P.graphHomeomorph hP g hPg hg s) v) = ↑↑v + g ↑↑v

The graph homeomorphism sends v to v + g v.

@[simp]

theorem ContinuousLinearMap.coe_graphHomeomorph_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M] (P : M →L[R] M) (hP : IsIdempotentElem P) (g : M → M) (hPg : ∀ v ∈ Set.range ⇑P, P (g v) = 0) (hg : ContinuousOn g (Set.range ⇑P)) (s : Set M) (z : ↑((fun (v : M) => v + g v) '' (Set.range ⇑P ∩ s))) : ↑↑((P.graphHomeomorph hP g hPg hg s).symm z) = P ↑z

The inverse graph homeomorphism is given by the projection.

def ContinuousLinearMap.projectionGraphChart {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) : OpenPartialHomeomorph M M

The triangular ambient chart straightening a graph over the range of an idempotent continuous linear map. Its source and target are the cylinder over U. The coordinate change itself does not require idempotence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.projectionGraphChart_source {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) : (P.projectionGraphChart g hU hg hPg).source = ⇑P ⁻¹' U

@[simp]

theorem ContinuousLinearMap.projectionGraphChart_target {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) : (P.projectionGraphChart g hU hg hPg).target = ⇑P ⁻¹' U

@[simp]

theorem ContinuousLinearMap.projectionGraphChart_apply {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) (z : M) : ↑(P.projectionGraphChart g hU hg hPg) z = z - g (P z)

@[simp]

theorem ContinuousLinearMap.projectionGraphChart_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) (z : M) : ↑(P.projectionGraphChart g hU hg hPg).symm z = z + g (P z)

theorem ContinuousLinearMap.projectionGraphChart_mem_range_iff {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] (P : M →L[R] M) (g : M → M) {U : Set M} (hU : IsOpen U) (hg : ContinuousOn g (↑(↑P).range ∩ U)) (hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0) (hP : IsIdempotentElem P) {S : Set M} (hUS : U ⊆ S) (hPgS : ∀ v ∈ ↑(↑P).range ∩ S, P (g v) = 0) {z : M} (hz : P z ∈ U) : ↑(P.projectionGraphChart g hU hg hPg) z ∈ (↑P).range ↔ z ∈ (fun (v : M) => v + g v) '' (↑(↑P).range ∩ S)

On its source, the chart takes a graph precisely to the range of the projection. The graph may be defined over a larger parameter set S, for example a closed disk whose interior contains U.