Should "Inverse equals symm" be a simp lemma?

Stream: Is there code for X?

[Terence Tao]

I recently had need of the following trivial lemma:

lemma LinearEquiv.inv_eq_symm {R : Type*} {E:Type*} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (S : E ≃ₗ[R] E) : S⁻¹ = S.symm := rfl

For some reason this lemma was outside the capacity of simp to resolve. Should one add it as a simp lemma? I guess there has to be a decision which of S⁻¹ and S.symm gets to be in simp normal form, as there are plenty of nice simp lemmas for both, but it was a speed bump for me to see simp get stuck because it could not equate the two here.

(I guess one would also need Perm.inv_eq_symm, etc.)

[Yakov Pechersky]

It depends on whether you are working on them in group expressions like S * S⁻¹, projection expressions like S⁻¹.comp S, or application expressions like S⁻¹ x. For the latter two, the .symm syntax will likely be more effective in further simplifying.

[Jireh Loreaux]

I think it should be a lemma, but not a simp lemma. When you want to work with the group structure of the linear automorphisms, you want to use S⁻¹, probably not S.symm. (e.g., imagine if you had (S⁻¹) ^ n and is simplified it to S.symm ^ n). Potentially it could go the other way, but I don't think that would be ideal either.

[Jireh Loreaux]

Probably the right answer here is to have an apply lemma marked @[simp] which performs the simplification (⁻¹ to .symm), but only if the linear map is applied to a vector. So I think S⁻¹ x = S.symm x makes sense as a simp lemma.

[Jireh Loreaux]

But we should also have the lemma you wrote.

[Eric Wieser]

Terence Tao said:

(I guess one would also need Perm.inv_eq_symm, etc.)

docs#Equiv.Perm.inv_def already exists :)

[Edward van de Meent]

Jireh Loreaux said:

I think it should be a lemma, but not a simp lemma. When you want to work with the group structure of the linear automorphisms, you want to use S⁻¹, probably not S.symm. (e.g., imagine if you had (S⁻¹) ^ n and is simplified it to S.symm ^ n). Potentially it could go the other way, but I don't think that would be ideal either.

if this is your context, doesn't the use of a type alias prevent the simp lemma from applying?

[Jireh Loreaux]

What type alias?

[Edward van de Meent]

there should be one... but i'm looking and it indeed looks to not exist

[Jireh Loreaux]

I'm not sure why you think there should be one.

[Edward van de Meent]

we have docs#MulAut for the same reason

[Jireh Loreaux]

That's an abbrev.

[Jireh Loreaux]

There is no abstraction boundary here.

[Edward van de Meent]

ah, you're right

[Edward van de Meent]

drat

[Jireh Loreaux]

(and I'm not sure why you would want one)

[Edward van de Meent]

recently, an example came up where we would need this... you can also define multiplication pointwise

[Edward van de Meent]

sometimes

[Edward van de Meent]

so it's not like we don't need type aliases ever in these kinds of cases

[Jireh Loreaux]

So, presumably you're talking about e.g., the type M ≃ₜ M where M is a topological monoid? Sure, it's possible to define * pointwise there, but I don't think we have any instances like that. I would believe that the pointwise instances are only defined for the one-way morphisms (but perhaps I'm wrong).

[Edward van de Meent]

i'm talking about things like #Is there code for X? > `Mul` instance on algebra homomorphisms from monoid algebra

[Aaron Liu]

See also #Is there code for X? > `Mul` instance on algebra homomorphisms from monoid algebra @ 💬

[Edward van de Meent]

in particular, docs#MonoidHom.instCommMonoid is a concrete example

[Eric Wieser]

Monoid.End is an abstraction boundary, unlike all the others

[Jireh Loreaux]

No? It's also an abbrev (misread)

[Jireh Loreaux]

(deleted)

[Eric Wieser]

Jireh Loreaux said:

No? It's also an abbrev

src#Monoid.End disagrees with you.

[Jireh Loreaux]

oops, sorry, I misread as docs#Module.End, my apologies.

[Eric Wieser]

It is a little surprising that Monoid is different to all the others, but I think pragmatically it's the right choice.

[Yaël Dillies]

#23705 is a first step towards having Module.End not be an abbrev anymore if we want to (and if we don't want to I still think we should merge #23705)

[Martin Dvořák]

Reminds me of:
https://github.com/Ivan-Sergeyev/seymour/blob/b8ae62db083db99cdd94d9bccedf3f45fde03d78/Seymour/Matrix/OfLinearMaps.lean#L4
Should it be a simp lemma? If so, in which direction?