feat(topology/fundamental_groupoid): fundamental groupoid #1160
Conversation
| finish := λ t, by erw [if_neg (not_le_of_lt $ half_lt_self (zero_lt_one : (0:ℝ)<1))]; | ||
| simp only [set.Icc_one_val, add_sub_cancel, max_eq_left (zero_le_one : (0:ℝ)≤1)]; exact G.6 t } | ||
|
|
||
| noncomputable def comp {α β : path y z} (F : homotopy f g) (G : homotopy α β) : |
There was a problem hiding this comment.
Please, don't use α and β for paths. I know it would be an excellent mathematical notation, but in a Lean context these have to be types, and nothing else.
There was a problem hiding this comment.
These names are confusing anyways because α and β are the same sort of thing (paths) as f and g. I suggest a convention of using names like f₀ and f₁ for paths (or maps or whatever) related by a homotopy; it makes the structure clearer and saves on letters too.
|
@kckennylau Can we please have a coercion from paths to functions? |
|
|
||
| variables {w x y z : X} {f g h : path x y} | ||
|
|
||
| def refl (f : path x y) : homotopy f f := |
| start := λ t, rfl, | ||
| finish := λ t, rfl } | ||
|
|
||
| def symm (F : homotopy f g) : homotopy g f := |
| start := λ t, by simp only [set.Icc_zero_val, sub_zero]; convert F.6 t, | ||
| finish := λ t, by simp only [set.Icc_one_val, sub_self]; convert F.5 t } | ||
|
|
||
| noncomputable def trans (F : homotopy f g) (G : homotopy g h) : homotopy f h := |
|
I think it's better not to start with paths but with general homotopies between continuous maps X -> Y, and the notion of "homotopy rel". Otherwise you will have to repeat all the work (mainly The API I designed for cylinder-based homotopy theory is at https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/formal/cylinder/homotopy.lean; you might want to borrow ideas/lemmas/names from there. Note that I didn't handle composition/transitivity there, since I wanted to avoid (or at least hide elsewhere) the explicit formulas involved in composition and associativity. |
|
|
||
| noncomputable def assoc (f : path w x) (g : path x y) (h : path y z) : | ||
| homotopy ((f.comp g).comp h) (f.comp (g.comp h)) := | ||
| { to_fun := λ p, if 4 * p.2.1 / (1 + p.1.1) ≤ 1 |
There was a problem hiding this comment.
In math you ought to somehow avoid being able to do any computation at all here. Both sides are some continuous reparameterization of the function defined on [0, 3] by f, then g, then h, and whatever those reparameterizations [0, 1] -> [0, 3] are, you can linearly interpolate between them to define a homotopy which is constant at the endpoints. I'm not sure how easy it is to express that to Lean though (and this is the point where I gave up on this kind of approach when I tried this).
Same comments, but doable for sure, apply to comp_id and comp_inv. And even for definitions like symm, maybe it's better to define them in terms of what I called congr_right (or possibly congr_left, Scott has caused me to lose all sense of direction). If you have access to Switzer's book Algebraic Topology I think this stuff is explained properly in Chapter 2 there--all these basic constructions are induced by structure on the unit interval (or more generally, on a cylinder functor, as in https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/formal/cylinder/definitions.lean).
robertylewis
added
the
needs-documentation
robertylewis
added
awaiting-author
robertylewis
changed the title
|
It looks like there's been no further progress for a while, and it seems likely that in the long run we want a much higher level approach to homotopy. I'll close for now, but certainly more work in this direction is very welcome in mathlib. |
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list