The limit clause for protected chains

The uniform recovery identity passes from a coherent protected chain to its completed direct limit. Together with DirectedLimitStage, this constructs a new protected stage at every nonempty limit segment.

theorem ScottishBook155.ProtectedChain.sourceDirectedSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : DirectedSystem (fun (i : ι) => (C.stage i).source.carrier) fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(C.sourceSystem.embed x1 x2 x3)

theorem ScottishBook155.ProtectedChain.targetDirectedSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : DirectedSystem (fun (i : ι) => (C.stage i).target.carrier) fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(C.targetSystem.embed x1 x2 x3)

@[reducible, inline]

abbrev ScottishBook155.ProtectedChain.LimitSource {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) : Type u

The completed direct limit of the source spaces in the protected chain.

Equations

• C.LimitSource = ScottishBook155.NormedDirectLimit.CompletedCarrier (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem.embed

@[reducible, inline]

abbrev ScottishBook155.ProtectedChain.LimitTarget {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) : Type u

The completed direct limit of the target spaces in the protected chain.

Equations

• C.LimitTarget = ScottishBook155.NormedDirectLimit.CompletedCarrier (fun (i : ι) => (C.stage i).target.carrier) C.targetSystem.embed

noncomputable def ScottishBook155.ProtectedChain.sourceProjectionSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : CoherentRetractionLimit.ProjectionSystem (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem.embed

The compatible source projections, packaged for extension to the completed limit.

Equations

• C.sourceProjectionSystem = ScottishBook155.CoherentBiSystem.projectionSystem (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem

noncomputable def ScottishBook155.ProtectedChain.targetProjectionSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : CoherentRetractionLimit.ProjectionSystem (fun (i : ι) => (C.stage i).target.carrier) C.targetSystem.embed

The compatible target projections, packaged for extension to the completed limit.

Equations

• C.targetProjectionSystem = ScottishBook155.CoherentBiSystem.projectionSystem (fun (i : ι) => (C.stage i).target.carrier) C.targetSystem

noncomputable def ScottishBook155.ProtectedChain.completedMap {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) : C.LimitSource → C.LimitTarget

The map between completed limits induced by the uniformly nonexpansive stage maps.

Equations

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

theorem ScottishBook155.ProtectedChain.completed_recovery_of_dist_lt {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (a : ι) (x : C.LimitSource) (hx : dist x (CoherentRetractionLimit.ProjectionSystem.approx (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem.embed C.sourceProjectionSystem a x) < L) : (CoherentRetractionLimit.ProjectionFamily.completedProjection (fun (i : ι) => (C.stage i).target.carrier) C.targetSystem.embed (CoherentRetractionLimit.ProjectionSystem.family (fun (i : ι) => (C.stage i).target.carrier) C.targetSystem.embed C.targetProjectionSystem a)) (C.completedMap x) = (C.stage a).map ((CoherentRetractionLimit.ProjectionFamily.completedProjection (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem.embed (CoherentRetractionLimit.ProjectionSystem.family (fun (i : ι) => (C.stage i).source.carrier) C.sourceSystem.embed C.sourceProjectionSystem a)) x)

Recovery to a fixed component extends from the algebraic direct limit to the completed limit throughout the open recovery band.

noncomputable def ScottishBook155.ProtectedChain.limitStage {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) : ProtectedStage r

The completed direct limit of a protected chain is again a protected stage. This is the limit clause used by the transfinite recursion.

Equations

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

noncomputable def ScottishBook155.ProtectedChain.toLimitLink {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) (a : ι) : ProtectedLink (C.stage a) (C.limitStage hr hL) L

Every component is coherently linked to the completed limit stage.

Equations

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