division_monoid and is_unit

Stream: maths

[Alexander Bentkamp]

There are a couple of lemmas about is_unit that depend on division_monoid such as docs#is_unit.inv_mul_eq_iff_eq_mul. Unfortunately, I can't use these lemmas when working with square matrices because a division_monoid requires x⁻¹⁻¹ = x, even for non-invertible x. Would removing that requirement from division_monoid be an option? Or should I reprove these lemmas specifically for matrices? Or do we need two finer-grained type-classes here?

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Nevermind, I misread your question.

[Moritz Doll]

Isn't the problem that the matrix multiplication is only a has_mul.mul if the matrices are square? and similarly the inverse of a : A has to have type A. I have the same problem with defining the resolvent and I was about to define my own version of inverse and unit, but if that problem occurs several times, then we might want to find a better solution.

[Junyan Xu]

It seems we lack a lemma saying if h : is_unit x then x⁻¹ = ↑(h.unit⁻¹) for a matrix x. After rewriting by that, what you want is defeq to docs#units.inv_mul_eq_iff_eq_mul.

[Alexander Bentkamp]

@Moritz Doll That's yet another problem, but I would already be happy with a solution that works for square matrices.

[Moritz Doll]

ah for non-invertible matrices the inverse is defined as zero and not as the matrix itself

[Moritz Doll]

and I also misread your question, I am sorry.

[Alexander Bentkamp]

Yes, the inverse of a noninvertible matrix would be the matrix itself, that would also work. Then we could use division_monoid directly. On the other hand, the definition of the inverse as ring.inverse A.det • A.adjugate is currenlty quite elegant.

[Moritz Doll]

the issue goes down to ring.inverse, but changing it there seems like a dangerous thing

[Moritz Doll]

I would guess that there a quite a few things that rely on the inverse being zero if the element is non-invertible

[Alexander Bentkamp]

Right, it would probably be easier to modify division_monoid, although I am not sure how much depends on it.

[Alexander Bentkamp]

@Junyan Xu Yes, that would be a nice way to transfer the lemmas from units to matrix. But it would still require us to create matrix-specific copies of the lemmas about units. I was wondering if we could use type class inference instead of copies.

[Jireh Loreaux]

@Yaël Dillies who put some serious thought into the creation of division_monoid

[Yaël Dillies]

Currently, matrices are not a division monoid because they do not respect docs#inv_inv.

[Yaël Dillies]

Removing this field to docs#division_monoid would make ~50 lemmas not true for them (out of ~300 division_monoid lemmas) iirc.

[Yaël Dillies]

What I suggested back then was to redefine inversion of matrices so as to make this axiom true, but @Yakov Pechersky says thus is too hard to ensure. I don't know whether I believe it but I also don't know much about matrices.

[Moritz Doll]

it feels a bit like the last three fields in division_monoid almost force the inverse to be a real inverse and I wonder whether the lemma Alexander was first mentioning is true without the is_unit assumption

[Yaël Dillies]

No, that lemma is wrong if you do not assume is_unit.

[Moritz Doll]

but there more serious question would be whether it is possible to prove it with something less than division_monoid

[Yaël Dillies]

Yes you can

[Yaël Dillies]

Its proof doesn't mention inv_inv.

[Yaël Dillies]

The easy way out is to write the typeclass division_monoid - inv_inv, but I was trying not to overengineer the hierarchy. The solution I would like to see is making inv_inv true for matrix.

[Jireh Loreaux]

Does this not work for div_inv_monoid?

[Yaël Dillies]

No, div_inv_monoid just states the definition of division in terms of inversion.

[Moritz Doll]

yeah, one would need a typeclass for having a⁻¹ = ↑(ha.unit)⁻¹, where ha : is_unit a, but I don't know whether that is worth it (probably not)

[Jireh Loreaux]

If it's just matrices for now, I think adding a standalone lemma for those is okay.

[Yakov Pechersky]

inv_inv_inv is true for matrices as it right now

[Yakov Pechersky]

If a matrix is not invertible, then currently inv sends it to 0. so A\inv\inv = 0 even when A \ne 0.

[Yakov Pechersky]

Let's say A\inv = A when A is not invertible. Then inv_inv is true. But then a lot of nice lemmas about the distribution of inv over mul, or zpow don't work.

[Eric Rodriguez]

I mean, I'd rather have lemmas applying sometimes under more conditions (e.g. requiring invertibility) instead of having to rewrite lemmas, but I'm not sure of the exact details of this situation. We can also prove lemmas about the adjugate+determinant combo separately, and leave the inv lemmas to another inv so that the typeclass system functions better.

[Yakov Pechersky]

There is also docs#ring.inverse

[Yakov Pechersky]

That's re Moritz Doll's suggestion

[Yakov Pechersky]

Sorry, I see that Alexander already mentioned it via the matrix.inv definition