Zulip Chat Archive

Stream: general

Topic: calc for linear equivs


Oliver Nash (May 26 2021 at 14:59):

Should I be able to use calc to construct a linear_equiv?

Oliver Nash (May 26 2021 at 14:59):

For example, should calc_linear_equiv work in the following:

import algebra.module.linear_map

variables (R M N P : Type*)
variables [semiring R]
variables [add_comm_monoid M] [module R M]
variables [add_comm_monoid N] [module R N]
variables [add_comm_monoid P] [module R P]

/-- Works. -/
def calc_equiv (e₁ : M  N) (e₂ : N  P) : M  P :=
calc M  N : e₁
   ...  P : e₂

/- Fails with error:
type mismatch at application
  linear_equiv.trans
term
  M
has type
  Type u_2 : Type (u_2+1)
but is expected to have type
  module ?m_1 ?m_2 : Type (max ? ?)
-/
def calc_linear_equiv (e₁ : M ≃ₗ[R] N) (e₂ : N ≃ₗ[R] P) : M ≃ₗ[R] P :=
calc M ≃ₗ[R] N : e₁
   ... ≃ₗ[R] P : e₂

Eric Wieser (May 26 2021 at 15:01):

@[trans] only works on types with two arguments, I think. docs#equiv is therefore fine, but docs#linear_equiv has way too many. I imagine even mul_equiv is not an option here. Maybe comparing docs#equiv.trans and docs#linear_equiv.trans can help.

Oliver Nash (May 26 2021 at 15:02):

I see!

Oliver Nash (May 26 2021 at 15:03):

Does @[trans] do anything else or are many such decorators basically pointless then?

Oliver Nash (May 26 2021 at 15:03):

(Also, if anyone has a reference for this "two arguments" rule, I'd be grateful to receive it.)

Eric Wieser (May 26 2021 at 15:05):

My hunch is it's pointless...

Eric Wieser (May 26 2021 at 15:05):

The attribute also works for tactic#transitivity I think

Eric Wieser (May 26 2021 at 15:05):

But I expect it to fail in the same way

Oliver Nash (May 26 2021 at 15:07):

Right, thanks.

Eric Wieser (May 26 2021 at 15:07):

Here's a possible fix - replace the weird {module} binders with [module] in linear_equiv.trans

Oliver Nash (May 26 2021 at 15:10):

The supposition being that implicit, but not typeclass, arguments contribute to the magical "two arguments" count?

Eric Wieser (May 26 2021 at 15:32):

Well, or that my previous rationale was nonsense.

Oliver Nash (May 26 2021 at 16:29):

Very unlikely! I'm going to leave this alone though, I don't want this badly enough.


Last updated: Dec 20 2023 at 11:08 UTC