Coherent nonlinear maps on completed normed direct limits

A coherent family of nonexpansive maps between two isometric directed systems induces a nonexpansive map between their completed normed direct limits. Linearity of the stage maps is neither assumed nor used.

theorem ScottishBook155.CompletedLimitMap.sourceLinearDirectedSystem {ι : Type u} [LinearOrder ι] (M : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] : DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(NormedDirectLimit.linearMap M eM x1 x2 x3)

theorem ScottishBook155.CompletedLimitMap.targetLinearDirectedSystem {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] : DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(NormedDirectLimit.linearMap N eN x1 x2 x3)

@[reducible, inline]

abbrev ScottishBook155.CompletedLimitMap.Source {ι : Type u} [LinearOrder ι] (M : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) : Type u

The normed direct limit of the source spaces before completion.

Equations

• ScottishBook155.CompletedLimitMap.Source M eM = ScottishBook155.NormedDirectLimit.Carrier M eM

@[reducible, inline]

abbrev ScottishBook155.CompletedLimitMap.Target {ι : Type u} [LinearOrder ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) : Type u

The normed direct limit of the target spaces before completion.

Equations

• ScottishBook155.CompletedLimitMap.Target N eN = ScottishBook155.NormedDirectLimit.Carrier N eN

@[reducible, inline]

abbrev ScottishBook155.CompletedLimitMap.CompletedSource {ι : Type u} [LinearOrder ι] [Nonempty ι] (M : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] : Type u

The completion of the normed direct limit of the source spaces.

Equations

• ScottishBook155.CompletedLimitMap.CompletedSource M eM = ScottishBook155.NormedDirectLimit.CompletedCarrier M eM

@[reducible, inline]

abbrev ScottishBook155.CompletedLimitMap.CompletedTarget {ι : Type u} [LinearOrder ι] [Nonempty ι] (N : ι → Type u) [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] : Type u

The completion of the normed direct limit of the target spaces.

Equations

• ScottishBook155.CompletedLimitMap.CompletedTarget N eN = ScottishBook155.NormedDirectLimit.CompletedCarrier N eN

theorem ScottishBook155.CompletedLimitMap.target_of_eq_of_source_of_eq {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) {i j : ι} {x : M i} {y : M j} (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (h : (NormedDirectLimit.of M eM i) x = (NormedDirectLimit.of M eM j) y) : (NormedDirectLimit.of N eN i) (V i x) = (NormedDirectLimit.of N eN j) (V j y)

Equal source representatives have equal images in the target direct limit.

noncomputable def ScottishBook155.CompletedLimitMap.algebraicMap {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (z : Source M eM) : Target N eN

The coherent map on the algebraic source direct limit.

Equations

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

theorem ScottishBook155.CompletedLimitMap.algebraicMap_of {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (i : ι) (x : M i) : algebraicMap M N eM eN V ((Module.DirectLimit.of ℝ ι M (NormedDirectLimit.linearMap M eM) i) x) = (Module.DirectLimit.of ℝ ι N (NormedDirectLimit.linearMap N eN) i) (V i x)

theorem ScottishBook155.CompletedLimitMap.algebraicMap_dist_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) (z w : Source M eM) : dist (algebraicMap M N eM eN V z) (algebraicMap M N eM eN V w) ≤ dist z w

theorem ScottishBook155.CompletedLimitMap.algebraicMap_lipschitz {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) : LipschitzWith 1 (algebraicMap M N eM eN V)

noncomputable def ScottishBook155.CompletedLimitMap.completedMap {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) : CompletedSource M eM → CompletedTarget N eN

The coherent nonexpansive map extended to the completed normed direct limits.

Equations

• ScottishBook155.CompletedLimitMap.completedMap M N eM eN V = UniformSpace.Completion.extension (UniformSpace.Completion.coe' ∘ ScottishBook155.CompletedLimitMap.algebraicMap M N eM eN V)

theorem ScottishBook155.CompletedLimitMap.completedMap_lipschitz {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) : LipschitzWith 1 (completedMap M N eM eN V)

theorem ScottishBook155.CompletedLimitMap.completedMap_completedOf {ι : Type u} [LinearOrder ι] [Nonempty ι] (M N : ι → Type u) [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] [(i : ι) → NormedAddCommGroup (N i)] [(i : ι) → NormedSpace ℝ (N i)] (eM : (i j : ι) → i ≤ j → M i →ₗᵢ[ℝ] M j) (eN : (i j : ι) → i ≤ j → N i →ₗᵢ[ℝ] N j) [DirectedSystem M fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eM x1 x2 x3)] [DirectedSystem N fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(eN x1 x2 x3)] (V : (i : ι) → M i → N i) (hV : ∀ (i j : ι) (hij : i ≤ j) (x : M i), V j ((eM i j hij) x) = (eN i j hij) (V i x)) (hLip : ∀ (i : ι) (x y : M i), dist (V i x) (V i y) ≤ dist x y) (i : ι) (x : M i) : completedMap M N eM eN V ((NormedDirectLimit.completedOf M eM i) x) = (NormedDirectLimit.completedOf N eN i) (V i x)