book
book copied to clipboard
HoTT
11.3.40 incorrect proof
11.3.40 says that if we have f : Q -> Q -> Q non-expanding on both components then we can extend it to f' : R -> R -> R also non-expanding on both components.
When defining the limit case for f', the book says that if u ~e v then f'(x (e/3))(u) ~(e/3) f'(x (e/3))(v) by induction hypothesis, but this is wrong. The induction hypothesis gives us that if u ~e v then for all n, f'(x n)(u) ~e f'(x n)(v). We can't get f'(lim x)(u) ~e f'(lim x)(v) from that.
We can however use 11.3.34 (~ is rounded) to get u ~(e-d) v then by the induction hypothesis f'(x (d/2))(u) ~(e-d) f'(x (d/2)) and by constructor f'(lim x)(u) ~e f'(lim x)(v).
Also
Therefore, by the second constructor of ∼ , we have f ̄ ( rat ( q ))( v ) ∼ e f ̄ ( lim ( y ))( v ) as required.
It's not by the second constructor, it's by 11.3.36.
Also, why do we have for q r : Q, e : Q+ if |q - r| < e then forall u : R, f' (rat q) u ~e f' (rat r) u? (first condition to check for the recursion)
EDIT: R-induction on forall u d, |q - r| < d < e -> f' (rat q) u ~d f' (rat r) u, and Q is dense to there is such a d.
Also typo in the statement in the lemma:
Furthermore, for all u, v, w : R c and q : Q +
should be
Furthermore, for all u, v, w : R c and \epsilon : Q + ,
I think you are right about all of this. (Also, in the second paragraph of the proof the d,e:Q and e:Q should be Q+.) Would you mind submitting a pull request?
@SkySkimmer any chance you'll be able to submit a pull request? I'm trying to clear out old issues, but I don't have the time to think hard enough about this to write the necessary text myself.
Therefore, by the second constructor of ∼ , we have f ̄ ( rat ( q ))( v ) ∼ e f ̄ ( lim ( y ))( v ) as required.
It's not by the second constructor, it's by 11.3.36.
It is not clear to me how to use either the second constructor of ~ or 11.3.36 to conclude that f'(rat q)(v) ~_ε f'(lim y)(v), as they both only give that rat q ~_ε lim y.
It seems one can solve this by replacing the relation
h ⌒_ε k :≡ ∀ (u : ℝ). h(u) ~_ε k(u)
by the relation
h ⌒_ε k :≡ ∃ (ε' : ℚ₊). ((ε' < ε) ∧ (∀ (u : ℝ). h(u) ~_{ε'} k(u))),
so that both ~ and ⌒ are open. Then show and use that ε' < ε and ∀ (r : ℚ). h(rat r) ~{ε'} k(rat r) implies ∀ (u : ℝ). h(u) ~ε k(u).
I wrote this issue while formalizing the proofs in https://github.com/SkySkimmer/HoTTClasses/ so what I wrote should be correct. I don't remember how it all works though.