## Stream: maths

### Topic: Define bundled homs using calc

#### 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?

#### 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.

#### Johan Commelin (May 05 2020 at 04:52):

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

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

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


#### 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...

#### Reid Barton (May 05 2020 at 11:23):

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

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

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