# 菲文笔记 | Technical theorem (v2) ---- level of camera

This is coming to you from continued) camera level one = {R, S, '} ==> camera of level two {Rs, Rs', R', ...}.

.

Step 7, Para two (b) ——

Since nR' := G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ' ~ L' +  ⌊(n + 1)Δ' ⌋ - nΔ' = 2M' + nN' ~Q 0/ X...

---- Recall, the target is to arrive at R|s = Rs; see Para two (a).

---- Recall, Rs is defined at the beginning of Step 6, and R is defined in Step 7, Para two (a).

---- Recall, L' + P' ~ G' is setup at the end of Step 6.

---- Where does the idea of defining nR' come from ?

---- The most close expression is (from Step 6) ——

(L' + P')|s' ~ Gs' := nRs' + nΔs' -  ⌊(n + 1)Δs'⌋ + Ps'.

---- By a rearrangement of terms, one arrives at nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs'.

---- So far, one has Rs, Rs', and R.

---- Rs and R have similar shape.

---- For one thing, nR: = G; for another, B := B + R.

---- However, one cannot define nR' := G', for there is an "exceptional" matter.

---- So, one resorts to the expression for nRs'.

---- That is, to define nR' by overlooking s' in the expression.

---- Indeed, the expression G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ' can stand.

---- So, let it be nR'.

---- So comes nR' := G' - P' + ⌊(n + 1)Δ' ⌋ - nΔ'.

---- The rest matter is straightforward, except for the last connection.

---- I cannot see 2M' + nN' ~Q 0/ X. (?)

.

New comments: The camera of nR' appears not apparent.

---- Perhaps, Rs, Rs' and R' should be added in the camera.

---- As Rs' is the pullback of Rs, one expects that R' is the pullback of R.

---- While the targe is of R|s = Rs, one needs to arrive there through R'|s' = Rs'.

---- So arises the need to define R'.

---- In regard of  R'|s' = Rs', one needs to "derive" R' through Rs'.

---- Actually, nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs' by Step 6.

---- So, one derives nRs' = Gs' - Ps' +  ⌊(n + 1)Δs'⌋ - nΔs' = (G' - P' +  ⌊(n + 1)Δ'⌋ - nΔ')|s'.

---- It is desirable to have nR':= G' - P' +  ⌊(n + 1)Δ'⌋ - nΔ', In regard of  R'|s' = Rs'.

(It appears that "camera" is of targets).

.

... and since ⌊(n + 1)Δ ⌋ - nΔ = 0, we get φ* nR' = G = nR and that R' is the pullback of R.

---- To be complete, I would calculate ——

(Note: the star in " φ* " is a subscript.)

φ* nR' = φ* (G' - P' + ⌊(n + 1)Δ'⌋  - nΔ')

φ* (G') - φ* (P') + φ* (⌊(n + 1)Δ'⌋ - nΔ')

= G + 0 + 0.

= nR.

.

New comment: This is to show that nR' is indeed the pullback of R (as desired).

.

That is, φ* nR' = nR, i.e. φ* R' = R. (So, R' is the pullback of R.)

.

Comment: It appears that the handle of principle behind the deduction stands out.

.

Now by Step 6, nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs' = (G' - P' + ⌊(n + 1)Δ'⌋ - nΔ')|s' = nR'|s' which means Rs' = R'|s'...

---- The preceding two equations have no new elements.

---- The third one comes only after the definition of nR'.

---- The net effect is nRs' = nR'|s', i.e. Rs' = R'|s'.

.

New comment: The key is the expression nRs' = Gs' - Ps' + ⌊(n + 1)Δs'⌋ - nΔs'  (set up by Step 6), plus the desire to seperate s'.

.

...hence Rs and R|s both pull back to Rs' which implies Rs = R|s as required.

---- This can be clarified by ——

.

Rs' = R'|s' --> R|s

||                   ||

Rs' -----------> Rs

.

Summary comment: I expect to rewrite the proof in a different style.

.

New comment: It appears that one is assumed to take for grounded R'|s' as the pullback of R|s.

.

↑↓ ℭ ℜ I|φ∪∩∈ ⊆ ⊂ ⊇ ⊃ ⊄ ⊅ ≤ ≥ Γ Θ α Δ δ μ ≠ ⌊ ⌋ ⌈ ⌉ ∨∧∞Φ⁻⁰ 1

Calling graph for the technical theorem (Th1.9) ——

.

Th1.9

|

[5, 2.13(7)]   Lem 2.26   Pro4.1   Lem2.7

|

.....................................................Lem2.3

Note: Th1.9 is only called by Pro.5.11, one of the two devices for Th1.8, the executing theorem.

Pro4.1

|

[5, ?]   [37, Pro3.8]   [5, Lem3.3]   Th2.13[5, Th1.7]   [16, Pro2.1.2]    [25, Th17.4]

Completed notes of the first round learning for v2 Pro.4.1 are * (v1).

.

.

It is my hope that this action would not be viewed from the usual perspective that many adults tend to hold.

http://www.blog.sciencetimes.com.cn/blog-315774-1300446.html

## 全部精选博文导读

GMT+8, 2021-10-25 06:48