Coherent bidirectional systems

An increasing family of normed spaces equipped with coherent contractive retractions supplies both a directed system and the projection system used at completed limit stages.

structure ScottishBook155.CoherentBiSystem {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] : Type u

Forward linear isometries together with coherent backward contractive projections.

• embed (i j : ι) : i ≤ j → G i →ₗᵢ[ℝ] G j

  Compatible linear isometric embeddings from earlier stages into later stages.

• project (i j : ι) : i ≤ j → G j →L[ℝ] G i

  Contractive continuous linear projections from later stages back to earlier stages.

• embed_refl (i : ι) (x : G i) : (self.embed i i ⋯) x = x
• embed_trans (i j k : ι) (hij : i ≤ j) (hjk : j ≤ k) (x : G i) : (self.embed j k hjk) ((self.embed i j hij) x) = (self.embed i k ⋯) x
• project_embed (a i j : ι) (hai : a ≤ i) (hij : i ≤ j) (x : G i) : (self.project a j ⋯) ((self.embed i j hij) x) = (self.project a i hai) x
• project_retracts (i j : ι) (hij : i ≤ j) (x : G i) : (self.project i j hij) ((self.embed i j hij) x) = x
• project_contractive (i j : ι) (hij : i ≤ j) (x : G j) : ‖(self.project i j hij) x‖ ≤ ‖x‖

theorem ScottishBook155.CoherentBiSystem.ext {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] {B D : CoherentBiSystem G} (hembed : B.embed = D.embed) (hproject : B.project = D.project) : B = D

A coherent bidirectional system is determined by its forward and backward maps; all coherence and norm fields are propositions.

instance ScottishBook155.CoherentBiSystem.directedSystem {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (B : CoherentBiSystem G) : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(B.embed x1 x2 x3)

A coherent bidirectional system gives Mathlib's directed-system coherence for its forward embeddings.

noncomputable def ScottishBook155.CoherentBiSystem.totalProject {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (B : CoherentBiSystem G) (a i : ι) : G i →L[ℝ] G a

Projection from any component to component a: embed forward below a, and retract backward above a.

Equations

• ScottishBook155.CoherentBiSystem.totalProject G B a i = if hia : i ≤ a then (B.embed i a hia).toContinuousLinearMap else B.project a i ⋯

theorem ScottishBook155.CoherentBiSystem.totalProject_of_le {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (B : CoherentBiSystem G) {i a : ι} (hia : i ≤ a) (x : G i) : (totalProject G B a i) x = (B.embed i a hia) x

theorem ScottishBook155.CoherentBiSystem.totalProject_of_ge {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (B : CoherentBiSystem G) {a i : ι} (hai : a ≤ i) (x : G i) : (totalProject G B a i) x = (B.project a i hai) x

noncomputable def ScottishBook155.CoherentBiSystem.projectionSystem {ι : Type u} [LinearOrder ι] (G : ι → Type u) [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → NormedSpace ℝ (G i)] (B : CoherentBiSystem G) : CoherentRetractionLimit.ProjectionSystem G B.embed

The total projections form the projection system required at a completed direct limit.

Equations

• ScottishBook155.CoherentBiSystem.projectionSystem G B = { project := ScottishBook155.CoherentBiSystem.totalProject G B, coherent := ⋯, contractive := ⋯, identityBelow := ⋯ }