Appending a completed limit stage to a coherent chain

theorem ScottishBook155.ProtectedChain.appendLimitSourceDirectedSystem {ι : 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.appendLimitTargetDirectedSystem {ι : 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)

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

The family obtained by placing the completed limit stage at a new top.

Equations

• C.appendLimitStage hr hL none = C.limitStage hr hL
• C.appendLimitStage hr hL (some i) = C.stage i

noncomputable def ScottishBook155.ProtectedChain.appendLimitLink {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) (i j : WithTop ι) (hij : i ≤ j) : ProtectedLink (C.appendLimitStage hr hL i) (C.appendLimitStage hr hL j) L

The old links and the canonical links into the completed limit.

Equations

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

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

Adjoin the completed direct limit as one new top stage.

Equations

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

theorem ScottishBook155.ProtectedChain.appendLimit_reindex_withTopCoe {κ : Type} [LinearOrder κ] [Nonempty κ] {r L : ℝ} (D : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) : (D.appendLimit hr hL).reindex withTopCoeOrderEmbedding = D

Restricting an appended limit chain back to the old indices recovers the original chain.