Normed direct limits of isometric systems

Mathlib supplies the algebraic direct limit of modules. For a directed system whose transition maps are linear isometries, this file equips that algebraic direct limit with the unique norm making every canonical map isometric.

@[reducible, inline]

abbrev ScottishBook155.NormedDirectLimit.linearMap {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) (i j : ι) (h : i ≤ j) : G i →ₗ[ℝ] G j

The linear map underlying an isometric transition in the direct system.

Equations

• ScottishBook155.NormedDirectLimit.linearMap G f i j h = (f i j h).toLinearMap

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

@[reducible, inline]

abbrev ScottishBook155.NormedDirectLimit.Carrier {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) : Type u

The underlying algebraic direct limit.

Equations

• ScottishBook155.NormedDirectLimit.Carrier G f = Module.DirectLimit G (ScottishBook155.NormedDirectLimit.linearMap G f)

theorem ScottishBook155.NormedDirectLimit.norm_eq_of_of_eq {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {i j : ι} {x : G i} {y : G j} (h : (Module.DirectLimit.of ℝ ι G (linearMap G f) i) x = (Module.DirectLimit.of ℝ ι G (linearMap G f) j) y) : ‖x‖ = ‖y‖

Equal representatives in an isometric direct system have equal norms.

noncomputable def ScottishBook155.NormedDirectLimit.reprIndex {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) (z : Carrier G f) : ι

A chosen component containing a representative of a direct-limit element.

Equations

• ScottishBook155.NormedDirectLimit.reprIndex G f z = Classical.choose ⋯

noncomputable def ScottishBook155.NormedDirectLimit.reprValue {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) (z : Carrier G f) : G (reprIndex G f z)

A chosen representative in reprIndex.

Equations

• ScottishBook155.NormedDirectLimit.reprValue G f z = Classical.choose ⋯

theorem ScottishBook155.NormedDirectLimit.repr_spec {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) (z : Carrier G f) : (Module.DirectLimit.of ℝ ι G (linearMap G f) (reprIndex G f z)) (reprValue G f z) = z

noncomputable def ScottishBook155.NormedDirectLimit.limitNorm {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) (z : Carrier G f) : ℝ

The norm of a direct-limit element, computed from any representative.

Equations

• ScottishBook155.NormedDirectLimit.limitNorm G f z = ‖ScottishBook155.NormedDirectLimit.reprValue G f z‖

theorem ScottishBook155.NormedDirectLimit.limitNorm_of {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (i : ι) (x : G i) : limitNorm G f ((Module.DirectLimit.of ℝ ι G (linearMap G f) i) x) = ‖x‖

noncomputable def ScottishBook155.NormedDirectLimit.addGroupNorm {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] : AddGroupNorm (Carrier G f)

The additive norm induced on the algebraic direct limit.

Equations

• ScottishBook155.NormedDirectLimit.addGroupNorm G f = { toFun := ScottishBook155.NormedDirectLimit.limitNorm G f, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }

@[instance_reducible]

noncomputable instance ScottishBook155.NormedDirectLimit.normedAddCommGroup {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] : NormedAddCommGroup (Carrier G f)

Equations

• ScottishBook155.NormedDirectLimit.normedAddCommGroup G f = (ScottishBook155.NormedDirectLimit.addGroupNorm G f).toNormedAddCommGroup

@[instance_reducible]

noncomputable instance ScottishBook155.NormedDirectLimit.normedSpace {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] : NormedSpace ℝ (Carrier G f)

Equations

• ScottishBook155.NormedDirectLimit.normedSpace G f = { toModule := Module.DirectLimit.module G (ScottishBook155.NormedDirectLimit.linearMap G f), norm_smul_le := ⋯ }

noncomputable def ScottishBook155.NormedDirectLimit.of {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (i : ι) : G i →ₗᵢ[ℝ] Carrier G f

Every canonical component map is a linear isometry.

Equations

• ScottishBook155.NormedDirectLimit.of G f i = { toLinearMap := Module.DirectLimit.of ℝ ι G (ScottishBook155.NormedDirectLimit.linearMap G f) i, norm_map' := ⋯ }

theorem ScottishBook155.NormedDirectLimit.of_f {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {i j : ι} (hij : i ≤ j) (x : G i) : (of G f j) ((f i j hij) x) = (of G f i) x

Transition maps have the same image in the algebraic normed direct limit.

@[reducible, inline]

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

The completed normed direct limit.

Equations

• ScottishBook155.NormedDirectLimit.CompletedCarrier G f = UniformSpace.Completion (ScottishBook155.NormedDirectLimit.Carrier G f)

noncomputable def ScottishBook155.NormedDirectLimit.completedOf {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (i : ι) : G i →ₗᵢ[ℝ] CompletedCarrier G f

The canonical isometric embedding of a component into the completed direct limit.

Equations

• ScottishBook155.NormedDirectLimit.completedOf G f i = UniformSpace.Completion.toComplₗᵢ.comp (ScottishBook155.NormedDirectLimit.of G f i)

@[simp]

theorem ScottishBook155.NormedDirectLimit.completedOf_apply {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (i : ι) (x : G i) : (completedOf G f i) x = ↑((of G f i) x)

theorem ScottishBook155.NormedDirectLimit.completedOf_f {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {i j : ι} (hij : i ≤ j) (x : G i) : (completedOf G f j) ((f i j hij) x) = (completedOf G f i) x

Transition maps have the same image in the completed direct limit.

noncomputable def ScottishBook155.NormedDirectLimit.algebraicLiftLinear {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) : Carrier G f →ₗ[ℝ] H

The coherent linear map on the algebraic normed direct limit.

Equations

• ScottishBook155.NormedDirectLimit.algebraicLiftLinear G f g hg = Module.DirectLimit.lift ℝ ι G (ScottishBook155.NormedDirectLimit.linearMap G f) (fun (i : ι) => ↑(g i)) hg

theorem ScottishBook155.NormedDirectLimit.algebraicLiftLinear_of {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i) : (algebraicLiftLinear G f g hg) ((of G f i) x) = (g i) x

theorem ScottishBook155.NormedDirectLimit.algebraicLiftLinear_norm_le {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (C : ℝ) (hC : ∀ (i : ι) (x : G i), ‖(g i) x‖ ≤ C * ‖x‖) (z : Carrier G f) : ‖(algebraicLiftLinear G f g hg) z‖ ≤ C * ‖z‖

A uniform componentwise bound descends to the algebraic direct limit.

noncomputable def ScottishBook155.NormedDirectLimit.algebraicLift {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (C : ℝ) (hC : ∀ (i : ι) (x : G i), ‖(g i) x‖ ≤ C * ‖x‖) : Carrier G f →L[ℝ] H

The bounded coherent map on the algebraic direct limit.

Equations

• ScottishBook155.NormedDirectLimit.algebraicLift G f g hg C hC = (ScottishBook155.NormedDirectLimit.algebraicLiftLinear G f g hg).mkContinuous C ⋯

noncomputable def ScottishBook155.NormedDirectLimit.completedLift {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (C : ℝ) (hC : ∀ (i : ι) (x : G i), ‖(g i) x‖ ≤ C * ‖x‖) : CompletedCarrier G f →L[ℝ] H

A bounded coherent family extends uniquely over the completed direct limit.

Equations

• ScottishBook155.NormedDirectLimit.completedLift G f g hg C hC = (ScottishBook155.NormedDirectLimit.algebraicLift G f g hg C hC).extend UniformSpace.Completion.toComplL

theorem ScottishBook155.NormedDirectLimit.completedLift_completedOf {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (C : ℝ) (hC : ∀ (i : ι) (x : G i), ‖(g i) x‖ ≤ C * ‖x‖) (i : ι) (x : G i) : (completedLift G f g hg C hC) ((completedOf G f i) x) = (g i) x

theorem ScottishBook155.NormedDirectLimit.completedLift_norm_le_one {ι : Type u} [LinearOrder ι] [Nonempty ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (f : (i j : ι) → i ≤ j → G i →ₗᵢ[ℝ] G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] (g : (i : ι) → G i →L[ℝ] H) (hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (hC : ∀ (i : ι) (x : G i), ‖(g i) x‖ ≤ ‖x‖) (z : CompletedCarrier G f) : ‖(completedLift G f g hg 1 ⋯) z‖ ≤ ‖z‖

A coherent componentwise contraction remains contractive after passage to the completed direct limit.