Zulip Chat Archive

Stream: maths

Topic: Define bundled homs using `calc`


view this post on Zulip Yury G. Kudryashov (May 05 2020 at 04:50):

If monoid_hom.comp was using another order of arguments, it would be possible to write something like

calc M →* N : f
... →* P : g

Can I make monoid_hom.comp usable for calc without changing order of arguments?

view this post on Zulip Yury G. Kudryashov (May 05 2020 at 04:51):

Right now I want to define a linear_map as a long composition of linear_maps and linear_equivs, and calc would make the definition much more readable.

view this post on Zulip Johan Commelin (May 05 2020 at 04:52):

Maybe we need to introduce cocalc that will swap the order of the arguments....

view this post on Zulip Yury G. Kudryashov (May 05 2020 at 04:58):

Or wait till those who chose the order of arguments in category_struct.comp will come and tell us to use it everywhere ;-)

view this post on Zulip Yury G. Kudryashov (May 05 2020 at 05:18):

Now I use

def linear_proj_of_is_compl (h : is_compl p q) :
  E [k] p :=
((comap p.subtype (p  q)).quot_equiv_of_eq_bot
  (eq_bot_mono (comap_mono inf_le_right) $ disjoint_iff_comap_eq_bot.1 h.disjoint) :
  (comap p.subtype (p  q)).quotient [k] p).comp $
((quotient_inf_equiv_sup_quotient p q).symm :
  (comap (p  q).subtype q).quotient [k] (comap p.subtype (p  q)).quotient).comp $
(comap (p  q).subtype q).mkq.comp
((linear_equiv.of_top (p  q) h.sup_eq_top).symm : E [k] (p  q : submodule k E))

view this post on Zulip Reid Barton (May 05 2020 at 11:21):

Hmm I think I've done something a lot like this, let me see why it worked for me...

view this post on Zulip Reid Barton (May 05 2020 at 11:23):

okay yes, it is because I used the same order as equiv.trans

view this post on Zulip Reid Barton (May 05 2020 at 11:23):

https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pair.lean#L296

view this post on Zulip Chris Hughes (May 05 2020 at 11:30):

You can always do the calc from right to left.


Last updated: May 14 2021 at 19:21 UTC