Define bundled homs using `calc`

Stream: maths

[Yury G. Kudryashov]

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?

[Yury G. Kudryashov]

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.

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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))

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Chris Hughes]

You can always do the calc from right to left.