# Zulip Chat Archive

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

s and `linear_equiv`

s, 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):

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